ON (UN)SOUNDNESS OF UNRAVELINGS

21st International Conference on Rewriting Techniques and Applications

KARL GMEINER 1 AND BERNHARD GRAMLICH 1 AND FELIX SCHERNHAMMER 1

Others  :  http://drops.dagstuhl.de/opus/volltexte/2010/2648/pdf/10002.GmeinerKarl.2648.pdf
PID  :  44836

来源: CEUR

【 摘 要 】

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.