Paths, computations and labels in the λ-calculus

  • Andrea Asperti
  • Cosimo Laneve
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 690)

Abstract

We provide a new characterization of Lévy's redex-families in the λ-calculus [11] 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.

Keywords

Prefix Suffix Imide 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    A. Asperti. Linear logic, comonads, and optimal reductions. Draft, INRIA-Rocquencourt, 1991.Google Scholar
  2. [2]
    A. Asperti and C. Laneve. Interaction systems 1: The theory of optimal reductions. Technical Report 1748, INRIA-Rocquencourt, September 1992.Google Scholar
  3. [3]
    A. Asperti and C. Laneve. Optimal reductions in interaction systems. In TapSoft '93, Lecture Notes in Computer Science. Springer-Verlag, 1993.Google Scholar
  4. [4]
    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
  5. [5]
    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
  6. [6]
    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
  7. [7]
    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
  8. [8]
    Y. Lafont. Interaction nets. In Proceedings 17th ACM Symposium on Principles of Programmining Languages, pages 95–08, 1990.Google Scholar
  9. [9]
    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
  10. [10]
    C. Laneve. Optimality and Concurrency in Interaction Systems. PhD thesis, Technical Report TD-8/93, Dip. Informatica, Università di Pisa, March 1993.Google Scholar
  11. [11]
    J.J. Lévy. Réductions correctes et optimales dans le lambda calcul. PhD thesis, Université Paris VII, 1978.Google Scholar
  12. [12]
    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
  13. [13]
    L. Regnier. Lambda Calcul et Reseaux. Thèse de doctorat, Université Paris VII. 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Andrea Asperti
    • 1
  • Cosimo Laneve
    • 2
  1. 1.Dip. di MatematicaBolognaItaly
  2. 2.INRIA Sophia-AntipolisItaly

Personalised recommendations