From: Chung-chieh Shan <Chung-chieh Shan ccshan@post.harvard.edu>
Date: Fri, 10 Jun 2011 00:04:51 +0000 (+0200)
Subject: Modifications
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=aa47742f7ab6e132d2afe3dd6703855bfaeb7ecf;ds=sidebyside

Modifications
---

diff --git a/cps.mdwn b/cps.mdwn
index bb478c65..35d0680c 100644
--- a/cps.mdwn
+++ b/cps.mdwn
@@ -71,30 +71,30 @@ 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.)
+target of 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 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
 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:
 
-    [(\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)
+    [(\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)
 
 Because the initial `\k` protects the entire transformed term, 
@@ -102,11 +102,14 @@ 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`.
 
-    [(\x.y)((\x.z)w)] I
-    \k.[\x.y](\m.m[(\x.z)w]k) I
-    [\x.y](\m.m[(\x.z)w] I)
+    [(\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
+     *
     y I
 
 The application to `I` unlocks the leftmost functor.  Because that
@@ -115,28 +118,37 @@ 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
+    {(\x.y)((\x.z)w)} I =
     (\k.{\x.y}(\m.{(\x.z)w}(\n.mnk))) I
-    {\x.y}(\m.{(\x.z)w}(\n.mnI))
+     *
+    {\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)
+     *             *
+    {(\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)))
+     *
+    {\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))
+     *             *
+    {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)
+     *
+    {z}(\n.(\x.{y})nI) =
     (\k.kz)(\n.(\x.{y})nI)
+     *      *
     (\x.{y})zI
-    {y}I
+     *
+    {y}I =
     (\k.ky)I
+     *
     I y
 
 Both xforms make the following guarantee: as long as redexes
@@ -144,7 +156,7 @@ 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:
+Questions and exercises:
 
 1. Why is the CBN xform for variables `[x] = x' instead of something
 involving kappas?  
@@ -177,22 +189,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 &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;
-for functional types a->b, (a->b)' = a' -> (b' -> o) -> o.
+for functional types a->b, (a->b)' = ((a' -> o) -> o) -> (b' -> o) -> o.
 
     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,11 +214,11 @@ 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