Hostname: page-component-74656f9884-2dmjx Total loading time: 0 Render date: 2026-11-10T08:21:59.595Z Has data issue: false hasContentIssue false
  • English
  • Français

Redexes are stable in the λ-calculus

Published online by Cambridge University Press:  15 July 2015

JEAN-JACQUES LÉVY
JEAN-JACQUES LÉVY*
Affiliation:
INRIA, Campus de l'École polytechnique, 91120 Palaiseau, France Email: jean-jacques.levy@inria.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

In the theory of sequential programming languages, Berry's stability property is an important step claiming that values have unique origins in their calculations. It has been shown that Bohm trees are stable in the λ-calculus, meaning that there is a unique minimum prefix of any lambda term which computes its Bohm tree. Moreover this property is also true for finite prefixes of Bohm trees. The proof relies on Curry's standardization theorem as initially pointed out by Plotkin in his famous article LCF considered as a programming language. In this paper we will show that the stability property also holds for redexes. Namely for any redex family, there is a unique minimum calculation and a unique redex which computes this family. This property was already known in the study of optimal reductions, but we stress here on stability and want to show that stability is inside the basic objects of calculations. The proof will be based on nice commutations between residuals and creations of new redexes. Our tool for proving this property will be the labelled lambda calculus used in the study of optimal reductions.

References

Abadi, M., Lampson, B. and Lévy, J.-J. (1996). Analysis and caching of dependencies. In: Proceedings of the 1996 ACM International Conference on Functional Programming 83–91.Google Scholar
Abramsky, S., Jagadeesan, R. and Malacaria, P. (2000). Full abstraction for PCF. Information and Computation 167 409–470.CrossRefGoogle Scholar
Amadio, R. and Curien, P.-L. (1998). Domains and Lambda-calculi, Cambridge University Press. ISBN 0-521-62277-8.Google Scholar
Asperti, A. and Laneve, C. (1995). Paths, computations and labels in the lambda-calculus. Theoretical Computer Science 142 (2) 272–288.CrossRefGoogle Scholar
Barendregt, H. (1977). The type free Lambda calculus. In: Barwise, J. (ed.) Handbook of Mathematical Logic, North-Holland. ISBN 0-7204-2285-X.Google Scholar
Barendregt, H. (1984). The Lambda Calculus, Its Syntax and Semantics, North-Holland. ISBN-13: 978-0-444-87508-2.Google Scholar
Berry, G. (1978). Modèles stables du lambda-calcul. PhD thesis, University of Paris 7.Google Scholar
Berry, G. and Curien, P.-L. (1982). Sequential algorithms on concrete data structures. Theoretical Computer Science 20 265–321.Google Scholar
Berry, G. and Curien, P.-L. (1985). Theory and practice of sequential algorithms: The Kernel of the programming language CDS. In: Nivat, M. and Reynolds, J.C. (eds.) Algebraic Methods in Semantics, Cambridge University Press.Google Scholar
Berry, G. and Lévy, J.-J. (1979). Minimal and optimal computations of recursive programs. JACM 26 (1) 148–175.CrossRefGoogle Scholar
Boudol, G. (1985). Computational semantics of term rewriting systems. In: Nivat, M. and Reynolds, J.C. (eds.) Algebraic Methods in Semantics, Cambridge University Press.Google Scholar
Cadiou, J.-M. (1972). Recursive Definitions of Partial Functions and Their Computations. PhD thesis, Stanford University.CrossRefGoogle Scholar
Church, A. (1941). The Calculi of Lambda-Conversion, Princeton University Press – Oxford University Press.Google Scholar
Curry, H. and Feys, R. (1958). Combinatory Logic, volume 1, North-Holland.Google Scholar
Curry, H., Feys, R. and Seldin, J. (1972). Combinatory Logic, volume 2, North-Holland.Google Scholar
Hindley, R. (1997). Basic Simple Type Theory, Cambridge University Press.Google Scholar
Huet, G. and Lévy, J.-J. (1991). Computations in orthogonal rewriting systems I and II. In: Lassez, J.-L. and Plotkin, G. (eds.) Computational Logic; Essays in Honor of Alan Robinson, The MIT Press 395–443.Google Scholar
Klop, J.-W. (1980). Combinatory Reduction Systems, PhD thesis, Mathematical Centre Tracts 127, CWI, Amsterdam.Google Scholar
Laneve, C. (1994). Distributive evaluations of lambda-calculus. Fundamenta Informaticae 20 (4) 333–352.Google Scholar
Lévy, J.-J. (1975). An algebraic interpretation of the λβ-calculus and a labeled λ-calculus. In: Böhm, C. (ed.) Lambda-Calculus and Computer Science Theory. Springer Lecture Notes in Computer Science 37 147–165.CrossRefGoogle Scholar
Lévy, J.-J. (1978). Réductions correctes et optimales dans le lambda calcul. PhD thesis, University of Paris 7.Google Scholar
Lévy, J.-J. (1980). Optimal reductions in the lambda-calculus. In: Hindley, J.R. and Seldin, J.P. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press 159–191.Google Scholar
Lévy, J.-J. (2009). Generalized Finite developments. In: Bertot, Y., Huet, G., Lévy, J.-J. and Plotkin, G. (eds.) From Semantics to Computer Science: Essays in Honour of Gilles Kahn, Cambridge University Press 185–204.CrossRefGoogle Scholar
Maranget, L. (1992). La stratégie paresseuse. PhD thesis, University of Paris 7.Google Scholar
Melliès, P.-A. (1997). A factorisation theorem in rewriting theory. In: Proceedings of the 7th Conference on Category Theory and Computer Science. Springer Lecture Notes in Computer Science 1290 49–68, Santa Margherita Ligure.Google Scholar
Plotkin, G. (1977). LCF considered as a programming language. Theoretical Computer Science 5 223–255.CrossRefGoogle Scholar
van Oostrom, V. and de Vrijer, R. (2002). Four equivalent equivalences of reductions. In: WRS'02. Electronic Notes in Theoretical Computer Science 70 (6).Google Scholar
van Oostrom, V. and de Vrijer, R. (2003). Equivalence of reductions. In: Bezem, M., Klop, J.W. and de Vrijer, R. (eds.) Terese, Term Rewriting Systems, Cambridge University Press.Google Scholar
Vuillemin, J. (1973). Proof Techniques for Recursive Programs, PhD thesis, Stanford University.Google Scholar
Winskel, G. (1983). Event structure semantics for CCS and related languages. Technical report, DAIMI – Aarhus University.Google Scholar