TY - JOUR
T1 - Descendants and origins in term rewriting.
AU - Bethke, I.
AU - Klop, J.W.
AU - de Vrijer, R.C.
PY - 2000
Y1 - 2000
N2 - In this paper we treat various aspects of a notion that is central in term rewriting, namely that of descendants or residuals. We address both first- order term rewriting and λ-calculus, their finitary as well as their infinitary variants. A recurrent theme is the parallel moves lemma. Next to the classical notion of descendant, we introduce an extended version, known as origin tracking. Origin tracking has many applications. Here it is employed to give new proofs of three classical theorems: the genericity lemma in λ-calculus, the theorem of Huet and Lévy on needed reductions in first- order term rewriting, and Berry's sequentiality theorem in (infinitary) λ-calculus. © 2000 Academic Press.
AB - In this paper we treat various aspects of a notion that is central in term rewriting, namely that of descendants or residuals. We address both first- order term rewriting and λ-calculus, their finitary as well as their infinitary variants. A recurrent theme is the parallel moves lemma. Next to the classical notion of descendant, we introduce an extended version, known as origin tracking. Origin tracking has many applications. Here it is employed to give new proofs of three classical theorems: the genericity lemma in λ-calculus, the theorem of Huet and Lévy on needed reductions in first- order term rewriting, and Berry's sequentiality theorem in (infinitary) λ-calculus. © 2000 Academic Press.
U2 - 10.1006/inco.2000.2876
DO - 10.1006/inco.2000.2876
M3 - Article
SN - 0890-5401
VL - 159
SP - 59
EP - 124
JO - Information and Computation
JF - Information and Computation
ER -