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

## Reference

H.J. Sander Bruggink.

A proof of finite family developments for higher-order rewriting using a prefix property. InProceedings of RTA '06. Springer, 2006.

## Abstract

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:

@

inproceedings{bruggink:ffd2006,

author= {H.J. Sander Bruggink},

booktitle= {Proceedings of RTA '06},

publisher= {Springer},

title= {A Proof of Finite Family Developments for Higher-Order Rewriting using a Prefix Property},

year= {2006}

}

PDF (192 kB)Tech report version