Michael J. Fischer
Abstract
A lambda calculus schema is an expression of the lambda calculus augmented by uninterpreted constant and function symbols and thus is an abstraction of programming languages such as LISP which permit functions to be passed to or returned from other functions. We then consider two natural implementation strategies: the retention strategy in which all variable bindings are retained until no longer needed (implying the use of some sort of garbage collected store) and the deletion strategy, modelled after the usual stack implementation of ALGOL-60, in which variable bindings are destroyed when control leaves the procedure (or block) in which they were created. Berry shows that the deletion strategy implementation is not “correct” for a wide class of languages in the sense that it is not equivalent to natural extensions of the copy rule of ALGOL to such languages, whereas the retention strategy is correct in that sense. We show, however, that no real power is lost in restricting oneself to a deletion strategy implementation, for any program can be translated into an equivalent one which will work correctly under such an implementation. The proof makes no use of the particular primitive functions and data of the language and hence is true of the corresponding schemata under all interpretations.
- 1 Berry, D.M., "Introduction to Oregano," SIGPLAN Notices 6,2 (February 1971), 171-190. Google Scholar
Digital Library
- 2 Berry, D.M., "Block Structure: Retention or Deletion," Proceedings of the Third Annual ACM Symposium on Theory of Computing (1971), 86-100. Google ScholarDigital Library
- 3 Church, A., The Calculi of Lambda Conversion, Princeton, 1941. Google ScholarDigital Library
- 4 Cole, S.N., "Pushdown Store Machines and Real-Time Computation," ACM Symposium on Theory of Computing (1969), 233-245. Google ScholarDigital Library
- 5 Dijkstra, E.W., "Recursive Programming," in Programming Systems and Languages, S. Rosen, McGraw-Hill, N.Y. 1967.Google Scholar
- 6 Evans, A., "PAL - A Language Designed for Teaching Programming Linguistics," Proceedings of the ACM 23rd National Conference, August 1968. Google ScholarDigital Library
- 7 Ginsburg, S., Greibach, S., and Harrison, M., "One-Way Stack Automata," JACM 14,2 (April 1967), 389-418. Google ScholarDigital Library
- 8 Henhapl, W. and Jones, C.D., "The Block Concept and Some Possible Implementations, with Proofs of Equivalence," TR 25.104, IBM Vienna, (April 1970).Google Scholar
- 9 Hewitt, C., "More Comparative Schematology," MIT Project MAC, Artificial Intelligence Memo No. 207 (August 1970).Google Scholar
- 10 Landin, P.J., "The Mechanical Evaluation of Expressions," Comput. J. 6,4 (January 1964).Google ScholarCross Ref
- 11 McCarthy, J. et al., The LISP 1.5 Programmers Manual, MIT Press (1963). Google ScholarDigital Library
- 12 McCarthy, J., "A Basis for a Mathematical Theory of Computation," in Computer Programming and Formal Systems, P. Braffort and D. Hirschberg, ed., North-Holland, Amsterdam, 1963.Google Scholar
- 13 Moses, J., "The Function of FUNCTION in LISP (or, Why the FUNARG Problem Should be Called the Environment Problem)," SIGSAM Bulletin No. 15 (July 1970). Google ScholarDigital Library
- 14 Randell, B. and Russell, L.J., Algol 60 Implementation, Academic Press, New York, 1964. Google ScholarDigital Library
Index Terms
- Lambda calculus schemata
Recommendations
Lambda calculus schemata
Proceedings of ACM conference on Proving assertions about programsA lambda calculus schema is an expression of the lambda calculus augmented by uninterpreted constant and function symbols and thus is an abstraction of programming languages such as LISP which permit functions to be passed to or returned from other ...
Lambda calculus schemata
Proceedings of ACM conference on Proving assertions about programsA lambda calculus schema is an expression of the lambda calculus augmented by uninterpreted constant and function symbols and thus is an abstraction of programming languages such as LISP which permit functions to be passed to or returned from other ...
Comments