Uniqueness of Normal Forms for Shallow Term Rewrite Systems

Nicholas Radcliffe, Luis Moraes, Rakesh Verma

Uniqueness of normal forms ($U{N}^{=}$) is an important property of term rewrite systems. $U{N}^{=}$ is decidable for ground (i.e., variable-free) systems and undecidable in general. Recen…