Transformational approaches for conditional term rewrite systems

Abstract

Termersetzung ist eine syntaktische Methode, um Ausdrücke zu Normalformen zu vereinfachen. Sie wird seit Jahrzehnten untersucht und weiterentwickelt und hat viele Anwendungen gefunden. Bedingte Termersetzung ist eine durch funktionale Programmiersprachen motivierte Erweiterung, bei der die Anwendung von Ersetzungsregeln an Bedingungen geknüpft ist. Obwohl natürlich und intuitiv, erschwert diese Erweiterung die Analyse von Termersetzungssystemen. So lassen sich etwa Kriterien für Eigenschaften wie Konfluenz und Termination nicht von konventionellen auf bedingte Termersetzungssysteme übertragen. Ein Ansatz, um diesen Komplikationen zu begegnen, sind Transformationen, die die Bedingungen eliminieren und bedingte Termersetzungssysteme in konventionelle unbedingte umwandeln. Diese Transformationen müssen korrekt (engl. "sound") sein, das heißt, es muss sichergestellt sein, dass jede Ersetzungskette im transformierten System einer solchen im ursprünglichen System entspricht. Diese Eigenschaft ist im Allgemeinen schwierig zu garantieren: Die Transformationen führen neue Strukturen und Regeln ein, um die Bedingungen zu kodieren, wodurch das transformierte System oft Auswertungen zulässt, die im ursprünglichen nicht möglich waren. In früheren Arbeiten wurde bereits gezeigt, dass Linkslinearität eine hinreichende Bedingung darstellt, um die Korrektheit von Transformationen zu garantieren. Die vorliegende Dissertation geht systematisch der Frage nach, welche anderen syntaktischen Eigenschaften dies noch tun. Wir analysieren zunächst mehrere Beispiele, die illustrieren, wie es zu Inkorrektheit kommt. Darauf aufbauend führen wir zwei unterschiedliche Methoden zum Nachweis von Korrektheit ein und zeigen mit ihrer Hilfe die Korrektheit der Transformationen für mehrere Klassen von Termersetzungssystemen. Von besonderer Bedeutung erweist sich eine Strategie namens "U-eager rewriting", mit der sich die Korrektheit für verschiedene Linearitätsbedingungen zeigen lässt. Zuletzt präsentieren wir einige Anwendungen dieser Resultate und vergleichen sie mit anderen Ansätzen.

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.