changes

[lambda.git] / cps.mdwn

diff --git a/cps.mdwn b/cps.mdwn
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:
 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.
 
 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
 ---------------------------------------------------------------------------
 
 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.
 
 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.  
 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:
 
 
 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
 
 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:
 
 
 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:
 
 
 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
     (\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:
 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
 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,
 
     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
 
 
 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
 --------------------------
 
 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
 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;
 choice of &rho;.
 
 We'll need an ancilliary function ': for any ground type a, a' = a;