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.RTA.2010.119
URN: urn:nbn:de:0030-drops-26485
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2648/
Go to the corresponding LIPIcs Volume Portal

Gmeiner, Karl ; Gramlich, Bernhard ; Schernhammer, Felix

On (Un)Soundness of Unravelings

pdf-format:
10002.GmeinerKarl.2648.pdf (0.2 MB)

Abstract

We revisit (un)soundness of transformations of conditional into
unconditional rewrite systems. The focus here is on so-called
unravelings, the most simple and natural kind of such
transformations, for the class of normal conditional systems without
extra variables. By a systematic and thorough study of existing
counterexamples and of the potential sources of unsoundness we
obtain several new positive and negative results. In particular, we
prove the following new results: Confluence, non-erasingness and
weak left-linearity (of a given conditional system) each guarantee
soundness of the unraveled version w.r.t. the original one. The
latter result substantially extends the only known sufficient
criterion for soundness, namely left-linearity. Furthermore, by
means of counterexamples we refute various other tempting
conjectures about sufficient conditions for soundness.

BibTeX - Entry

@InProceedings{gmeiner_et_al:LIPIcs:2010:2648,
  author =	{Karl Gmeiner and Bernhard Gramlich and Felix Schernhammer},
  title =	{{On (Un)Soundness of Unravelings}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{119--134},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Christopher Lynch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2648},
  URN =		{urn:nbn:de:0030-drops-26485},
  doi =		{10.4230/LIPIcs.RTA.2010.119},
  annote =	{Keywords: Conditional rewriting, transformation into unconditional systems, unsoundness, unraveling}
}

Keywords: Conditional rewriting, transformation into unconditional systems, unsoundness, unraveling
Collection: Proceedings of the 21st International Conference on Rewriting Techniques and Applications
Issue Date: 2010
Date of publication: 06.07.2010

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