(\x.y)(ww) @@ -59,67 +59,187 @@ Y (\f n. blah) = 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` --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)) -+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.