Update: Jul 28, 2014

WPTE 2014 Paper

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

Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner
In Proceedings of the 1st International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE'14),
Vol. 40 of OpenAccess Series in Informatics (OASIcs), issue 1, pp.\ 39-50, Schloss Dagstuhl Leibniz - Zentrum für Informatik, July 2014.
The SR 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 SR transformation. 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 SR transformation. In this paper, we show that the SR transformation is sound for weakly left-linear normal 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 which is obtained by the simultaneous unraveling proposed by Marchiori. Then, we use the fact that the unraveling is sound for weakly left-linear normal CTRSs.
[OASIcs] [full version (pdf)]

Sakai Lab. Graduate School of Informatics Dept. of Information Engineering Graduate School/School of Engineering Nagoya University
Produced by N.Nishida (nishida @ i.nagoya-u.ac.jp)