Bruggink, Sander:
A Proof of Finite Family Developments for Higher-Order Rewriting using a Prefix Property
In: Proceedings of the 17th International Conference of Term Rewriting and Applications, RTA 2006. - (Lecture Notes in Computer Science ; 4098) / Pfenning, Frank (Hrsg.). - Berlin: Springer, 2006, S. 372 - 386
2006Buchaufsatz/Kapitel in Sammelwerk
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
WWW URL:
http://www.ti.inf.uni-due.de/publications/bruggink/rta06.pdf
Erschienen in
Proceedings of the 17th International Conference of Term Rewriting and Applications, RTA 2006. - (Lecture Notes in Computer Science ; 4098)
Herausgeber*in:
Pfenning, Frank
Erscheinungsort:
Berlin
Verlag:
Springer
Erscheinungsjahr:
2006
in:
S. 372 - 386
ISBN
978-3-540-36834-2

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.