X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=cps.mdwn;h=7f037caa43d4a49107bfea753e546e668b2412ff;hp=605e86a5fc4f038b00dc9cf9444f0fbfe4d52ead;hb=75d46539f289007a9983110854425c3477e85406;hpb=172783a2998a2d2d6a0e1cbda2e4f68710099fe3
diff --git a/cps.mdwn b/cps.mdwn
index 605e86a5..7f037caa 100644
--- a/cps.mdwn
+++ b/cps.mdwn
@@ -1,61 +1,125 @@
-;; call-by-value CPS
-; see Dancy and Filinski, "Representing control: a study of the CPS transformation" (1992)
-; and Sabry, "Note on axiomatizing the semantics of control operators" (1996)
-
-; [x] = var x
-let var = \x (\k. k x) in
-; [\x. body] = lam (\x. [body])
-let lam = \x_body (\k. k (\x. x_body x)) in
-; [M N] = app [M] [N]
-let app = \m n. (\k. m (\m. n (\n. m n k))) in
-
-; helpers
-let app3 = \a b c. app (app a b) c in
-let app4 = \a b c d. app (app (app a b) c) d in
-; [succ] = op1 succ
-let op1 = \op. \u. u (\a k. k (op a)) in
-; [plus] = op2 plus
-let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in
-let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in
-
-;; continuation operators
-; [let/cc k M] = letcc (\k. [M])
-let callcc = \k. k (\f u. (\j. f j u) (\y w. u y)) in
-let letcc = \x_body. app callcc (lam x_body) in
-let letcc = \k_body. \k. (\j. (k_body j) k) (\y w. k y) in
-
-; [abort M] = abort [M]
-let abort = \body. \k. body (\m m) in
-; [prompt M] = prompt [M]
-let prompt = \body. \k. k (body (\m m)) in
-; [shift k M] = shift (\k. [M])
-let shift = \k_body. \k. (\j. (k_body j) (\m m)) (\y w. w (k y)) in
-
-;; examples
-; (+ 100 (let/cc k (+ 10 1))) ~~> 111
-; app3 (op2 plus) (var hundred) (letcc (\k. app3 (op2 plus) (var ten) (var one)))
-
-; (+ 100 (let/cc k (+ 10 (k 1)))) ~~> 101
-; app3 (op2 plus) (var hundred) (letcc (\k. app3 (op2 plus) (var ten) (app (var k) (var one))))
-
-; (+ 100 (+ 10 (abort 1))) ~~> 1
-; app3 (op2 plus) (var hundred) (app3 (op2 plus) (var ten) (abort (var one)))
-
-; (+ 100 (prompt (+ 10 (abort 1)))) ~~> 101
-; app3 (op2 plus) (var hundred) (prompt (app3 (op2 plus) (var ten) (abort (var one))))
-
-; (+ 1000 (prompt (+ 100 (shift k (+ 10 1))))) ~~> 1011
-; app3 (op2 plus) (var thousand) (prompt (app3 (op2 plus) (var hundred) (shift (\k. ((op2 plus) (var ten) (var one))))))
-
-; (+ 1000 (prompt (+ 100 (shift k (k (+ 10 1)))))) ~~> 1111
-; app3 (op2 plus) (var thousand) (prompt (app3 (op2 plus) (var hundred) (shift (\k. (app (var k) ((op2 plus) (var ten) (var one)))))))
-
-; (+ 1000 (prompt (+ 100 (shift k (+ 10 (k 1)))))) ~~> 1111 but added differently
-; app3 (op2 plus) (var thousand) (prompt (app3 (op2 plus) (var hundred) (shift (\k. ((op2 plus) (var ten) (app (var k) (var one)))))))
-
-; (+ 100 ((prompt (+ 10 (shift k k))) 1)) ~~> 111
-; app3 (op2 plus) (var hundred) (app (prompt (app3 (op2 plus) (var ten) (shift (\k. (var k))))) (var one))
-
-; (+ 100 (prompt (+ 10 (shift k (k (k 1)))))) ~~> 121
-; app3 (op2 plus) (var hundred) (prompt (app3 (op2 plus) (var ten) (shift (\k. app (var k) (app (var k) (var one))))))
+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!