# Origin functions in λ-calculus and term rewriting systems

## Abstract

We use *Origin functions* to describe the notions of descendance and residuals in reduction systems such as the λ-calculus and linear term rewriting systems. We compare the origin functions for the λ-calculus and for term rewriting systems that implement this calculus, λ*σ* and λ*Env*. We show that the notions of origin do not correspond exactly, but we describe an extension of the notion of origin that permits the correct computation of λ-calculus origins for derivations of λ*Env*. We show that this extension is not sufficient to give the same result for λ*σ* and we give another extension for that system. This work is interesting as it provides a distinction between the two term rewriting systems. This work has applications in the debugging of languages based on the λ-calculus or environments.

## Keywords

Origin Function Reduction System Critical Pair Label Function Final Term## Preview

Unable to display preview. Download preview PDF.

## References

- [ACCL90]M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, “Explicit Substitutions”,
*Proceedings of the 17th Annual Symposium on the Principles of Programming Languages*, San Francisco, California, January 1990, pp. 31–46.Google Scholar - [Bertot91a]Y. Bertot,
*Une Automatisation du Calcul des Résidus en Sémantique Naturelle*, PhD thesis, University of Nice, France, June 1991.Google Scholar - [Boudol85]G. Boudol, “Computational Semantics of Term Rewriting Systems”,
*Algebraic Methods in Semantics*, M. Nivat, J. C. Reynolds (editors), Cambridge University Press, 1985.Google Scholar - [de Bruijn72]N. de Bruijn, “Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem”, Indag. Math. 34,5, 1972, pp. 381–392.Google Scholar
- [CHL91]P.-L. Curien, T. Hardin, J.-J. Lévy, “Confluence Properties of Weak and Strong Calculi of Explicit Substitutions”, Personal communication, July 1991.Google Scholar
- [Curien86]P.-L. Curien,
*Categorical Combinators, Sequential Algorithms and Functional Programming*, Pitman, London, 1986.Google Scholar - [Curry&Feys58]
- [Field90]J. Field, “On Laziness and Optimality in Lambda Interpreters: Tools for Specification and Analysis”,
*Proceedings of the 17th ACM Symposium on Principles of Programming Languages*, San Francisco, California, January 1990, pp. 1–15.Google Scholar - [Hardin & Lévy89]T. Hardin, J.-J. Lévy, “A Confluent Calculus of Substitutions”,
*Proceedings of the France Japan Artificial Intelligence and Computer Science Symposium*, Izu, Japan, November 89.Google Scholar - [Hindley&Seldin86]J. Hindley, J. Seldin,
*Introduction to Combinators and*λ-*calculus*, London Mathematical Society Student Texts, Cambridge University Press, 1986.Google Scholar - [Huet80]G. Huet, “Confluent reductions: abstract properties and applications to term rewriting systems”, Journal of the ACM, 27, 4, pp. 797–821, 1980.Google Scholar
- [Klop80]J. W. Klop,
*Combinatory Reduction Systems*, PhD Thesis, Mathematisch Centrum Amsterdam, 1980.Google Scholar - [Knuth&Bendix70]Knuth, D. E., Bendix P. B., “Simple Word Problems in Universal Algebras”,
*Computational Problems in Abstract Algebra*, J. Leech (editor), Pergamon Press, 1970.Google Scholar - [Lévy78]J.-J. Lévy,
*Réductions Correctes et Optimales dans le Lambda Calcul*, PhD Thesis, Université de Paris VII, 1978.Google Scholar - [Maranget91]L. Maranget, “Optimal Derivations in Weak Lambda-Calculi and in Orthogonal Terms Rewriting Systems”,
*Proceeding of the 18th ACM Symposium on Principles of Programming Languages*, Orlando, Florida, January 1991, pp. 255–269.Google Scholar - [Morris68]J. Morris,
*Lambda Calculus Models of Programming Languages*, PhD Thesis, MIT, Cambridge, Massachusetts, 1968.Google Scholar - [Tolmach&Appel90]A. P. Tolmach, A. W. Appel, “Debugging Standard ML without Reverse Engineering”,
*Proceedings of the 1990 ACM Conference on Lisp and Functional Programming*, Nice, France, June 1990, pp. 1–12.Google Scholar