Descendants and origins in term rewriting

Inge Bethke
Jan Willem Klop
Roel de Vrijer


Abstract

In this paper we treat various aspects of the notion that is central
in term rewriting, namely that of descendants or residuals.
We address both first order term rewriting and lambda calculus.
For both we consider also infinitary rewriting. A recurrent theme
is the Parallel Moves Lemma. Next to the classical notion of descendant,
we introduce an extended version that recently found several
applications as `origin tracking'. This device is employed to give three new
proofs of classical theorems: the Genericity Lemma in lambda calculus,
the theorem of Huet and L\'evy on needed reductions in first order
term rewriting, and Berry's Sequentiality Theorem in (infinitary) 
lambda calculus.


Contents

1.  Introduction
2.  Early views on descendants
3.  Preliminaries
4.  Descendants in lambda-beta calculus
5.  Descendants in lambda-beta-eta calculus
6.  L\'evy's labeled lambda calculus
7.  Origin tracking in lambda calculus
8.  Origin tracking in first-order rewriting
9.  First-order infinitary rewriting
10. Infinitary lambda calculus
11. Origin tracking in infinitary lambda calculus
12. Recent views on descendants

Appendix A: Abstract reduction systems
Appendix B: Transitivity of the descendant relation
Appendix C: Collapsing reductions
Appendix D: Failure of FD for lambda residuals
Appendix E: Parallel reduction  \`a la Aczel