Call by name, assignment, and the lambda calculus

ABSTRACT

We define an extension of the call-by-name lambda calculus with additional constructs and reduction rules that represent mutable variables and assignments. The extended calculus has neither a concept of an explicit store nor a concept of evaluation order; nevertheless, we show that programs in the calculus can be implemented using a single-threaded store. We also show that the new calculus has the Church-Rosser property and that it is a conservative extension of classical lambda calculus with respect to operational equivalence; that is, all algebraic laws of the functional subset are preserved.

REFERENCES

• 1: H. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984.
• 2: Hans-Juergen Boehm, Side effects and aliasing can have simple axiomatic descriptions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.4, p.637-655, Oct. 1985 [doi>10.1145/4472.4474]
• 3: 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]
• 4: M. Felleisen, On the expressive power of programming languages, Proceedings of the third European symposium on programming on ESOP '90, p.134-151, May 1990, Copenhagen, Denmark
• 5: M. Felleisen , D. P. Friedman, A calculus for assignments in higher-order languages, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.314, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41654]
• 6: M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Technical Report Rice COMP TR89-100, Rice University, June 1989. To Appear in Theoretical Computer Science.
• 7: J. Field. A simple rewriting semantics for realistic imperative programs and its application to program analysis. In PEPM'92: A CM SIGPLAN Workshop on Partial Evaluation and Semantics.Based Program Manipulation, pages 98-107, June 1992. Yale University Research Report YALEU/DCS/RR-909.
• 8: J. GuzmAn and P. Hudak. Single-threaded polymorphic lambda calculus. In IEEE Symposium on Logic in Computer Science, pages 333-343, June 1990.
• 9: C. A. R. Hoare , I. J. Hayes , He Jifeng , C. C. Morgan , A. W. Roscoe , J. W. Sanders , I. H. Sorensen , J. M. Spivey , B. A. Sufrin, Laws of programming, Communications of the ACM, v.30 n.8, p.672-686, Aug. 1987 [doi>10.1145/27651.27653]
• 10: P. Hudak and D. Robin. Mutable abstract datatypes - or- how to have your state and munge it too. Research Report YALEU/DCS/RR-914, Yale University, Department of Computer Science, July 1992.
• 11: Ian A. Mason , Carolyn L. Talcott, Programming, Transforming, and Providing with Function Abstractions and Memories, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.574-588, July 11-15, 1989
• 12: i. Mason and C. Talcott. Equivalence in functional languages with side effects. Journal of Functional Programming, 1(3):287-327, July 1991.
• 13: Martin Odersky, Observers for linear types, Symposium proceedings on 4th European symposium on programming, p.390-407, January 1992, Rennes, France
• 14: M. Odersky and D. Robin. The unexpurgated callby-name, assignment, and the lambda-calculus. Research Report YALEU/DCS/RR-930, Department of Computer Science, Yale University, New Haven, Connecticut, October 1992.
• 15: G. D. Plotkin. Call-by-name, call-by-value, and the ,k-calculus. Theoretical Computer Science, 1:125-159, 1975.
• 16: J. C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, June 1988.
• 17: David A. Schmidt, Detecting global variables in denotational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.2, p.299-310, April 1985 [doi>10.1145/3318.3323]
• 18: Vipin Swarup , Uday S. Reddy , Evan Ireland, Assignments for applicative languages, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.192-214, June 1991, Cambridge, Massachusetts, United States
• 19: j.-P. Talpin and P. Jouvelot. Type, effect and region reconstruction in polymorphic functional languages. In Workshop on Static Analysis of Equational, Functional, and Logic Programs, Bordeaux, Oct. 1991.
• 20: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]
• 21: Philip Wadler, Is there a use for linear logic?, ACM SIGPLAN Notices, v.26 n.9, p.255-273, Sept. 1991
• 22: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]

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:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory