Complexity of Normal Form Properties and Reductions for Term Rewriting Problems Complexity of Normal Form Properties and Reductions for Term Rewriting Problems
Rakesh M Verma · Fundamenta Informaticae · 2009
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.