Lazy evaluation and delimited control

ABSTRACT

The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics.

By a series of reasoning steps, we systematically unpack the standard-order reduction relation of the calculus and discover a novel abstract machine definition which, like the calculus, goes "under lambdas." We prove that machine evaluation is equivalent to standard-order evaluation.

Unlike traditional abstract machines, delimited control plays a significant role in the machine's behavior. In particular, the machine replaces the manipulation of a heap using store-based effects with disciplined management of the evaluation stack using control-based effects. In short, state is replaced with control.

To further articulate this observation, we present a simulation of call-by-need in a call-by-value language using delimited control operations.

REFERENCES

• 1: Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming, 1 (4): 375--416, 1991.
• 2: Zena M. Ariola , Matthias Felleisen, The call-by-need lambda calculus, Journal of Functional Programming, v.7 n.3, p.265-301, May 1997 [doi>10.1017/S0956796897002724]
• 3: Zena M. Ariola , John Maraist , Martin Odersky , Matthias Felleisen , Philip Wadler, A call-by-need lambda calculus, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.233-246, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199507]
• 4: Henk P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North-Holland, Amsterdam, NL, 1981. Studies in Logic and the Foundations of Mathematics.
• 5: Małgorzata Biernacka , Olivier Danvy, A concrete framework for environment machines, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.6-es, December 2007 [doi>10.1145/1297658.1297664]
• 6: Haskell Brookes Curry and Robert Feys. Combinatory Logic, Volume I. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1958. Second printing 1968.
• 7: Olivier Danvy , Andrzej Filinski, Abstracting control, Proceedings of the 1990 ACM conference on LISP and functional programming, p.151-160, June 27-29, 1990, Nice, France [doi>10.1145/91556.91622]
• 8: Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics. Technical Report RS-04-26, BRICS, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, November 2004.
• 9: R. Kent Dyvbig , Simon Peyton Jones , Amr Sabry, A monadic framework for delimited continuations, Journal of Functional Programming, v.17 n.6, p.687-730, November 2007 [doi>10.1017/S0956796807006259]
• 10: Mattias Felleisen, The theory and practice of first-class prompts, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.180-190, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73576]
• 11: Matthias Felleisen and Matthew Flatt. Programming languages and lambda calculi. Available from http://www.cs.utah.edu/plt/publications/pllc.pdf, January 2002.
• 12: Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD-machine, and the λ-calculus. In M. Wirsing, editor, Formal Description of Programming Concepts, pages 193--217. North-Holland, 1986.
• 13: 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]
• 14: Daniel P. Friedman and David S. Wise. CONS should not evaluate its arguments. In S. Michaelson and Robin Milner, editors, Automata, Languages and Programming, pages 257--284, Edinburgh, Scotland, 1976. Edinburgh University Press.
• 15: Daniel P. Friedman , Abdulaziz Ghuloum , Jeremy G. Siek , Onnie Lynn Winebarger, Improving the lazy Krivine machine, Higher-Order and Symbolic Computation, v.20 n.3, p.271-293, September 2007 [doi>10.1007/s10990-007-9014-0]
• 16: Jeremy Gibbons and Keith Wansbrough. Tracing lazy functional languages. In Michael E. Houle and Peter Eades, editors, Proceedings of Conference on Computing: The Australian Theory Symposium, pages 11--20, Townsville, January 29-30 1996. Australian Computer Science Communications. ISBN ISSN 0157-3055.
• 17: Peter Henderson , James H. Morris, Jr., A lazy evaluator, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.95-103, January 19-21, 1976, Atlanta, Georgia [doi>10.1145/800168.811543]
• 18: Yukiyoshi Kameyama , Oleg Kiselyov , Chung-chieh Shan, Closing the stage: from staged code to typed closures, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA [doi>10.1145/1328408.1328430]
• 19: Oleg Kiselyov , Chung-chieh Shan , Daniel P. Friedman , Amr Sabry, Backtracking, interleaving, and terminating monad transformers: (functional pearl), Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 20: Oleg Kiselyov , Chung-chieh Shan , Amr Sabry, Delimited dynamic binding, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 21: Jean-Louis Krivine, A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, v.20 n.3, p.199-207, September 2007 [doi>10.1007/s10990-007-9018-9]
• 22: 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]
• 23: John Maraist , Martin Odersky , Philip Wadler, The call-by-need lambda calculus, Journal of Functional Programming, v.8 n.3, p.275-317, May 1998 [doi>10.1017/S0956796898003037]
• 24: Eugenio Moggi and Amr Sabry. An abstract monadic semantics for value recursion. Theoretical Informatics and Applications, 38 (4): 375--400, 2004.
• 25: 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]
• 26: Simon L. Peyton Jones , Jon Salkild, The spineless tagless G-machine, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.184-201, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99385]
• 27: Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1 (2): 125--159, December 1975.
• 28: Peter Sestoft, Deriving a lazy abstract machine, Journal of Functional Programming, v.7 n.3, p.231-264, May 1997 [doi>10.1017/S0956796897002712]
• 29: Chung-Chieh Shan, A static simulation of dynamic delimited control, Higher-Order and Symbolic Computation, v.20 n.4, p.371-401, December 2007 [doi>10.1007/s10990-007-9010-4]
• 30: Gerald Jay Sussman , Guy L. Steele, Jr., Scheme: A Interpreter for Extended Lambda Calculus, Higher-Order and Symbolic Computation, v.11 n.4, p.405-439, December 1998 [doi>10.1023/A:1010035624696]
• 31: Mitchell Wand , Dale Vaillancourt, Relating models of backtracking, Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, September 19-21, 2004, Snow Bird, UT, USA
• 32: C. Wang, Obtaining lazy evaluation with continuations in scheme, Information Processing Letters, v.35 n.2, p.93-97, June 1990 [doi>10.1016/0020-0190(90)90112-B]
• 33: Hongwei Xi, Evaluation Under Lambda Abstraction, Proceedings of the9th International Symposium on Programming Languages: Implementations, Logics, and Programs: Including a Special Trach on Declarative Programming Languages in Education, p.259-273, September 03-05, 1997

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

General Terms:
Languages, Theory

Keywords:
abstract machines, call-by-need, delimited continuations, lambda calculus, reduction semantics