2026-08-16T05:35:31Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4585 2024-03-06T10:29:34Z ddc:004 open_access

On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings Nishida, Naoki Yanagisawa, Makishi Gmeiner, Karl conditional term rewriting unraveling condition elimination 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Naoki Nishida and Makishi Yanagisawa and Karl Gmeiner 2014 Is Part Of OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.WPTE.2014.39 urn:nbn:de:0030-drops-45850 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.39 eng https://creativecommons.org/licenses/by/3.0/legalcode