Gmeiner, K., Gramlich, B., & Schernhammer, F. (2010). On (Un)Soundness of Unravelings. In C. Lynch (Ed.), Proceedings of the 21st International Conference on Rewriting Techniques and Applications (pp. 119–134). LIPIcs - Leibniz International Proceedings in Informatics / Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.RTA.2010.119
Proceedings of the 21st International Conference on Rewriting Techniques and Applications
-
ISBN:
978-3-939897-18-7
-
Band:
6
-
Datum (veröffentlicht):
2010
-
Veranstaltungsname:
21st International Conference on Rewriting Techniques and Applications
-
Veranstaltungszeitraum:
11-Jul-2010 - 13-Jul-2010
-
Veranstaltungsort:
Edinburgh, EU
-
Umfang:
16
-
Verlag:
LIPIcs - Leibniz International Proceedings in Informatics / Dagstuhl Publishing, Volume 6, Dagstuhl
-
Verlag:
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl
-
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.
