On context-sensitive term rewriting

Abstract

Termersetzungssysteme bilden die formale Basis für funktionale und funktional-logische Programmiersprachen. Unglücklicherweise hängen die Effizienz und das Terminierungsverhalten von Reduktionen, die durch Termersetzungssysteme induziert werden, in hohem Maße von der verwendeten Evaluierungsstrategie ab, bei deren Wahl oft ein Kompromiss zwischen Effizienz und gutem Terminierungsverhalten getroffen werden muss. Mit Hilfe von Einschränkungen der Termersetzungsrelation kann dieses Problem teilweise gelöst werden. In dieser Arbeit werden drei Formalismen vorgestellt, die solche Einschränkungen vornehmen: Beim sogenannten Context-Sensitive Rewriting gibt die Replacement Map für jedes Funktionssymbol an welche Argumente reduziert werden sollen und welche nicht. Im Lazy Rewriting dürfen Argumente von Funktionen nur dann ausgewertet werden, wenn ihre Auswertung für das Berechnen der Funktion unbedingt notwendig ist. Beim Rewriting with Strategy Annotations wird für jede Funktion eine Reihenfolge festgelegt, mit der ihre Argumente evaluiert werden. Ziel dieser Arbeit ist es einen Überblick und Vergleich bestehender Ansätze zu geben, und weitere Anwedungsgebiete der Termersetzung mit Einschränkungen zu untersuchen (z. B. Einschränkungen der Relationen, die durch bedingte Termersetzungssysteme erzeugt werden). Die wichtigsten Resultate dieser Arbeit sind Kriterien für die Terminierung von "lazy" Termersetzungssystemen und für "Quasi-Reductivity" von deterministischen konditionalen Systemen.<br />Außerdem wird ein neuer Ansatz von Kontexteinschränkungen definitert, der mit verbotenen Patterns arbeitet.<br />

Term Rewriting provides a suitable computational model for functional and functional-logic programming languages. One major drawback, however, is that in many cases efficiency and termination of evaluations highly depend on an adequate rewrite strategy. One way to overcome this problem is to restrict the rewrite relation by using context information. In this thesis we will study three models that follow this approach: In context-sensitive rewriting a replacement map specifies for every function symbol those argument positions where a rewrite step may take place. In lazy rewriting we define for each function symbol lazy argument positions. Subterms on these positions may only be reduced if the reduction can possibly improve the matching of a superterm with some rule. The third model is called rewriting with strategy annotations. Here, for every function symbol a list is given that specifies which argument positions should be evaluated and in which order this should be done. The aim of this work is to give a survey and comparison of these techniques, as well as to consider extensions (e.g. conditional context-sensitive rewriting) and alternative approaches. In particular, the contributions of this thesis are the definition of a criterion for termination of lazy rewrite systems, an improved criterion for quasi-reductivity of deterministic conditional term rewriting systems, and the definition of an entirely new form of context restrictions using forbidden patterns.