On (Un)Soundness of Unravelings

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 leftlinearity (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.

• Type: Conference
• Year: 2010
• Where: RTA
• Authors: Karl Gmeiner, Bernhard Gramlich, Felix Schernhammer
• Keywords: Conditional System, Normal Conditional Systems, RTA 2010, Theoretical Computer Science, Unconditional Rewrite Systems