X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=cps.mdwn;h=4c40a667f2717f9e6b3e61958ca1016672dc9718;hp=a9842d12bb2d05cd19b462e376dbc9d6bc12863b;hb=27ce0d45d4ab28840605ec2130f6ba4ecd9d6213;hpb=aab06ee4eafe7ac322521e4cef1b1704a9258900 diff --git a/cps.mdwn b/cps.mdwn index a9842d12..4c40a667 100644 --- a/cps.mdwn +++ b/cps.mdwn @@ -18,8 +18,8 @@ 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:
(\x.y)(ww) @@ -68,103 +68,138 @@ what the CPS is doing, and how. 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 `\w.(\x.y)z` does not, because -the `\w` protects the redex in the body from reduction. -(A redex is a subform ...(\xM)N..., i.e., something that can be the -target of beta reduction.) +That is, `(\x.y)z` reduces to `z`, but `\u.(\x.y)z` does not reduce to +`\u.z`, because the `\u` 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.) Start with a simple form that has two different reduction paths: -reducing the leftmost lambda first: `(\x.y)((\x.z)w) ~~> y` +reducing the leftmost lambda first: `(\x.y)((\x.z)u) ~~> y` -reducing the rightmost lambda first: `(\x.y)((\x.z)w) ~~> (x.y)z ~~> y` +reducing the rightmost lambda first: `(\x.y)((\x.z)u) ~~> (\x.y)z ~~> 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: +Here's the CPS transform defined: - [x] => x - [\xM] => \k.k(\x[M]) - [MN] => \k.[M](\m.m[N]k) + [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: +Here's the result of applying the transform to our simple example: - [(\x.y)((\x.z)w)] - \k.[\x.y](\m.m[(\x.z)w]k) - \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[w]k))k) - \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.mwk))k) + [(\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 the entire transformed term, -we can't perform any reductions. In order to see the computation -unfold, we have to apply the transformed term to a trivial -continuation, usually the identity function `I = \x.x`. +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)w)] I - \k.[\x.y](\m.m[(\x.z)w]k) I - [\x.y](\m.m[(\x.z)w] I) - (\k.k(\x.y))(\m.m[(\x.z)w] I) - (\x.y)[(\x.z)w] I + [(\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 --A-- + * 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. +functor (`\x.y`) throws away its argument (consider the reduction in the +line marked (A)), we never need to expand the +CPS transform of the argument. This means that we never bother to +reduce redexes inside the argument. Compare with a call-by-value xform: -=> \k.kx - <\aM> => \k.k(\a ) - => \k. (\m. (\n.mnk)) + {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)w>(\n.mnk))) I - <\x.y>(\m.<(\x.z)w>(\n.mnI)) - (\k.k(\x. ))(\m.<(\x.z)w>(\n.mnI)) - <(\x.z)w>(\n.(\x. )nI) - (\k.<\x.z>(\m. (\n.mnk)))(\n.(\x. )nI) - <\x.z>(\m. (\n.mn(\n.(\x. )nI))) - (\k.k(\x. ))(\m. (\n.mn(\n.(\x. )nI))) - (\n.(\x. )n(\n.(\x. )nI)) - (\k.kw)(\n.(\x. )n(\n.(\x. )nI)) - (\x. )w(\n.(\x. )nI) - (\n.(\x. )nI) - (\k.kz)(\n.(\x. )nI) - (\x. )zI - I + {(\x.y)((\x.z)u)} 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) --A-- + * + {z}(\n.(\x.{y})nI) = + (\k.kz)(\n.(\x.{y})nI) + * * + (\x.{y})zI + * + {y}I = (\k.ky)I + * I y +In this case, the argument does get evaluated: consider the reduction +in the line marked (A). + 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. -Questions and excercises: +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. Why is the CBN xform for variables `[x] = x' instead of something -involving kappas? +1. Prove that {(\x.y)(ww)} does not terminate. -2. Write an Ocaml function that takes a lambda term and returns a +2. Why is the CBN xform for variables `[x] = x` instead of something +involving kappas (i.e., `k`'s)? + +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;; -3. What happens (in terms of evaluation order) when the application -rule for CBN CPS is changed to `[MN] = \k.[N](\n.[M]nk)`? Likewise, -What happens when the application rule for CBV CPS is changed to -` = \k. (\n. (\m.mnk))`? +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. -4. What happens when the application rules for the CPS xforms are changed to +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))`? + +6. A term and its CPS xform are different lambda terms. Yet in some +sense they "do" the same thing computationally. Make this sense +precise. - - [MN] = \k.Thinking through the types -------------------------- @@ -177,22 +212,22 @@ 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 +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' -> o) -> o. +for functional types a->b, (a->b)' = ((a' -> σ) -> σ) -> (b' -> σ) -> σ. Call by name transform Terms Types - [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] = \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 Remember that types associate to the right. Let's work through the application xform and make sure the types are consistent. We'll have @@ -202,15 +237,49 @@ the following types: N:a MN:b k:b'->o - [N]:a' - m:a'->(b'->o)->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'->(b'->o)->o)->o)->o + [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o [M](\m.m[N]k):o [MN]:(b'->o)->o -Note that even though the transform uses the same symbol for the -translation of a variable, in general it will have a different type in -the transformed term. +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. + + +Other CPS transforms +-------------------- + +It is easy to think that CBN and CBV are the only two CPS transforms. +(We've already seen a variant on call-by-value one of the excercises above.) + +In fact, the number of distinct transforms is unbounded. For +instance, here is a variant of CBV that uses the same types as CBN: + +(\m.m k) - = \k.[M](\m.[N](\n.mnk)) - = x + <\xM> = \k.k(\x ) + = \k. (\m. (\n.m(\k.kn)k)) + +Try reducing `<(\x.x) ((\y.y) (\z.z))> I` to convince yourself that +this is a version of call-by-value. + +Once we have two evaluation strategies that rely on the same types, we +can mix and match: + + [x] = x + = x + [\xM] = \k.k(\x ) + <\xM] = \k.k(\x[M]) + [MN] = \k. (\m.m k) + = \k.[M](\m.[N](\n.m(\k.kn)k)) + +This xform interleaves call-by-name and call-by-value in layers, +according to the depth of embedding.