Lazy evaluation alternative

Keith Wansbrough Keith.Wansbrough@cl.cam.ac.uk
Sun, 26 Jan 2003 12:38:01 +0000


>     I wonder if I could run an idea I've had by this list. It seems to
> me you could get some of the desired effects of lazy evaluation by using
> continuation passing style in code. For example, take this psuedo-code
> using CPS to represent an infinite data type.

This has been known for a long time; the CPS translation results in a 
program that has the same behaviour no matter what the underlying 
language's evaluation semantics are.  The lambdas make explicit what 
can happen now and what must be delayed until later.  Consequently 
using a strict (call-by-value) or lazy (roughly call-by-name) language 
makes no difference.

Here is what I believe to be the original paper (1975):

@Article{
   Plotkin75:Call,
   author="G. D. Plotkin",
   title="Call-By-Name, Call-By-Value and the Lambda Calculus",
   journal="Theoretical Computer Science",
   year="1975",
   volume="1",
   pages="125--159",
   abstract="This paper examines the old question of the relationship
      between ISWIM and the $\lambda$-calculus, using the distinction
      between call-by-value and call-by-name.  It is held that the
      relationship should be mediated by a standardisation theorem.
      Since this leads to difficulties, a new $\lambda$-calculus is
      introduced whose standardisation theorem gives a good
      correspondence with ISWIM as given by the SECD machine, but
      without the \emph{letrec} feature.  Next a call-by-name variant of
      ISWIM is introduced which is in an analogous correspondence with
      the usual $\lambda$-calculus.  The relation between call-by-value
      and call-by-name is then studied by giving simulations of each
      language by the other and interpretations of each calculus in the
      other.  These are obtained as another application of the
      continuation technique.  Some emphasis is placed throughout on the
      notion of operational equality (or contextual equality).  If terms
      can be proved equal in a calculus they are operationally equal in
      the corresponding language.  Unfortunately, operational equality
      is not preserved by either of the simulations.",
}

Enjoy!

--KW 8-)
-- 
Keith Wansbrough <kw217@cl.cam.ac.uk>
http://www.cl.cam.ac.uk/users/kw217/
University of Cambridge Computer Laboratory.