index 73edf0d..bb478c6 100644 (file)
--- 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:

-    <x> => \k.kx
-    <\aM> => \k.k(\a<M>)
-    <MN> => \k.<M>(\m.<N>(\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.<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
+    {(\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 `<MN>
-= \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>(\m.m<N>k)
-    <MN> = \k.[M](\m.[N](\n.mnk))
-
+<pre>
+   [MN] = \k.{M}(\m.m{N}k)
+   {MN} = \k.[M](\m.[N](\n.mnk))
+</pre>

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 `&rho; --> &sigma;` for some
+to a result.  Let's use &sigma; as the result type.  The each `k` in
+the transform will be a function of type &rho; --> &sigma; for some
choice of &rho;.

We'll need an ancilliary function ': for any ground type a, a' = a;