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

TL;DR

This paper proves that the SR transformation is a sound, structure-preserving method for converting weakly-left-linear deterministic conditional term rewriting systems into equivalent forms, ensuring no undesired reductions occur.

Contribution

It establishes the soundness of the SR transformation specifically for weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting systems.

Findings

SR transformation is sound for the specified systems.

Every such system can be converted to an equivalent form.

The transformation preserves the reduction properties without introducing undesired behaviors.

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.