Complexity of Normal Form Properties and Reductions for Term
Rewriting Problems Complexity of Normal Form Properties and Reductions for Term
Rewriting Problems
Affiliations: Computer Science Department, University of Houston,
Houston, TX, 77204-3010, USA. rverma@uh.edu
Note: [] Address for correspondence: Comp. Sci. Dept. – 501 PGH,
4800 Calhoun Road, University of Houston, Houston, TX 77204-3010, USA
Abstract: We present several new and some significantly improved
polynomial-time reductions between basic decision problems of term rewriting
systems. We prove two theorems that imply tighter upper bounds for deciding the
uniqueness of normal forms (UN^{=}) and unique normalization (UN^{→})
properties
under certain conditions. From these theorems we derive a new and simpler
polynomial-time algorithm for the UN^{=} property of ground rewrite systems, and
explicit upper bounds for both UN^{=} and UN^{→} properties of left-linear
right-ground systems. We also show that both properties are undecidable for
right-ground systems. It was already known that these properties are
undecidable for linear systems. Hence, in a sense the decidability results are
"close" to optimal.
Keywords: Term rewriting systems, decision problems, reductions, confluence, existence of normal form, uniqueness of normal forms, reachability, joinability, unique normalization
