A Proof of Finite Family Developments for Higher-Order Rewriting ...


H.J. Sander Bruggink. A proof of finite family developments for higher-order rewriting using a prefix property. Technical Report 245, Utrecht University, 2006.


A prefix property is the property that, given a reduction, the ancestor of a prefix of the target is a prefix of the source of the reduction. In this paper we prove a prefix property for the class of Higher-order Rewrite Systems with pattern (HRSs), by reducing it to a similar property of a -calculus with explicit substitutions. This prefix property is then used to prove that Higher-order Rewrite Systems enjoy Finite Family Developments. This property states that reductions in which the creation depth of the redexes is bounded are finite, and is a useful tool to prove various properties of HRSs.

Suggested BibTeX entry:

    author = {H.J. Sander Bruggink},
    institution = {Utrecht University},
    number = {245},
    series = {Logic Group Preprint Series},
    title = {A Proof of Finite Family Developments for Higher-Order Rewriting using a Prefix Property},
    year = {2006}

PDF (256 kB)Conference version
© University of Duisburg-Essen, Theoretical Computer Science group