context of the lambda calculus can be found here:
[Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf).
Sestoft also provides a lovely on-line lambda evaluator:
-[Sestoft: Lambda calculus reduction workbench]
-(http://www.itu.dk/~sestoft/lamreduce/index.html),
+[Sestoft: Lambda calculus reduction workbench](http://www.itu.dk/~sestoft/lamreduce/index.html),
which allows you to select multiple evaluation strategies,
and to see reductions happen step by step.
Using a Continuation Passing Style transform to control order of evaluation
---------------------------------------------------------------------------
-We'll exhibit and explore the technique of transforming a lambda term
+We'll present a technique for controlling evaluation order by transforming a lambda term
using a Continuation Passing Style transform (CPS), then we'll explore
what the CPS is doing, and how.
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.)
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)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
Both xforms make the following guarantee: as long as redexes
underneath a lambda are never evaluated, there will be at most one
-reduction avaialble at any step in the evaluation.
+reduction available at any step in the evaluation.
That is, all choice is removed from the evaluation process.
Questions and excercises:
involving kappas?
2. Write an Ocaml function that takes a lambda term and returns a
-CPS-xformed lambda term.
+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))'?
+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
--------------------------
CBN xform of a variable appears to be an exception, but instead of
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 `ρ --> σ` for some
+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;