Abstract

Term rewriting is a purely syntactical method to replace subterms of a term by other terms. This way, terms can be simplified until they are in normalform. Such syntactical replacements are used in many areas, for theoretical and practical purposes. Term rewriting therefore has been investigated in research for a long time and its theory is well-understood.
There are many extensions of term rewriting. One of them, conditional term rewriting comes up in many applications like for instance functional programming. Although adding conditions is an intuitive and natural approach, it makes such systems much harder to analyze. Many properties change their intuitive meaning and many criteria for properties of rewriting (like confluence or termination) do not hold anymore.
Transformations have been developed to eliminate the conditions in such conditional term rewrite systems in order to use criteria and properties of unconditional rewriting and adapt them for conditional rewriting. This approach has been used successfully for theoretical and practical purposes, yet it comes with a price.
A rewrite sequence in the transformed system should correspond to a rewrite sequence in the original system. This property is called soundness. Without soundness, the analysis of transformed systems leads to results that differ from those of the original system.
The reason why we do not obtain soundness in general is as follows: A transformation introduces some framework to encode conditions. Because of this encoding, transformed systems might give rise to different evaluation paths than the original system.
Counterexamples for soundness are usually syntactically very complex. It turns out that many of these syntactical properties are crucial for unsoundness. [14] already proves that for a certain class of conditional term rewrite systems left-linearity is a sufficient criterion to obtain soundness.
This thesis mainly deals with the question for which other syntactical properties we obtain soundness. For this purpose we present several examples that illustrate and explain in detail why we obtain unsoundness.
We then provide two different proof ideas for soundness properties. Using this approach we prove soundness for some syntactical properties, yet since these results have strong preconditions these property might be of limited use.
In the second proof approach we prove soundness for a strategy that we call U-eager rewriting. We then show how complex rewrite sequences can be transformed into such U-eager rewrite sequences. Using this approach we will prove soundness for certain linearity conditions.
Finally we will present some applications of soundness results, discuss differences of soundness properties for different transformations and provide a detailed overview of results in this thesis.

BibTeX

@phdthesis{KG14,
  author    = "Karl Gmeiner",
  title     = "Transformational Approaches for Conditional Term Rewrite
               Systems",
  school    = "Vienna PhD School of Informatics",
  year      = 2014
}