2026-07-21T14:16:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2871 2024-03-06T10:33:39Z ddc:004 open_access

Uniqueness of Normal Forms is Decidable for Shallow Term Rewrite Systems Radcliffe, Nicholas Verma, Rakesh M. term rewrite systems uniqueness of normal forms decidability shallo w rewrite systems flat rewrite systems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nicholas Radcliffe and Rakesh M. Verma 2010 Is Part Of LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2010.284 urn:nbn:de:0030-drops-28715 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.284 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode