WPTE 2016 Paper

Postproceedings Version

Sound Structure-Preserving Transformation for Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems

Authors

Ryota Nakayama, Naoki Nishida, and Masahiko Sakai

State

Booktitle

In Informal Proceedings of the 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE'16), Electronic Proceedings in Theoretical Computer Science, Vol. 235, pp. 62–77, Open Publishing Association, January 2017.

Abstract

In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is a sound structure-preserving transformation for weakly-left-linear deterministic conditional term rewriting systems. More precisely, we show that every weakly-left-linear deterministic conditional term rewriting system can be converted to an equivalent weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting system and prove that the SR transformation is sound for weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting systems. Here, soundness for a conditional term rewriting system means that reduction of the transformed unconditional term rewriting system creates no undesired reduction sequence for the conditional system.

DOI

10.4204/EPTCS.235.5

Link

[EPTCS page] [full version (pdf)]

Note

Published: January 1st, 2017

Informalproceedings Version

Sound Structure-Preserving Transformation for Ultra-Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems

Authors

Ryota Nakayama, Naoki Nishida, and Masahiko Sakai

Booktitle

In Informal Proceedings of the 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE'16), pp. 77-85, Porto, Portugal, June 2016.

Abstract

A computationally equivalent transformation proposed by Serbanuta and Rosu is one of structure-preserving transformations for conditional term rewriting systems (CTRSs). The transformation has been proposed for normal CTRSs, and then has been extended to strongly or syntactically deterministic CTRSs (SDCTRSs) that are ultra-left-linear (i.e., their unraveled TRSs are left-linear). Soundness of the transformation for weakly-left-linear normal CTRSs has been proved, but the result has not been adapted to SDCTRSs yet. Here, soundness for a CTRS means that reduction of the transformed unconditional term rewriting system creates no undesired reduction for the CTRS. In this paper, we show that the transformation is a sound structure-preserving transformation for ultra-weakly-left-linear SDCTRSs. More precisely, we show that the transformation is applicable to ultra-weakly-left-linear SDCTRSs without any change, and prove that the transformation is still sound for such SDCTRSs.