author Chung-chieh Shan Fri, 10 Jun 2011 00:04:51 +0000 (02:04 +0200) committer Chung-chieh Shan Fri, 10 Jun 2011 00:04:51 +0000 (02:04 +0200)
 cps.mdwn patch | blob | history

index bb478c6..35d0680 100644 (file)
--- 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
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`

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.

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:

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,
\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`.

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)
(\k.k(\x.y))(\m.m[(\x.z)w] I)
+     *           *
(\x.y)[(\x.z)w] I
(\x.y)[(\x.z)w] I
+     *
y I

The application to `I` unlocks the leftmost functor.  Because that
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:

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
+    {(\x.y)((\x.z)w)} I =
(\k.{\x.y}(\m.{(\x.z)w}(\n.mnk))) 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))
(\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)
(\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)))
(\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))
(\k.kw)(\n.(\x.{z})n(\n.(\x.{y})nI))
+     *      *
(\x.{z})w(\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)
(\k.kz)(\n.(\x.{y})nI)
+     *      *
(\x.{y})zI
(\x.{y})zI
-    {y}I
+     *
+    {y}I =
(\k.ky)I
(\k.ky)I
+     *
I y

Both xforms make the following guarantee: as long as redexes
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.

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?

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

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

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

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

[M](\m.m[N]k):o
[MN]:(b'->o)->o