X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=cps.mdwn;h=bb478c6585e0070c72defa7e3cda1faa398ae9d2;hp=73edf0d0bd24778e1bfe9c4cda35b259cc146f42;hb=b182d028574a85cb3bf9d8105f054c8ea6a99b03;hpb=84044a390060ed446864f14556ece128d48e53d8 diff --git a/cps.mdwn b/cps.mdwn index 73edf0d0..bb478c65 100644 --- a/cps.mdwn +++ b/cps.mdwn @@ -9,8 +9,7 @@ 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), +[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. @@ -63,7 +62,7 @@ And we never get the recursion off the ground. Using a Continuation Passing Style transform to control order of evaluation --------------------------------------------------------------------------- -We'll exhibit and explore the technique of transforming a lambda term +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. @@ -71,12 +70,14 @@ 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.) 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)w) ~~> y` -reducing the rightmost lambda first: `(\x.y)((\x.z)w) ~~> (x.y)z ~~> y' +reducing the rightmost lambda first: `(\x.y)((\x.z)w) ~~> (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 @@ -114,33 +115,33 @@ CPS transform of 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)w)} I + (\k.{\x.y}(\m.{(\x.z)w}(\n.mnk))) I + {\x.y}(\m.{(\x.z)w}(\n.mnI)) + (\k.k(\x.{y}))(\m.{(\x.z)w}(\n.mnI)) + {(\x.z)w}(\n.(\x.{y})nI) + (\k.{\x.z}(\m.{w}(\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))) + {w}(\n.(\x.{z})n(\n.(\x.{y})nI)) + (\k.kw)(\n.(\x.{z})n(\n.(\x.{y})nI)) + (\x.{z})w(\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 avaialble at any step in the evaluation. +reduction available at any step in the evaluation. That is, all choice is removed from the evaluation process. Questions and excercises: @@ -149,20 +150,21 @@ Questions and excercises: involving kappas? 2. Write an Ocaml function that takes a lambda term and returns a -CPS-xformed lambda term. +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](\n.[M](\m.mnk))'? +What happens when the application rule for CBV CPS is changed to +`{MN} = \k.{N}(\n.{M}(\m.mnk))`? 4. What happens when the application rules for the CPS xforms are changed to - [MN] = \k.(\m.mk) - = \k.[M](\m.[N](\n.mnk)) - +
+   [MN] = \k.{M}(\m.m{N}k)
+   {MN} = \k.[M](\m.[N](\n.mnk))
+
Thinking through the types -------------------------- @@ -177,8 +179,8 @@ 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 $sigma; as the result type. The each `k` in -the transform will be a function of type `ρ --> σ` for some +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;