Abstract
The existing call-by-need λ describe lazy evaluation via equational logics. A programmer can use these logics to safely ascertain whether one term is behaviorally equivalent to another or to determine the value of a lazy program. However, neither of the existing calculi models evaluation in a way that matches lazy implementations.
Both calculi suffer from the same two problems. First, the calculi never discard function calls, even after they are completely resolved. Second, the calculi include re-association axioms even though these axioms are merely administrative steps with no counterpart in any implementation.
In this paper, we present an alternative axiomatization of lazy evaluation using a single axiom. It eliminates both the function call retention problem and the extraneous re-association axioms. Our axiom uses a grammar of contexts to describe the exact notion of a needed computation. Like its predecessors, our new calculus satisfies consistency and standardization properties and is thus suitable for reasoning about behavioral equivalence. In addition, we establish a correspondence between our semantics and Launchbury’s natural semantics.
Keywords
References
Ariola, Z., Blom, S.: Cyclic Lambda Calculi. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 77–106. Springer, Heidelberg (1997)
Ariola, Z.M., Felleisen, M.: The call-by-need lambda-calculus. Tech. Rep. CIS-TR-94-23, University of Oregon (1994)
Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program. 7, 265–301 (1997)
Ariola, Z.M., Maraist, J., Odersky, M., Felleisen, M., Wadler, P.: A call-by-need lambda calculus. In: Proc. 22nd Symp. on Principles of Programming Languages, pp. 233–246 (1995)
Barendregt, H.P.: Lambda Calculus, Syntax and Semantics. North-Holland (1985)
Church, A.: The Calculi of Lambda Conversion. Princeton University Press (1941)
Curry, H.B., Feys, R.: Combinatory Logic, vol. I. North-Holland (1958)
Danvy, O., Millikin, K., Munk, J., Zerny, I.: Defunctionalized Interpreters for Call-by-Need Evaluation. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 240–256. Springer, Heidelberg (2010)
Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. MIT Press (2009)
Felleisen, M., Friedman, D.P.: A syntactic theory of sequential state. Theor. Comput. Sci. 69(3), 243–287 (1989)
Friedman, D.P., Ghuloum, A., Siek, J.G., Winebarger, O.L.: Improving the lazy Krivine machine. Higher Order Symbolic Computation 20, 271–293 (2007)
Friedman, D.P., Wise, D.S.: Cons should not evaluate its arguments. In: Proc. 3rd Intl. Colloq. on Automata, Languages and Programming. pp. 256–284 (1976)
Garcia, R., Lumsdaine, A., Sabry, A.: Lazy evaluation and delimited control. In: Proc. 36th Symp. on Principles of Programming Languages, pp. 153–164 (2009)
Henderson, P., Morris Jr., J.H.: A lazy evaluator. In: Proc. 3rd Symp. on Principles of Programming Languages, pp. 95–103 (1976)
Josephs, M.B.: The semantics of lazy functional languages. Theor. Comput. Sci. 68(1) (1989)
Landin, P.J.: The next 700 programming languages. Comm. ACM 9, 157–166 (1966)
Launchbury, J.: A natural semantics for lazy evaluation. In: Proc. 20th Symp. on Principles of Programming Languages, pp. 144–154 (1993)
Loader, R.: Notes on simply typed lambda calculus. Tech. Rep. ECS-LFCS-98-381, Department of Computer Science, University of Edinburgh (1998)
Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name call-by-value, call-by-need, and the linear lambda calculus. In: Proc. 11th Conference on Mathematical Foundations of Programminng Semantics, pp. 370–392 (1995)
Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus (unabridged). Tech. Rep. 28/94, Universität Karlsruhe (1994)
Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. J. Funct. Program. 8, 275–317 (1998)
Morris, J.H.: Lambda Calculus Models of Programming Languages. Ph.D. thesis, MIT (1968)
Nakata, K., Hasegawa, M.: Small-step and big-step semantics for call-by-need. J. Funct. Program. 19(6), 699–722 (2009)
Peyton Jones, S.L., Salkild, J.: The spineless tagless g-machine. In: Proc. 4th Conf. on Functional Programming Lang. and Computer Architecture, pp. 184–201 (1989)
Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1, 125–159 (1975)
Purushothaman, S., Seaman, J.: An adequate operational semantics for sharing in lazy evaluation. In: Proc. 4th European Symp. on Program, pp. 435–450 (1992)
Sestoft, P.: Deriving a lazy abstract machine. J. Func. Program. 7(3), 231–264 (1997)
Wadsworth, C.P.: Semantics and Pragmatics of the Lambda Calculus. Ph.D. thesis, Oxford University (1971)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chang, S., Felleisen, M. (2012). The Call-by-Need Lambda Calculus, Revisited. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)