(\x.y)(ww) @@ -68,10 +68,11 @@ 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 reduction.) +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.) Start with a simple form that has two different reduction paths: @@ -92,23 +93,23 @@ Here's the CPS transform defined: Here's the result of applying the transform to our problem term: - [(\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)((\x.z)u)] I = + (\k.[\x.y](\m.m[(\x.z)u]k)) I * - [\x.y](\m.m[(\x.z)w] I) = - (\k.k(\x.y))(\m.m[(\x.z)w] I) + [\x.y](\m.m[(\x.z)u] I) = + (\k.k(\x.y))(\m.m[(\x.z)u] I) * * - (\x.y)[(\x.z)w] I + (\x.y)[(\x.z)u] I * y I @@ -125,21 +126,21 @@ Compare with a call-by-value xform: 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 + (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I * - {\x.y}(\m.{(\x.z)w}(\n.mnI)) = - (\k.k(\x.{y}))(\m.{(\x.z)w}(\n.mnI)) + {\x.y}(\m.{(\x.z)u}(\n.mnI)) = + (\k.k(\x.{y}))(\m.{(\x.z)u}(\n.mnI)) * * - {(\x.z)w}(\n.(\x.{y})nI) = - (\k.{\x.z}(\m.{w}(\n.mnk)))(\n.(\x.{y})nI) + {(\x.z)u}(\n.(\x.{y})nI) = + (\k.{\x.z}(\m.{u}(\n.mnk)))(\n.(\x.{y})nI) * - {\x.z}(\m.{w}(\n.mn(\n.(\x.{y})nI))) = - (\k.k(\x.{z}))(\m.{w}(\n.mn(\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))) * * - {w}(\n.(\x.{z})n(\n.(\x.{y})nI)) = - (\k.kw)(\n.(\x.{z})n(\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})w(\n.(\x.{y})nI) + (\x.{z})u(\n.(\x.{y})nI) * {z}(\n.(\x.{y})nI) = (\k.kz)(\n.(\x.{y})nI) @@ -156,27 +157,40 @@ 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. Why is the CBN xform for variables `[x] = x' instead of something +1. Prove that {(\x.y)(ww)} does not terminate. + +2. Why is the CBN xform for variables `[x] = x' instead of something involving kappas? -2. Write an Ocaml function that takes a lambda term and returns a +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 -`{MN} = \k.{N}(\n.{M}(\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))`? -- [MN] = \k.{M}(\m.m{N}k) - {MN} = \k.[M](\m.[N](\n.mnk)) -Thinking through the types -------------------------- @@ -196,15 +210,15 @@ 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' -> o) -> o) -> (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'->σ)->σ + [\xM] = \k.k(\x[M]) [a->b] = ((a->b)'->σ)->σ + [MN] = \k.[M](\m.m[N]k) [b] = (b'->σ)->σ Remember that types associate to the right. Let's work through the application xform and make sure the types are consistent. We'll have @@ -213,16 +227,19 @@ the following types: 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 - -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. - + k:b'->σ + [N]:(a'->σ)->σ + m:((a'->σ)->σ)->(b'->σ)->σ + m[N]:(b'->σ)->σ + m[N]k:σ + [M]:((a->b)'->σ)->σ = ((((a'->σ)->σ)->(b'->σ)->σ)->σ)->σ + [M](\m.m[N]k):σ + [MN]:(b'->σ)->σ + +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.