Paths, computations and labels in the λ-calculus
We provide a new characterization of Lévy's redex-families in the λ-calculus  as suitable paths in the initial term of the derivation. The idea is that redexes in a same family are created by “contraction” (via β-reduction) of a unique common path in the initial term. This fact gives new evidence about the “common nature” of redexes in a same family, and about the possibility of sharing their reduction. From this point of view, our characterization underlies all recent works on optimal graph reduction techniques for the λ-calculus [9,6,7,1], providing an original and intuitive understanding of optimal implementations.
As an easy by-product, we prove that neither overlining nor underlining are required in Lévy's labelling.
KeywordsAtomic Label Initial Term Return Path Optimal Reduction Optimal Implementation
Unable to display preview. Download preview PDF.
- A. Asperti. Linear logic, comonads, and optimal reductions. Draft, INRIA-Rocquencourt, 1991.Google Scholar
- A. Asperti and C. Laneve. Interaction systems 1: The theory of optimal reductions. Technical Report 1748, INRIA-Rocquencourt, September 1992.Google Scholar
- A. Asperti and C. Laneve. Optimal reductions in interaction systems. In TapSoft '93, Lecture Notes in Computer Science. Springer-Verlag, 1993.Google Scholar
- V. Danos and L. Regnier. Local and asynchronous beta-reduction. In Proceedings 8th Annual Symposium on Logic in Com puter Science, Montreal, 1993.Google Scholar
- J. Field. On laziness and optimality in lambda interpreters: tools for specification and analysis. In Proceedings 17th ACM Symposium on Principles of Programmining Languages, pages 1–15, 1990.Google Scholar
- G. Gonthier, M. Abadi, and J.J. Lévy. The geometry of optimal lambda reduction. In Proceedings 19th ACM Symposium on Principles of Programmining Languages, pages 15–26, 1992.Google Scholar
- G. Gonthier, M. Abadi, and J.J. Lévy. Linear logic without boxes. In Proceedings 7th Annual Symposium on Logic in Computer Science, 1992.Google Scholar
- Y. Lafont. Interaction nets. In Proceedings 17th ACM Symposium on Principles of Programmining Languages, pages 95–08, 1990.Google Scholar
- J. Lamping. An algorithm for optimal lambda calculus reductions. In Proceedings 17th ACM Symposium on Principles of Programmining Languages, pages 16–30, 1990.Google Scholar
- C. Laneve. Optimality and Concurrency in Interaction Systems. PhD thesis, Technical Report TD-8/93, Dip. Informatica, Università di Pisa, March 1993.Google Scholar
- J.J. Lévy. Réductions correctes et optimales dans le lambda calcul. PhD thesis, Université Paris VII, 1978.Google Scholar
- J.J. Lévy. Optimal reductions in the lambda-calculus. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 159–191. Academic Press, 1980.Google Scholar
- L. Regnier. Lambda Calcul et Reseaux. Thèse de doctorat, Université Paris VII. 1992.Google Scholar