author Chris Barker Fri, 10 Jun 2011 18:52:19 +0000 (14:52 -0400) committer Chris Barker Fri, 10 Jun 2011 18:52:19 +0000 (14:52 -0400)
 cps.mdwn patch | blob | history

index 35d0680..f869b79 100644 (file)
--- a/cps.mdwn
+++ b/cps.mdwn
@@ -18,8 +18,8 @@ Evaluation order matters

We've seen this many times.  For instance, consider the following
reductions.  It will be convenient to use the abbreviation `w =

We've seen this many times.  For instance, consider the following
reductions.  It will be convenient to use the abbreviation `w =
-\x.xx`.  I'll indicate which lambda is about to be reduced with a *
-underneath:
+\x.xx`.  I'll
+indicate which lambda is about to be reduced with a * underneath:

<pre>
(\x.y)(ww)

<pre>
(\x.y)(ww)
@@ -68,10 +68,11 @@ 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.

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 reduction.)
+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
+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:

Start with a simple form that has two different reduction paths:

@@ -92,23 +93,23 @@ Here's the CPS transform defined:

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) =
-    \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.mwk))k)
+    [(\x.y)((\x.z)u)] =
+    \k.[\x.y](\m.m[(\x.z)u]k) =
+    \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[u]k))k) =
+    \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.muk))k)

-Because the initial `\k` protects the entire transformed term,
-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`.
+Because the initial `\k` protects (i.e., takes scope over) the entire
+transformed term, we can't perform any reductions.  In order to watch
+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)((\x.z)u)] I =
+    (\k.[\x.y](\m.m[(\x.z)u]k)) I
*
*
-    [\x.y](\m.m[(\x.z)w] I) =
-    (\k.k(\x.y))(\m.m[(\x.z)w] I)
+    [\x.y](\m.m[(\x.z)u] I) =
+    (\k.k(\x.y))(\m.m[(\x.z)u] I)
*           *
*           *
-    (\x.y)[(\x.z)w] I
+    (\x.y)[(\x.z)u] I
*
y I

*
y I

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

{(\x.y)((\x.z)w)} I =
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
+    (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I
*
*
-    {\x.y}(\m.{(\x.z)w}(\n.mnI)) =
-    (\k.k(\x.{y}))(\m.{(\x.z)w}(\n.mnI))
+    {\x.y}(\m.{(\x.z)u}(\n.mnI)) =
+    (\k.k(\x.{y}))(\m.{(\x.z)u}(\n.mnI))
*             *
*             *
-    {(\x.z)w}(\n.(\x.{y})nI) =
-    (\k.{\x.z}(\m.{w}(\n.mnk)))(\n.(\x.{y})nI)
+    {(\x.z)u}(\n.(\x.{y})nI) =
+    (\k.{\x.z}(\m.{u}(\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)))
+    {\x.z}(\m.{u}(\n.mn(\n.(\x.{y})nI))) =
+    (\k.k(\x.{z}))(\m.{u}(\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))
+    {u}(\n.(\x.{z})n(\n.(\x.{y})nI)) =
+    (\k.ku)(\n.(\x.{z})n(\n.(\x.{y})nI))
*      *
*      *
-    (\x.{z})w(\n.(\x.{y})nI)
+    (\x.{z})u(\n.(\x.{y})nI)
*
{z}(\n.(\x.{y})nI) =
(\k.kz)(\n.(\x.{y})nI)
*
{z}(\n.(\x.{y})nI) =
(\k.kz)(\n.(\x.{y})nI)
@@ -156,27 +157,40 @@ 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.

+Now let's verify that the CBN CPS avoids the infinite reduction path
+discussed above (remember that `w = \x.xx`):
+
+    [(\x.y)(ww)] I =
+    (\k.[\x.y](\m.m[ww]k)) I
+     *
+    [\x.y](\m.m[ww]I) =
+    (\k.k(\x.y))(\m.m[ww]I)
+     *             *
+    (\x.y)[ww]I
+     *
+    y I
+
+
Questions and exercises:

Questions and exercises:

-1. Why is the CBN xform for variables `[x] = x' instead of something
+1. Prove that {(\x.y)(ww)} does not terminate.
+
+2. Why is the CBN xform for variables `[x] = x' instead of something
involving kappas?

involving kappas?

-2. Write an Ocaml function that takes a lambda term and returns a
+3. Write an Ocaml function that takes a lambda term and returns a
CPS-xformed lambda term.  You can use the following data declaration:

type form = Var of char | Abs of char * form | App of form * form;;

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))`?
+4. The discussion above talks about the "leftmost" redex, or the
+"rightmost".  But these words apply accurately only in a special set
+of terms.  Characterize the order of evaluation for CBN (likewise, for
+CBV) more completely and carefully.

-4. What happens when the application rules for the CPS xforms are changed to
+5. What happens (in terms of evaluation order) when the application
+rule for CBV CPS is changed to `{MN} = \k.{N}(\n.{M}(\m.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
--------------------------
@@ -196,15 +210,15 @@ 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;
-for functional types a->b, (a->b)' = ((a' -> o) -> o) -> (b' -> o) -> o.
+for functional types a->b, (a->b)' = ((a' -> &sigma;) -> &sigma;) -> (b' -> &sigma;) -> &sigma;.

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'->&sigma;)->&sigma;
+    [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->&sigma;)->&sigma;
+    [MN] = \k.[M](\m.m[N]k)          [b] = (b'->&sigma;)->&sigma;

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
@@ -213,16 +227,19 @@ the following types:
M:a->b
N:a
MN:b
M:a->b
N:a
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
-
-Note that even though the transform uses the same symbol for the
-translation of a variable, in general it will have a different type in
-the transformed term.
-
+    k:b'->&sigma;
+    [N]:(a'->&sigma;)->&sigma;
+    m:((a'->&sigma;)->&sigma;)->(b'->&sigma;)->&sigma;
+    m[N]:(b'->&sigma;)->&sigma;
+    m[N]k:&sigma;
+    [M]:((a->b)'->&sigma;)->&sigma; = ((((a'->&sigma;)->&sigma;)->(b'->&sigma;)->&sigma;)->&sigma;)->&sigma;
+    [M](\m.m[N]k):&sigma;
+    [MN]:(b'->&sigma;)->&sigma;
+
+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
+in the transformed term will have a different type than in the source
+term.
+
+Excercise: what should the function ' be for the CBV xform?  Hint: