Efficient rewriting techniques

This thesis considers three aspects of the (efficient) implementation of term rewrite systems. For efficient matching of terms against rules we introduce a formal notion of match trees. These match trees can be used to simultaneously match a term against multiple rewrite rules. The second aspect is that of temporary-term construction. After each application of a rewrite rule, a new (often temporary) term is constructed. In order to make rewriting as efficient as possible, it is shown how to annotate these temporary terms such that the information about which (sub)terms are already rewritten to normal form is preserved. This allows strategies to be written such that these subterms, known to be in normal form, will not be considered a second time. To avoid needless construction of temporary terms, it is also shown how to determine what subterms will be rewritten later on for sure, allowing for immediate rewriting of such terms. Finally, the notion of strategy trees is introduced. These strategy trees allow for a flexible specification of lazy rewrite strategies. Conditions are given for strategy trees that guarantee that rewriting a term results in a normal form of that term. Also, a method is given to automatically generate strategy trees that satisfy these conditions