[Back]

K. Gmeiner, B. Gramlich, F. Schernhammer:
"On (Un)Soundness of Unravelings";
Report No. Technical Report E1852-2010-01, 2010; 23 pages.

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

http://publik.tuwien.ac.at/files/PubDat_194747.pdf