License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2012.193
URN: urn:nbn:de:0030-drops-34936
URL: http://drops.dagstuhl.de/opus/volltexte/2012/3493/
Go to the corresponding Portal


Gmeiner, Karl ; Gramlich, Bernhard ; Schernhammer, Felix

On Soundness Conditions for Unraveling Deterministic Conditional Rewrite Systems

pdf-format:
Document 1.pdf (624 KB)


Abstract

We study (un)soundness of transformations of conditional term rewriting systems (CTRSs) into unconditional term rewriting systems (TRSs). The focus here is on analyzing (un)soundness of so-called unravelings, the most basic and natural class of such transformations. We extend our previous analysis from normal 1-CTRSs to the more general class of deterministic CTRSs (DCTRSs) where extra variables in right-hand sides of rules are allowed to a certain extent. We prove that the previous soundness results based on weak left-linearity and on right-linearity can be extended from normal 1-CTRSs to DCTRSs. Counterexamples show that such an extension to DCTRSs does not work for the previous criteria which were based on confluence and on non-erasingness, not even for right-stable systems. Yet, we prove weaker versions of soundness criteria based on confluence and on non-erasingness. Finally, we compare our approach and results with other recently established soundness criteria for unraveling DCTRSs.

BibTeX - Entry

@InProceedings{gmeiner_et_al:LIPIcs:2012:3493,
  author =	{Karl Gmeiner and Bernhard Gramlich and Felix Schernhammer},
  title =	{{On Soundness Conditions for Unraveling Deterministic Conditional Rewrite Systems}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12) },
  pages =	{193--208},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Ashish Tiwari},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3493},
  URN =		{urn:nbn:de:0030-drops-34936},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.RTA.2012.193},
  annote =	{Keywords: Conditional term rewriting system (CTRS), deterministic   CTRS, transformation, simulation, soundness}
}

Keywords: Conditional term rewriting system (CTRS), deterministic CTRS, transformation, simulation, soundness
Seminar: 23rd International Conference on Rewriting Techniques and Applications (RTA'12)
Issue Date: 2012
Date of publication: 15.05.2012


DROPS-Home | Fulltext Search | Imprint Published by LZI