The semantics of lazy (and industrious) evaluation

ABSTRACT

Since the publication of two influential papers on lazy evaluation in 1976 [Henderson and Morris, Friedman and Wise], the idea has gained widespread acceptance among language theoreticians—particularly among the advocates of “functional programming” [Henderson80, Backus78]. There are two basic reasons for the popularity of lazy evaluation. First, by making some of the data constructors in a functional language non-strict, it supports programs that manipulate “infinite objects” such as recursively enumerable sequences, which may make some applications easier to program. Second, by delaying evaluation of arguments until they are actually needed, it may speed up computations involving ordinary finite objects. First, there are several semantically distinct definitions of lazy evaluation that plausibly capture the intuitive notion. Second, non-trivial lazy spaces are similar in structure (under the approximation ordering) to universal domains (as defined by Scott [Scott81, Scott76]) such as the P@@@@ model for the untyped lambda calculus. Third, we prove that neither initial algebra specifications [ADJ76,77] nor final algebra specifications [Guttag78, Kamin80] have the power to define lazy spaces. Fourth, although lazy spaces have the same “higher-order” structure as P@@@@, they nevertheless have an elegant, natural characterization within first order logic. In this paper, we develop a simple, yet comprehensive first order theory of lazy spaces relying on three axiom schemes asserting (1) the principle of structural induction for finite objects; (2) the existence of least upper bounds for directed sets; and (3) the continuity of functions.

REFERENCES

• 1: Goguen, J., J. Thatcher and E. Wagner. An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types. IBM Research Report RC-6478, Yorktown Heights, 1976.
• 2: J. A. Goguen , J. W. Thatcher , E. G. Wagner , J. B. Wright, Initial Algebra Semantics and Continuous Algebras, Journal of the ACM (JACM), v.24 n.1, p.68-95, Jan. 1977 [doi>10.1145/321992.321997]
• 3: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 4: Barendregt, H. The Type Free Lambda Calculus. Handbook of Mathematical Logic, J. Barwise. ed., North-Holland, Amsterdam, pp. 1091-1132.
• 5: Robert S. Boyer , J. Strother Moore, Proving Theorems about LISP Functions, Journal of the ACM (JACM), v.22 n.1, p.129-144, Jan. 1975 [doi>10.1145/321864.321875]
• 6: Boyer, R.S., and Moore, JS. A Computational Logic, Academic Press, New York, 1979.
• 7: Cartwright, R. User-Defined Data Types as an Aid to Verifying LISP Programs. Automata, Languages and Programming. Edinburgh Press, 1976.
• 8: Robert Cartwright, A constructive alternative to axiomatic data type definitions, Proceedings of the 1980 ACM conference on LISP and functional programming, p.46-55, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802789]
• 9: Enderton, H.B. A Mathematical Introduction to Logic. Academic Press, New York, 1972.
• 10: Friedman, D. and D. Wise. CONS Should Not Evaluate Its Arguments. Automata, Languages and Programming, Edinburgh University Press, 1976, pp.257-284.
• 11: Giles. An LCF Axiomatization of Lazy Lists. CSR-31-78. Computer Science Department, Edinburgh University.
• 12: Gordon, M., R. Milner and C. Wadsworth. Edinburgh LCF. CSR-11-77. Computer Science Department, Edinburgh University.
• 13: Guttag, J. and J. Horning. The Algebraic Specification of Abstract Data Types. Acta Informatica 10 (1978), pp. 27-52.
• 14: Peter Henderson, Functional Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1980
• 15: 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]
• 16: Samuel Kamin, Final data type specifications: a new data type specification method, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.131-138, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567459]
• 17: Scott, D. Data Types as Lattices. SIAM J. Computing 5 (1976), pp. 522-587.
• 18: Scott, D. Lectures on a Mathematical Theory of Computation. Technical Monograph PRG-19, Oxford University Computing Laboratory, Oxford.
• 19: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977

INDEX TERMS

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

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

General Terms:
Languages