The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2010.284
URN: urn:nbn:de:0030-drops-28715
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2871/
Go to the corresponding LIPIcs Volume Portal

Radcliffe, Nicholas ; Verma, Rakesh M.

Uniqueness of Normal Forms is Decidable for Shallow Term Rewrite Systems

pdf-format:
25.pdf (0.4 MB)

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 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.

BibTeX - Entry

@InProceedings{radcliffe_et_al:LIPIcs:2010:2871,
  author =	{Nicholas Radcliffe and Rakesh M. Verma},
  title =	{{Uniqueness of Normal Forms is Decidable for Shallow Term Rewrite Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{284--295},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Kamal Lodaya and Meena Mahajan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2871},
  URN =		{urn:nbn:de:0030-drops-28715},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.284},
  annote =	{Keywords: term rewrite systems, uniqueness of normal forms, decidability, shallo w rewrite systems, flat rewrite systems}
}

Keywords: term rewrite systems, uniqueness of normal forms, decidability, shallo w rewrite systems, flat rewrite systems
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Issue Date: 2010
Date of publication: 14.12.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI