License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WPTE.2014.39
URN: urn:nbn:de:0030-drops-45850
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4585/
Go to the corresponding OASIcs Volume Portal

Nishida, Naoki ; Yanagisawa, Makishi ; Gmeiner, Karl

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

pdf-format:
p039-05-nishida.pdf (0.5 MB)

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 - Entry

@InProceedings{nishida_et_al:OASIcs:2014:4585,
  author =	{Naoki Nishida and Makishi Yanagisawa and Karl Gmeiner},
  title =	{{On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  pages =	{39--50},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Manfred Schmidt-Schau{\ss} and Masahiko Sakai and David Sabel and Yuki  Chiba},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4585},
  URN =		{urn:nbn:de:0030-drops-45850},
  doi =		{10.4230/OASIcs.WPTE.2014.39},
  annote =	{Keywords: conditional term rewriting, unraveling, condition elimination}
}

Keywords: conditional term rewriting, unraveling, condition elimination
Collection: First International Workshop on Rewriting Techniques for Program Transformations and Evaluation
Issue Date: 2014
Date of publication: 13.07.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI