Continuations may be unreasonable

ABSTRACT

We show that two lambda calculus terms can be observationally congruent (i.e., agree in all contexts) but their continuation-passing transforms may not be. We also show that two terms may be congruent in all untyped contexts but fail to be congruent in a calculus with call/cc operators. Hence, familiar reasoning about functional terms may be unsound if the terms use continuations explicitly or access them implicitly through new operators. We then examine one method of connecting terms with their continuized form, extending the work of Meyer and Wand [8].

REFERENCES

• 1: H. P. Barendregt. The Lambda Calculus: Its Syntaz and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, 1981. l~evised Edition, 1984.
• 2: M. Felleisen. Private communication, April 22, 1988.
• 3: M. 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]
• 4: M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba. Reasoning with continuations. In Syrup. or~ Logic in Computer Science, pages 131-I41, IEEE, 1986.
• 5: M. Felleisen , D. P. Friedman , E. Kohlbecker , B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, v.52 n.3, p.205-237, June 1987 [doi>10.1016/0304-3975(87)90109-5]
• 6: Michael J. Fischer, Lambda calculus schemata, Proceedings of ACM conference on Proving assertions about programs, p.104-109, January 06-07, 1972, Las Cruces, New Mexico, United States
• 7: A. R. Meyer. Semantical paradigms. In Syrup. on Logic and Computer Science, IEEE, 1988. Appendices by Stavros Cosmadakis. To appear.
• 8: Albert R. Meyer , Mitchell Wand, Continuation Semantics in Typed Lambda-Calculi (Summary), Proceedings of the Conference on Logic of Programs, p.219-224, June 17-19, 1985
• 9: R. Milner. A theory of type polymorphism in programming. J. Computer and System Sci., 17:348-375, 1978.
• 10: G. D. Plotkin. Call-by-name, call-byvalue and the lambda calculus. Theoretical Computer Science, 1:125-159, 1975.
• 11: G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-256, 1977.
• 12: G. D. Plotkin. Types and partial functions. 1984. Unpublished lecture notes.
• 13: J Rees , W Clinger, Revised report on the algorithmic language scheme, ACM SIGPLAN Notices, v.21 n.12, p.37-79, Dec. 1986 [doi>10.1145/15042.15043]
• 14: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 15: John C. Reynolds, On the Relation between Direct and Continuation Semantics, Proceedings of the 2nd Colloquium on Automata, Languages and Programming, p.141-156, July 29-August 02, 1974
• 16: David A. Schmidt, Denotational semantics: a methodology for language development, William C. Brown Publishers, Dubuque, IA, 1986
• 17: Ravi Sethi , Adrian Tang, Constructing Call-by-Value Continuation Semantics, Journal of the ACM (JACM), v.27 n.3, p.580-597, July 1980 [doi>10.1145/322203.322216]
• 18: R. Statman. A-definable functionals and /3r/-conversion. A rchiv Math. Logik Grundlagenforsch., 22:1-6, 1982.
• 19: Guy L. Steele, Jr., Rabbit: A Compiler for Scheme, Massachusetts Institute of Technology, Cambridge, MA, 1978
• 20: Guy L. Steele, Jr., Common LISP: the language, Digital Press, Newton, MA, 1984
• 21: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 22: J. E. Stoy. The congruence of two programming language definitions. Theoretical Computer Science, 13:151-174, 1981.
• 23: C. Strachey and C. Wadsworth. Contin~ations: A Mathematical Semantics for Handling Full Jumps. Technical Report PRG-11, Oxford University Computing Laboratory, 1974.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Design, Languages