cl-banner

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

Naoki Nishida, Makashi Yanagisawa, and Karl Gmeiner

Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014), OpenAccess Series in Informatics (OASIcs) 40, pp. 39 – 50, 2014.

Abstract

In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is sound for weakly left-linear normal conditional term rewriting systems (CTRS). Here, soundness for a CTRS means that reduction of the transformed unconditional term rewriting system (TRS) creates no undesired reduction for the CTRS. 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 TRS obtained by the simultaneous unraveling. Then, we use the fact that the unraveling is sound for weakly left-linear normal CTRSs.

 

  PDF |    doi:10.4230/OASIcs.WPTE.2014.39  |  © Creative Commons License – CC   BY

BibTeX 

@inproceedings{NNMYKG-WPTE14,
author = "Naoki Nishida and Makashi Yanagisawa and Karl Gmeiner",
title = "On Proving Soundness of the Computationally Equivalent
Transformation for Normal Conditional Term Rewriting Systems
by Using Unravelings",
booktitle = "Proceedings of the First International Workshop on Rewriting
Techniques for Program Transformations and Evaluation (WPTE 2014)",
editor = "Manfred Schmidt-Schau{\ss} and Masahiko Sakai and David Sabel and Yuki Chiba",
series = "OpenAccess Series in Informatics (OASIcs)",
volume = 40,
pages = "39--50",
year = 2014,
doi = "10.4230/OASIcs.WPTE.2014.39"
}
Nach oben scrollen