Uniqueness of Normal Forms is Decidable for Shallow Term Rewrite Systems

Authors Nicholas Radcliffe, Rakesh M. Verma

Thumbnail PDF


  • Filesize: 458 kB
  • 12 pages

Document Identifiers

Author Details

Nicholas Radcliffe
Rakesh M. Verma

Cite AsGet BibTex

Nicholas Radcliffe and Rakesh M. Verma. Uniqueness of Normal Forms is Decidable for Shallow Term Rewrite Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 284-295, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


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 superclasses of flat systems: left-flat, left-linear systems in which right-hand sides are of depth at most two and right-flat, right-linear systems in which left-hand sides are of depth at most two.
  • term rewrite systems
  • uniqueness of normal forms
  • decidability
  • shallo w rewrite systems
  • flat rewrite systems


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail