changes

[lambda.git] / cps.mdwn

diff --git a/cps.mdwn b/cps.mdwn
index f869b79..6668b48 100644 (file)
--- a/cps.mdwn
+++ b/cps.mdwn
@@ -69,16 +69,16 @@ 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 `\u.(\x.y)z` does not reduce to
 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 `\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
+`\u.z`, because the `\u` 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:
 
 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:
 

-reducing the leftmost lambda first: `(\x.y)((\x.z)w)  ~~> y`
+reducing the leftmost lambda first: `(\x.y)((\x.z)u)  ~~> y`

 
 

-reducing the rightmost lambda first: `(\x.y)((\x.z)w)  ~~> (\x.y)z ~~> y`
+reducing the rightmost lambda first: `(\x.y)((\x.z)u)  ~~> (\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


@@ -91,7 +91,7 @@ Here's the CPS transform defined:
     [\xM] = \k.k(\x[M])
     [MN] = \k.[M](\m.m[N]k)
 
     [\xM] = \k.k(\x[M])
     [MN] = \k.[M](\m.m[N]k)
 

-Here's the result of applying the transform to our problem term:
+Here's the result of applying the transform to our simple example:

 
     [(\x.y)((\x.z)u)] =
     \k.[\x.y](\m.m[(\x.z)u]k) =
 
     [(\x.y)((\x.z)u)] =
     \k.[\x.y](\m.m[(\x.z)u]k) =


@@ -109,13 +109,15 @@ trivial continuation, usually the identity function `I = \x.x`.
     [\x.y](\m.m[(\x.z)u] I) =
     (\k.k(\x.y))(\m.m[(\x.z)u] I)
      *           *
     [\x.y](\m.m[(\x.z)u] I) =
     (\k.k(\x.y))(\m.m[(\x.z)u] I)
      *           *

-    (\x.y)[(\x.z)u] I
+    (\x.y)[(\x.z)u] I           --A--

      *
     y I
 
 The application to `I` unlocks the leftmost functor.  Because that
      *
     y I
 
 The application to `I` unlocks the leftmost functor.  Because that

-functor (`\x.y`) throws away its argument, we never need to expand the
-CPS transform of the argument.
+functor (`\x.y`) throws away its argument (consider the reduction in the
+line marked (A)), we never need to expand the
+CPS transform of the argument.  This means that we never bother to
+reduce redexes inside the argument.

 
 Compare with a call-by-value xform:
 
 
 Compare with a call-by-value xform:
 


@@ -125,7 +127,7 @@ Compare with a call-by-value xform:
 
 This time the reduction unfolds in a different manner:
 
 
 This time the reduction unfolds in a different manner:
 

-    {(\x.y)((\x.z)w)} I =
+    {(\x.y)((\x.z)u)} I =

     (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I
      *
     {\x.y}(\m.{(\x.z)u}(\n.mnI)) =
     (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I
      *
     {\x.y}(\m.{(\x.z)u}(\n.mnI)) =


@@ -140,7 +142,7 @@ This time the reduction unfolds in a different manner:
     {u}(\n.(\x.{z})n(\n.(\x.{y})nI)) =
     (\k.ku)(\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})u(\n.(\x.{y})nI)
+    (\x.{z})u(\n.(\x.{y})nI)       --A--

      *
     {z}(\n.(\x.{y})nI) =
     (\k.kz)(\n.(\x.{y})nI)
      *
     {z}(\n.(\x.{y})nI) =
     (\k.kz)(\n.(\x.{y})nI)


@@ -152,6 +154,9 @@ This time the reduction unfolds in a different manner:
      *
     I y
 
      *
     I y
 

+In this case, the argument does get evaluated: consider the reduction
+in the line marked (A).
+

 Both xforms make the following guarantee: as long as redexes
 underneath a lambda are never evaluated, there will be at most one
 reduction available at any step in the evaluation.
 Both xforms make the following guarantee: as long as redexes
 underneath a lambda are never evaluated, there will be at most one
 reduction available at any step in the evaluation.


@@ -216,9 +221,9 @@ for functional types a->b, (a->b)' = ((a' -> σ) -> σ) -> (b' -> &sig
 
     Terms                            Types
 
 
     Terms                            Types
 

-    [x] = \k.xk                      [a] = (a'->σ)->σ
-    [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->σ)->σ
-    [MN] = \k.[M](\m.m[N]k)          [b] = (b'->σ)->σ
+    [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
 
 Remember that types associate to the right.  Let's work through the
 application xform and make sure the types are consistent.  We'll have


@@ -227,14 +232,14 @@ the following types:
     M:a->b
     N:a
     MN:b 
     M:a->b
     N:a
     MN:b 

-    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'->σ)->σ
+    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

 
 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
 
 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