to gain some control over order of evaluation (think of Jim's abort handler).
We continue to reason about order of evaluation.
-A superbly clear and lucid discussion can be found here:
-[Sestoft: Demonstrating Lambda Calculus Reduction](http://tinyurl.com/27nd3ub).
-Sestoft also provides a really lovely lambda evaluator,
+A lucid discussion of evaluation order in the
+context of the lambda calculus can be found here:
+[Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf).
+Sestoft also provides a lovely on-line lambda evaluator:
+[Sestoft: Lambda calculus reduction workbench](http://www.itu.dk/~sestoft/lamreduce/index.html),
which allows you to select multiple evaluation strategies,
-and to see reductions happen step by step:
-[Sestoft's lambda reduction webpage](http://ellemose.dina.kvl.dk/~sestoft/lamreduce/lamframes.html).
-
+and to see reductions happen step by step.
Evaluation order matters
------------------------
We've seen this many times. For instance, consider the following
reductions. It will be convenient to use the abbreviation `w =
-\x.xx`. I'll indicate which lambda is about to be reduced with a *
-underneath:
+\x.xx`. I'll
+indicate which lambda is about to be reduced with a * underneath:
<pre>
(\x.y)(ww)
And we never get the recursion off the ground.
-Restricting evaluation: call by name, call by value
----------------------------------------------------
+Using a Continuation Passing Style transform to control order of evaluation
+---------------------------------------------------------------------------
-One way to begin to gain some control is by adjusting our notion of
-beta reduction. This strategy has some of the flavor of adding types,
-but is actually a part of the untyped calculus.
+We'll present a technique for controlling evaluation order by transforming a lambda term
+using a Continuation Passing Style transform (CPS), then we'll explore
+what the CPS is doing, and how.
-In order to have a precise discussion, we'll need some vocabulary.
-We've been talking about normal form (lambda terms that can't be
-further reduced), and leftmost evaluation (the reduction strategy of
-always choosing the left most reducible lambda); we'll need to refine
-both of those concepts.
+In order for the CPS to work, we have to adopt a new restriction on
+beta reduction: beta reduction does not occur underneath a lambda.
+That is, `(\x.y)z` reduces to `z`, but `\u.(\x.y)z` does not reduce to
+`\w.z`, because the `\w` protects the redex in the body from
+reduction. (In this context, a redex is a part of a term that matches
+the pattern `...((\xM)N)...`, i.e., something that can potentially be
+the target of beta reduction.)
-Kinds of normal form:
----------------------
+Start with a simple form that has two different reduction paths:
-Recall that there are three kinds of lambda term. Let `a` be an
-arbitrary variable, and let `M` and `N` be arbitrary terms:
+reducing the leftmost lambda first: `(\x.y)((\x.z)w) ~~> y`
-<pre>
-The pure untyped lambda calculus (again):
+reducing the rightmost lambda first: `(\x.y)((\x.z)w) ~~> (\x.y)z ~~> y`
- Form Examples
-Variable a x, y, z
-Abstract \aM \x.x, \x.y, \x.\y.y
-Application MN (x x), ((\x.x) y), ((\x.x)(\y.y))
-</pre>
+After using the following call-by-name CPS transform---and assuming
+that we never evaluate redexes protected by a lambda---only the first
+reduction path will be available: we will have gained control over the
+order in which beta reductions are allowed to be performed.
+
+Here's the CPS transform defined:
+
+ [x] = x
+ [\xM] = \k.k(\x[M])
+ [MN] = \k.[M](\m.m[N]k)
+
+Here's the result of applying the transform to our problem term:
+
+ [(\x.y)((\x.z)u)] =
+ \k.[\x.y](\m.m[(\x.z)u]k) =
+ \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[u]k))k) =
+ \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.muk))k)
+
+Because the initial `\k` protects (i.e., takes scope over) the entire
+transformed term, we can't perform any reductions. In order to watch
+the computation unfold, we have to apply the transformed term to a
+trivial continuation, usually the identity function `I = \x.x`.
+
+ [(\x.y)((\x.z)u)] I =
+ (\k.[\x.y](\m.m[(\x.z)u]k)) I
+ *
+ [\x.y](\m.m[(\x.z)u] I) =
+ (\k.k(\x.y))(\m.m[(\x.z)u] I)
+ * *
+ (\x.y)[(\x.z)u] I
+ *
+ y I
+
+The application to `I` unlocks the leftmost functor. Because that
+functor (`\x.y`) throws away its argument, we never need to expand the
+CPS transform of the argument.
+
+Compare with a call-by-value xform:
+
+ {x} = \k.kx
+ {\aM} = \k.k(\a{M})
+ {MN} = \k.{M}(\m.{N}(\n.mnk))
+
+This time the reduction unfolds in a different manner:
+
+ {(\x.y)((\x.z)w)} I =
+ (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I
+ *
+ {\x.y}(\m.{(\x.z)u}(\n.mnI)) =
+ (\k.k(\x.{y}))(\m.{(\x.z)u}(\n.mnI))
+ * *
+ {(\x.z)u}(\n.(\x.{y})nI) =
+ (\k.{\x.z}(\m.{u}(\n.mnk)))(\n.(\x.{y})nI)
+ *
+ {\x.z}(\m.{u}(\n.mn(\n.(\x.{y})nI))) =
+ (\k.k(\x.{z}))(\m.{u}(\n.mn(\n.(\x.{y})nI)))
+ * *
+ {u}(\n.(\x.{z})n(\n.(\x.{y})nI)) =
+ (\k.ku)(\n.(\x.{z})n(\n.(\x.{y})nI))
+ * *
+ (\x.{z})u(\n.(\x.{y})nI)
+ *
+ {z}(\n.(\x.{y})nI) =
+ (\k.kz)(\n.(\x.{y})nI)
+ * *
+ (\x.{y})zI
+ *
+ {y}I =
+ (\k.ky)I
+ *
+ I y
+
+Both xforms make the following guarantee: as long as redexes
+underneath a lambda are never evaluated, there will be at most one
+reduction available at any step in the evaluation.
+That is, all choice is removed from the evaluation process.
+
+Now let's verify that the CBN CPS avoids the infinite reduction path
+discussed above (remember that `w = \x.xx`):
+
+ [(\x.y)(ww)] I =
+ (\k.[\x.y](\m.m[ww]k)) I
+ *
+ [\x.y](\m.m[ww]I) =
+ (\k.k(\x.y))(\m.m[ww]I)
+ * *
+ (\x.y)[ww]I
+ *
+ y I
+
+
+Questions and exercises:
+
+1. Prove that {(\x.y)(ww)} does not terminate.
+
+2. Why is the CBN xform for variables `[x] = x' instead of something
+involving kappas?
+
+3. Write an Ocaml function that takes a lambda term and returns a
+CPS-xformed lambda term. You can use the following data declaration:
+
+ type form = Var of char | Abs of char * form | App of form * form;;
+
+4. The discussion above talks about the "leftmost" redex, or the
+"rightmost". But these words apply accurately only in a special set
+of terms. Characterize the order of evaluation for CBN (likewise, for
+CBV) more completely and carefully.
-It will be helpful to define a *redex*, which is a lambda term of
-the form `((\aM) N)`. That is, a redex is a form for which beta
-reduction is defined (ignoring, as usual, the manouvering required in
-order to avoid variable collision).
+5. What happens (in terms of evaluation order) when the application
+rule for CBV CPS is changed to `{MN} = \k.{N}(\n.{M}(\m.mnk))`?
-It will also be helpful to have names for the two components of an
-application `(M N)`: we'll call `M` the *functor*, and `N` the
-*argument*. Note that functor position can be occupied by a variable,
-since `x` is in the functor position of the term `(x y)`.
-Ok, with that vocabulary, we can distinguish four different types of
-normal form:
+Thinking through the types
+--------------------------
+This discussion is based on [Meyer and Wand 1985](http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.44.7943&rep=rep1&type=pdf).
+Let's say we're working in the simply-typed lambda calculus.
+Then if the original term is well-typed, the CPS xform will also be
+well-typed. But what will the type of the transformed term be?
+The transformed terms all have the form `\k.blah`. The rule for the
+CBN xform of a variable appears to be an exception, but instead of
+writing `[x] = x`, we can write `[x] = \k.xk`, which is
+eta-equivalent. The `k`'s are continuations: functions from something
+to a result. Let's use σ as the result type. The each `k` in
+the transform will be a function of type ρ --> σ for some
+choice of ρ.
+We'll need an ancilliary function ': for any ground type a, a' = a;
+for functional types a->b, (a->b)' = ((a' -> σ) -> σ) -> (b' -> σ) -> σ.
+ Call by name transform
+ Terms Types
-Take Plotkin's CBN CPS:
+ [x] = \k.xk [a] = (a'->o)->o
+ [\xM] = \k.k(\x[M]) [a->b] = ((a->b)'->o)->o
+ [MN] = \k.[M](\m.m[N]k) [b] = (b'->o)->o
-[x] ~~> x
-[\xM] ~~> \k.k(\x[M])
-[MN] ~~> \k.[M](\m.m[N]k)
+Remember that types associate to the right. Let's work through the
+application xform and make sure the types are consistent. We'll have
+the following types:
-let w = \x.xx in
+ M:a->b
+ N:a
+ MN:b
+ k:b'->o
+ [N]:(a'->o)->o
+ m:((a'->o)->o)->(b'->o)->o
+ m[N]:(b'->o)->o
+ m[N]k:o
+ [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o
+ [M](\m.m[N]k):o
+ [MN]:(b'->o)->o
-[(\xy)(ww)] ~~>
-\k.[\xy](\m.m[ww]k) ~~>
-\k.[\xy](\m.m(\k.[w](\m.m[w]k))k) ~~>
-\k.[\xy](\m.m(\k.(\k.k(\x[xx]))(\m.m[w]k))k) ~~> beta*
-\k.[\xy](\m.m(\k.(\x[xx])[w]k)k) ~~>
-\k.[\xy](\m.m(\k.(\x(\k.[x](\m.m[x]k)))[w]k)k) ~~>
-\k.[\xy](\m.m(\k.(\x(\k.x(\m.mxk)))[w]k)k) ~~> beta
-\k.[\xy](\m.m(\k.[w](\m.m[w]k))k) --- same as second line!
+Be aware that even though the transform uses the same symbol for the
+translation of a variable (i.e., `[x] = x`), in general the variable
+in the transformed term will have a different type than in the source
+term.
+Excercise: what should the function ' be for the CBV xform? Hint:
+see the Meyer and Wand abstract linked above for the answer.