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.
