Efficient rewriting techniques

M.J. Weerdenburg, van

    Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)

    71 Downloads (Pure)


    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.
    Original languageEnglish
    QualificationDoctor of Philosophy
    Awarding Institution
    • Mathematics and Computer Science
    • Groote, Jan Friso, Promotor
    • van den Brand, Mark G.J., Promotor
    • Reniers, Michel A., Copromotor
    Award date1 Apr 2009
    Place of PublicationEindhoven
    Print ISBNs978-90-386-1671-1
    Publication statusPublished - 2009


    Dive into the research topics of 'Efficient rewriting techniques'. Together they form a unique fingerprint.

    Cite this