From: Chris Barker Date: Wed, 8 Jun 2011 18:16:39 +0000 (-0400) Subject: added little file on cpsX X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=75d46539f289007a9983110854425c3477e85406 added little file on cpsX --- diff --git a/cps.mdwn b/cps.mdwn new file mode 100644 index 00000000..7f037caa --- /dev/null +++ b/cps.mdwn @@ -0,0 +1,125 @@ +Gaining control over order of evaluation +---------------------------------------- + +We know that evaluation order matters. We're beginning to learn how +to gain some control over order of evaluation (think of Jim's abort handler). +We continue to reason about order of evaluation. + +A superbly clear and lucid discussion can be found here: +[Sestoft: Demonstrating Lambda Calculus Reduction](http://tinyurl.com/27nd3ub). +Sestoft also provides a really lovely lambda evaluator, +which allows you to select multiple evaluation strategies, +and to see reductions happen step by step: +[Sestoft's lambda reduction webpage](http://ellemose.dina.kvl.dk/~sestoft/lamreduce/lamframes.html). + + +Evaluation order matters +------------------------ + +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.y)(ww)
+ *
+y
+```
+ +Done! We have a normal form. But if we reduce using a different +strategy, things go wrong: + +
```+(\x.y)(ww) =
+(\x.y)((\x.xx)w) =
+        *
+(\x.y)(ww) =
+(\x.y)((\x.xx)w) =
+        *
+(\x.y)(ww)
+```
+ +Etc. + +As a second reminder of when evaluation order matters, consider using +`Y = \f.(\h.f(hh))(\h.f(hh))` as a fixed point combinator to define a recursive function: + +
```+Y (\f n. blah) =
+(\f.(\h.f(hh))(\h.f(hh))) (\f n. blah)
+     *
+(\f.f((\h.f(hh))(\h.f(hh)))) (\f n. blah)
+       *
+(\f.f(f((\h.f(hh))(\h.f(hh))))) (\f n. blah)
+         *
+(\f.f(f(f((\h.f(hh))(\h.f(hh)))))) (\f n. blah)
+```
+ +And we never get the recursion off the ground. + + +Restricting evaluation: call by name, call by value +--------------------------------------------------- + +One way to begin to gain some control is by adjusting our notion of +beta reduction. This strategy has some of the flavor of adding types, +but is actually a part of the untyped calculus. + +In order to have a precise discussion, we'll need some vocabulary. +We've been talking about normal form (lambda terms that can't be +further reduced), and leftmost evaluation (the reduction strategy of +always choosing the left most reducible lambda); we'll need to refine +both of those concepts. + +Kinds of normal form: +--------------------- + +Recall that there are three kinds of lambda term. Let `a` be an +arbitrary variable, and let `M` and `N` be arbitrary terms: + +
```+The pure untyped lambda calculus (again):
+
+             Form     Examples
+Variable     a        x, y, z
+Abstract     \aM      \x.x, \x.y, \x.\y.y
+Application  MN       (x x), ((\x.x) y), ((\x.x)(\y.y))
+```
+ +It will be helpful to define a *redex*, which is a lambda term of +the form `((\aM) N)`. That is, a redex is a form for which beta +reduction is defined (ignoring, as usual, the manouvering required in +order to avoid variable collision). + +It will also be helpful to have names for the two components of an +application `(M N)`: we'll call `M` the *functor*, and `N` the +*argument*. Note that functor position can be occupied by a variable, +since `x` is in the functor position of the term `(x y)`. + +Ok, with that vocabulary, we can distinguish four different types of +normal form: + + + + + + + +Take Plotkin's CBN CPS: + +[x] ~~> x +[\xM] ~~> \k.k(\x[M]) +[MN] ~~> \k.[M](\m.m[N]k) + +let w = \x.xx in + +[(\xy)(ww)] ~~> +\k.[\xy](\m.m[ww]k) ~~> +\k.[\xy](\m.m(\k.[w](\m.m[w]k))k) ~~> +\k.[\xy](\m.m(\k.(\k.k(\x[xx]))(\m.m[w]k))k) ~~> beta* +\k.[\xy](\m.m(\k.(\x[xx])[w]k)k) ~~> +\k.[\xy](\m.m(\k.(\x(\k.[x](\m.m[x]k)))[w]k)k) ~~> +\k.[\xy](\m.m(\k.(\x(\k.x(\m.mxk)))[w]k)k) ~~> beta +\k.[\xy](\m.m(\k.[w](\m.m[w]k))k) --- same as second line! +