Uniqueness of Normal Forms for Shallow Term Rewrite Systems

TL;DR

This paper proves that the property of uniqueness of normal forms ($UN^=$) is decidable for shallow term rewrite systems, extending previous results and contrasting with the undecidability of related properties.

Contribution

It generalizes the decidability of $UN^=$ to all shallow rewrite systems, showing it is decidable in this class but undecidable for certain linear systems with bounded depth.

Findings

$UN^=$ is decidable for shallow systems.

$UN^=$ is undecidable for certain linear systems with depth constraints.

Contrasts with undecidability of confluence and reachability in flat systems.

Abstract

Uniqueness of normal forms ($UN^=$) is an important property of term rewrite systems. $UN^=$ is decidable for ground (i.e., variable-free) systems and undecidable in general. Recently it was shown to be decidable for linear, shallow systems. We generalize this previous result and show that this property is decidable for shallow rewrite systems, in contrast to confluence, reachability and other properties, which are all undecidable for flat systems. Our result is also optimal in some sense, since we prove that the $UN^=$ property is undecidable for two classes of linear rewrite systems: left-flat systems in which right-hand sides are of depth at most two and right-flat systems in which left-hand sides are of depth at most two.