Continuations may be unreasonable
A Meyer, JG Riecke - Proceedings of the 1988 ACM Conference on Lisp …, 1988 - dl.acm.org
A Meyer, JG Riecke
Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, 1988•dl.acm.orgWe show that two lambda calculus terms can be observationally congruent (ie, 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 …
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 …
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].