eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2010-07-06
119
134
10.4230/LIPIcs.RTA.2010.119
article
On (Un)Soundness of Unravelings
Gmeiner, Karl
Gramlich, Bernhard
Schernhammer, Felix
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol006-rta2010/LIPIcs.RTA.2010.119/LIPIcs.RTA.2010.119.pdf
Conditional rewriting
transformation into unconditional systems
unsoundness
unraveling