On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings

ABSTRACT. The Serbanuta-Rosu transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, converts a left-linear confluent normal conditional term rewriting system (CTRS) into an unconditional term rewriting system (TRS) which is computationally equivalent to the original CTRS. This paper aims at investigating sufficient conditions for soundness of the Serbanuta-Rosu transformation w.r.t.\ reduction. Here, soundness for a CTRS means that reduction of the converted TRS creates no undesired reduction for the CTRS. Left-linearity or confluence of the CTRS are the only known soundness conditions for the Serbanuta-Rosu transformation. In this paper, we show that the Serbanuta-Rosu transformation is sound for weakly left-linear constructor CTRSs. To this end, we first show that every reduction sequence of the transformed TRS starting with a term corresponding to the one considered on the CTRS is simulated by the reduction of the unraveled TRS obtained by the simultaneous unraveling proposed by Marchiori. Then, we use the fact that the unraveling is sound for weakly left-linear normal CTRSs.