Martin Odersky
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.
- 1.H. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984.Google Scholar
- 2.H.-J. Boehm. Side effects and aliasing can have simple axiomatic descriptions. A CM Transactions on Programming Languages and Systems, 7(4):637-655, October 1985. Google ScholarDigital Library
- 3.E. Crank and M. Felleisen. Parameter-passing and the lambda-calculus. In Proc. 18th A CM Symposium on Principles of Programming Languages, pages 233-244, January 1991. Google ScholarDigital Library
- 4.M. Felleisen. On the expressive power of programming languages. In N. D. Jones, editor, ESOP '90, European Symposium on Programming, Lecture Notes in Computer Science 432, pages 134-151. Springer-Verlag, 1990. Google ScholarDigital Library
- 5.M. Felleisen and D. P. Friedman. A calculus for assignments in higher-order languages. In Proc. 14th A CM Symposium on Principles of Programming Languages, pages 314-325, January 1987. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- 8.J. GuzmAn and P. Hudak. Single-threaded polymorphic lambda calculus. In IEEE Symposium on Logic in Computer Science, pages 333-343, June 1990.Google ScholarCross Ref
- 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, and B. A. Sufrin. Laws of programming. Communications of the A CM, 30(8):672-686, August 1987. Google ScholarDigital Library
- 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.Google Scholar
- 11.I. Mason and C. Talcott. Programming, transforming, and proving with function abstractions and memories. In Automata, Languages, and Programming: 16th International Colloquium, Lecture Notes in Computer Science 372, pages 574-588. Springer-Verlag, 1989. Google Scholar
- 12.i. Mason and C. Talcott. Equivalence in functional languages with side effects. Journal of Functional Programming, 1(3):287-327, July 1991.Google ScholarCross Ref
- 13.M. Odersky. Observers for linear types. In B. Krieg- Briickner, editor, ESOP '92: 4th European Symposium on Programming, Rennes, France, Proceedings, Lecture Notes in Computer Science 582, pages 390-407. Springer-Verlag, February 1992. Google ScholarDigital Library
- 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.Google Scholar
- 15.G. D. Plotkin. Call-by-name, call-by-value, and the ,k-calculus. Theoretical Computer Science, 1:125-159, 1975.Google ScholarCross Ref
- 16.J. C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, June 1988.Google Scholar
- 17.D. Schmidt. Detecting global variables in denotational specifications. A CM Transactions on Programming Languages and Systems, 5(2):299-310, 1985. Google ScholarDigital Library
- 18.V. Swarup, U. S. Reddy, and E. ireland. Assignments for applicative languages. In J. Hughes, editor, Proc. 5th A CM Conf. on Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science 523, pages 192-214. Springer-Verlag, August 1991. Google Scholar
- 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.Google Scholar
- 20.P. Wadler. Comprehending monads. In Proc. A CM Conf. on Lisp and Functional Programming, pages 61- 78, June 1990. Google ScholarDigital Library
- 21.P. Wadler. Is there a use for linear logic? In Proc. Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 255-273, June 1991. SIG- PLAN Notices, Volume 26, Number 9. Google ScholarDigital Library
- 22.P. Wadler. The essence of functional programming. In Proc. 19th A CM Symposium on Principles of Programming Languages, pages 1-14, January 1992. Google ScholarDigital Library
Index Terms
- Call by name, assignment, and the lambda calculus
Recommendations
The call-by-need lambda calculus
We present a calculus that captures the operational semantics of call-by-need. The call-by-need lambda calculus is confluent, has a notion of standard reduction, and entails the same observational equivalence relation as the call-by-name calculus. The ...
An approach to call-by-name delimited continuations
POPL '08We show that a variant of Parigot's λμ-calculus, originally due to de Groote and proved to satisfy Boehm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al'...
Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus
We study normalization in the simply typed lambda-mu calculus, an extension of lambda calculus with control flow operators. Using an enriched version of the Yoneda embedding, we obtain a categorical normal form function for simply typed lambda-mu terms, ...
Comments