[Prev][Next][Index][Thread]

Continuations may be unreasonable


In an upcoming paper (LISP and Func. Prog. '88), we show that lambda
calculus terms can be call-by-value observationally congruent (i.e.
agree in all contexts---see below) but their continuation-passing
versions may not be.

We use the call-by-value transform of Fischer, Plotkin, and others, in
a call-by-value calculus with integer base constants and recursion.
The two terms

     \a. \b. \c. (\x. (b a) x) (c a)
     \a. \b. \c. (b a) (c a)

are call-by-value observationally congruent, but their continuized
versions are not.  This counterexample is quite strong: these terms
are call-by-value observationally congruent in *untyped* contexts, but
we have exhibited a *typed* context that distinguishes their
transforms.  No strange operators are used in distinguishing the 
continuized versions, only a single integer and a nonterminating
computation.

One can also show that the lambda calculus augmented by call/cc
operators (a la Felleisen-Friedman-Kohlbecker-Duba) distinguishes
these terms.  Continuation-passing and call/cc give us an added
measure of control over functional programs---the price, though, is
that observational congruence reasoning on direct terms becomes too
coarse for reasoning about continuation-passing terms or terms
appearing in contexts with call/cc.  Continuations thus require
new reasoning tools; old intuitions about programs fail.
Techniques for reasoning about continuations and observational
congruences remain to be developed.

Our notion of observational congruence is the following:
     DEF:  Two terms M and N are *observationally congruent* if for 
           any closing context C[ ] with C[M], C[N] of integer type, 
           Eval(C[M]) and Eval(C[N]) either both do not halt or both 
           equal the numeral 0.
One can modify this definition to observe all numerals or simply 
termination; one can also consider typed or untyped contexts.
Any of these modifications preserves the integrity of the above 
counterexample.

We can send preprints to those who are interested further in these
results.  Would people like access to an electronic version?  We will
leave the LaTeX files in a world-readable directory (accessible using
"ftp") if enough people could make use of an electronic copy.


-Albert Meyer and Jon Riecke