A Proof of Finite Family Developments for Higher-Order Rewriting using a Prefix Property
Utrecht: Utrecht University, 2006
(Technical Report ; 245)
2006Buch
Informatik
Titel:
A Proof of Finite Family Developments for Higher-Order Rewriting using a Prefix Property
Autor*in:
Bruggink, SanderUDE
- LSF ID
- 47885
- Sonstiges
- der Hochschule zugeordnete*r Autor*in
Erscheinungsort:
Utrecht
Verlag:
Utrecht University
Erscheinungsjahr:
2006
Umfang:
23
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 $\lambda$-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.