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.

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"
}