Efficient rewriting techniques

M.J. Weerdenburg, van

    Onderzoeksoutput: ScriptieDissertatie 1 (Onderzoek TU/e / Promotie TU/e)

    75 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.
    Originele taal-2Engels
    KwalificatieDoctor in de Filosofie
    Toekennende instantie
    • Mathematics and Computer Science
    • Groote, Jan Friso, Promotor
    • van den Brand, Mark G.J., Promotor
    • Reniers, Michel A., Co-Promotor
    Datum van toekenning1 apr 2009
    Plaats van publicatieEindhoven
    Gedrukte ISBN's978-90-386-1671-1
    StatusGepubliceerd - 2009


    Duik in de onderzoeksthema's van 'Efficient rewriting techniques'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit