Descendants and origins in term rewriting.

I. Bethke, J.W. Klop, R.C. de Vrijer

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

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.
Original languageEnglish
Pages (from-to)59-124
JournalInformation and Computation
Volume159
DOIs
Publication statusPublished - 2000

Fingerprint

Dive into the research topics of 'Descendants and origins in term rewriting.'. Together they form a unique fingerprint.

Cite this