A call-by-need lambda calculus

ABSTRACT

The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their evaluator in terms of source level syntax, and they cannot easily compare distinct implementations of different lazy strategies. In this paper we derive an equational characterization of call-by-need and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than the lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g., the call-by-need continuation passing transformation and the realization of sharing via assignments.

REFERENCES

• 1: M. Abadi, L. Cardelli, P.-L. Curien, and :}.-J. L@vy. Explicit substitutions. Journal of Functional Programming, 4(1), 1991.
• 2: S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Declarative Programming. Addison-Wesley, 1990.
• 3: Zena M. Ariola , Arvind, Properties of a first-order functional language with sharing, Theoretical Computer Science, v.146 n.1-2, p.69-108, July 24, 1995 [doi>10.1016/0304-3975(94)00185-L]
• 4: Z. M. Ariola and M. Felleisen. The call-by-need lambda calculus. Technical Report CIS-TR-94- 23, Department of computer science, University of Oregon, October 1994.
• 5: Z. M. Ariola and J. W. KIop. Cyclic lambda graph rewriting. In Proc. of #he Eighth IEEE Symposium on Logic in Computer Science, Paris, 1994.
• 6: Z. M. Ariola and J. W. Klop. Equational term graph rewriting. Acta Informahca, 1994.
• 7: Arvind, V. Kathail, and K. Pingali. Sharing of computation in functional language implementations. In Proc. International Workshop on High- Level Computer Architecture, 1984.
• 8: H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1984.
• 9: E. Crank. Parameter-passing and the lambda calculus. Master's thesis, Rice University, 1990.
• 10: Erik Crank , Matthias Felleisen, Parameter-passing and the lambda calculus, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.233-244, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99616]
• 11: M. Felleisen and D. P. Friedman. Control operators, the SECD-machine, and the lambda-calculus. in 3rd Working Conference on the Formal Description of Programming Concepts, Ebberup, Denmark, August 1986.
• 12: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 13: John Field, On laziness and optimality in lambda interpreters: tools for specification and analysis, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-15, December 1989, San Francisco, California, United States [doi>10.1145/96709.96710]
• 14: D. P. Friedman and D. S. Wise. Cons should not evaluate its arguments, in Proc. Internatzonal Conference on Automata, Languages and Programming, 1976.
• 15: Georges Gonthier , Martín Abadi , Jean-Jacques Lévy, The geometry of optimal lambda reduction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.15-26, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143172]
• 16: V. K. Kathail. Optimal Interpreters for Lambdacalculus Based Funtional Languages. PhD thesis, Dept. of Electrical Engineering and Computer Science, MIT, 1990.
• 17: John Lamping, An algorithm for optimal lambda calculus reduction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.16-30, December 1989, San Francisco, California, United States [doi>10.1145/96709.96711]
• 18: John Launchbury, A natural semantics for lazy evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.144-154, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158618]
• 19: J. Maraist, M. Odersky, and P. Wadler. The callby-need lambda calculus (unabridged). Technical Report 28/94, Universit#it Karlsruhe, Fakult#t fiir informatik, October 1994.
• 20: Luc Maranget, Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.255-269, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99618]
• 21: Ian A. Mason , Carolyn L. Talcott, Reasoning About Programs with Effects, Proceedings of the 2nd International Workshop on Programming Language Implementation and Logic Programming, p.189-203, August 20-22, 1990
• 22: I. A. Mason and C. L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(2), 1991.
• 23: G. Morrisett, M. Felleisen, and R. Harper. Modeling memory management. Technical report, Departement of computer science, Carnegie Mellon University, forthcoming 1994.
• 24: Chris Okasaki , Peter Lee , David Tarditi, Call-by-need and continuation-passing style, Lisp and Symbolic Computation, v.7 n.1, p.57-82, Jan. 1994 [doi>10.1007/BF01019945]
• 25: Simon L. Peyton Jones , David Lester, A modular fully-lazy lambda lifter in HASKELL, Software—Practice & Experience, v.21 n.5, p.479-506, May 1991 [doi>10.1002/spe.4380210505]
• 26: G. D. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, I, 1975.
• 27: S. Purushothaman , Jill Seaman, An adequate operational semantics of sharing in lazy evaluation, Symposium proceedings on 4th European symposium on programming, p.435-450, January 1992, Rennes, France
• 28: Kristoffer Høgsbro Rose, Explicit Cyclic Substitutions, Proceedings of the Third International Workshop on Conditional Term Rewriting Systems, p.36-50, July 08-10, 1992
• 29: Jill M. Seaman, An operational semantics of lazy evaluation for analysis, Pennsylvania State University, University Park, PA, 1993
• 30: C. Wadsworth. Semaniics And Pragmatics Of The Lambda-Calculus. PhD thesis, University of Oxford, September 1971.
• 31: Nobuko Yoshida, Optimal reduction in weak-&lgr;-calculus with shared environments, Proceedings of the conference on Functional programming languages and computer architecture, p.243-252, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165217]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs

General Terms:
Algorithms, Theory, Verification