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,
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
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
- (\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
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?
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
- [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
--------------------------
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 σ as the result type. The each `k` in
the transform will be a function of type ρ --> σ for some
choice of ρ.
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
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