10.4230/LIPICS.FSTTCS.2010.284
Radcliffe, Nicholas
Nicholas
Radcliffe
Verma, Rakesh M.
Rakesh M.
Verma
Uniqueness of Normal Forms is Decidable for Shallow Term Rewrite Systems
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2010
Article
term rewrite systems
uniqueness of normal forms
decidability
shallo w rewrite systems
flat rewrite systems
Lodaya, Kamal
Kamal
Lodaya
Mahajan, Meena
Meena
Mahajan
2010
2010-12-14
2010-12-14
2010-12-14
en
urn:nbn:de:0030-drops-28715
10.4230/LIPIcs.FSTTCS.2010
978-3-939897-23-1
1868-8969
10.4230/LIPIcs.FSTTCS.2010
LIPIcs, Volume 8, FSTTCS 2010
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
2013
8
24
284
295
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Lodaya, Kamal
Kamal
Lodaya
Mahajan, Meena
Meena
Mahajan
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2010
8
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
469486 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), pages 284-295