Origin functions in λ-calculus and term rewriting systems

  • Yves Bertot
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 581)


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.


Origin Function Reduction System Critical Pair Label Function Final Term 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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
  2. [Bertot91a]
    Y. Bertot, Une Automatisation du Calcul des Résidus en Sémantique Naturelle, PhD thesis, University of Nice, France, June 1991.Google Scholar
  3. [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
  4. [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
  5. [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
  6. [Curien86]
    P.-L. Curien, Categorical Combinators, Sequential Algorithms and Functional Programming, Pitman, London, 1986.Google Scholar
  7. [Curry&Feys58]
    H. Curry, R. Feys, Combinatory Logic, Vol. I, North-Holland, 1958.Google Scholar
  8. [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
  9. [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
  10. [Hindley&Seldin86]
    J. Hindley, J. Seldin, Introduction to Combinators and λ-calculus, London Mathematical Society Student Texts, Cambridge University Press, 1986.Google Scholar
  11. [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
  12. [Klop80]
    J. W. Klop, Combinatory Reduction Systems, PhD Thesis, Mathematisch Centrum Amsterdam, 1980.Google Scholar
  13. [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
  14. [Lévy78]
    J.-J. Lévy, Réductions Correctes et Optimales dans le Lambda Calcul, PhD Thesis, Université de Paris VII, 1978.Google Scholar
  15. [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
  16. [Morris68]
    J. Morris, Lambda Calculus Models of Programming Languages, PhD Thesis, MIT, Cambridge, Massachusetts, 1968.Google Scholar
  17. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Yves Bertot
    • 1
  1. 1.INRIA Sophia-AntipolisBulgaria

Personalised recommendations