| Descendants and Origins in Term Rewriting (2007) | |||||||||||||||||
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'evy on needed reductions in first order term rewriting, and Berry's Sequentiality Theorem in (infinitary) -calculus. Note: This article is based on a lecture given by Jan Willem Klop at RTA '98 held in Tsukuba, Japan. Contents 1 Introduction 2 2 Early views on descendants 3 3 Preliminaries 5 3.1 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Reduction . . . . . . . . . . . . . . . . . . . . . .... | |||||||||||||||||
Details der Publikation | |||||||||||||||||
| |||||||||||||||||