DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2010.284

Uniqueness of Normal Forms is Decidable for Shallow Term Rewrite Systems

Authors: Nicholas Radcliffe and Rakesh M. Verma

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{radcliffe_et_al:LIPIcs.FSTTCS.2010.284,
  author =	{Radcliffe, Nicholas and Verma, Rakesh M.},
  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 =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.284},
  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}
}

Search Results

Documents authored by Verma, Rakesh M.

Uniqueness of Normal Forms is Decidable for Shallow Term Rewrite Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message