On (Un)Soundness of Unravelings

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.