[Back]

F. Schernhammer:
"On Context-Sensitive Term Rewriting";
Supervisor: B. Gramlich; Institut für Computersprachen / AB Theoretische Informatik und Logik, 2007; final examination: 2007-02-08.

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 \emph{context-sensitive rewriting} a replacement map specifies for every function symbol those argument positions where a rewrite step may take place. In \emph{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 \emph{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 \emph{forbidden patterns}.

Term rewriting, termination, confluence, functional-logic programming, context-sensitivity.