From: Chris Barker Date: Sun, 17 Oct 2010 16:11:04 +0000 (-0400) Subject: changes to offsite-reading X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=fa5f84861179e2ffcc16dfadffbd4b1c4f01c5df;hp=b059b718b62f3b4beffb3bd7fbe66af01069f9c9 changes to offsite-reading --- diff --git a/hints/assignment_4_hint_3_alternate_1.mdwn b/hints/assignment_4_hint_3_alternate_1.mdwn new file mode 100644 index 00000000..f75bad0e --- /dev/null +++ b/hints/assignment_4_hint_3_alternate_1.mdwn @@ -0,0 +1,58 @@ +Alternate strategy for Y1, Y2 + +* This is (in effect) the strategy used by OCaml. The mutually recursive: + + let rec + f x = A ; A may refer to f or g + and + g y = B ; B may refer to f or g + in + C + + is implemented using regular, non-mutual recursion, like this (`u` is a variable not occurring free in `A`, `B`, or `C`): + + let rec u g x = (let f = u g in A) in + let rec g y = (let f = u g in B) in + let f = u g in + C + + or, expanded into the form we've been working with: + + let u = Y (\u g. (\f x. A) (u g)) in + let g = Y ( \g. (\f y. B) (u g)) in + let f = u g in + C + + We could abstract Y1 and Y2 combinators from this as follows: + + let Yu = \ff. Y (\u g. ff ( u g ) g) in + let Y2 = \ff gg. Y ( \g. gg (Yu ff g ) g) in + let Y1 = \ff gg. (Yu ff) (Y2 ff gg) in + let f = Y1 (\f g. A) (\f g. B) in + let g = Y2 (\f g. A) (\f g. B) in + C + + +* Here's the same strategy extended to three mutually-recursive functions. `f`, `g` and `h`: + + let v = Y (\v g h. (\f x. A) (v g h)) in + let w = Y ( \w h. (\g. (\f y. B) (v g h)) (w h)) in + let h = Y ( \h. (\g. (\f z. C) (v g h)) (w h)) in + let g = w h in + let f = v g h in + D + + + diff --git a/lambda_library.mdwn b/lambda_library.mdwn index 423ad596..e170dcf4 100644 --- a/lambda_library.mdwn +++ b/lambda_library.mdwn @@ -12,7 +12,7 @@ and all sorts of other places. Others of them are our own handiwork. **Spoilers!** Below you'll find implementations of map and filter for v3 lists, and several implementations of leq for Church numerals. Those were all requested in Assignment 2; so if you haven't done that yet, you should try to figure them out on your own. (You can find implementations of these all over the internet, if you look for them, so these are no great secret. In fact, we'll be delighted if you're interested enough in the problem to try to think through alternative implementations.) - ; booleans + ;; booleans let true = \y n. y in ; aka K let false = \y n. n in ; aka K I let and = \p q. p q false in ; or @@ -25,75 +25,20 @@ and all sorts of other places. Others of them are our own handiwork. let iff = \p q. not (xor p q) in ; or let iff = \p q. p q (not q) in - ; pairs + ;; tuples let make_pair = \x y f. f x y in let get_fst = \x y. x in ; aka true let get_snd = \x y. y in ; aka false - - ; triples let make_triple = \x y z f. f x y z in - ; Church numerals: basic operations - + ;; Church numerals let zero = \s z. z in ; aka false let one = \s z. s z in ; aka I let succ = \n s z. s (n s z) in ; for any Church numeral n > zero : n (K y) z ~~> y let iszero = \n. n (\x. false) true in - - ; version 3 lists - - let empty = \f z. z in - let make_list = \h t f z. f h (t f z) in - let isempty = \lst. lst (\h sofar. false) true in - let head = \lst. lst (\h sofar. h) junk in - let tail_empty = empty in - let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) get_snd) - ; where shift is - (\h p. p (\t y. make_pair (make_list h t) t)) in - let length = \lst. lst (\h sofar. succ sofar) 0 in - let map = \f lst. lst (\h sofar. make_list (f h) sofar) empty in - let filter = \f lst. lst (\h sofar. f h (make_list h sofar) sofar) empty in ; or - let filter = \f lst. lst (\h. f h (make_list h) I) empty in - let singleton = \x f z. f x z in - ; append [a;b;c] [x;y;z] ~~> [a;b;c;x;y;z] - let append = \left right. left make_list right in - ; very inefficient but correct reverse - let reverse = \lst. lst (\h sofar. append sofar (singleton h)) empty in ; or - ; more efficient reverse builds a left-fold instead - ; make_left_list a (make_left_list b (make_left_list c empty)) ~~> \f z. f c (f b (f a z)) - let reverse = (\make_left_list lst. lst make_left_list empty) (\h t f z. t f (f h z)) in - ; from Oleg, of course it's the most elegant - ; revappend [a;b;c] [x;y] ~~> [c;b;a;x;y] - let revappend = \left. left (\hd sofar. \right. sofar (make_list hd right)) I in - let rev = \lst. revappend lst empty in - ; zip [a;b;c] [x;y;z] ~~> [(a,x);(b,y);(c,z)] - let zip = \left right. (\base build. reverse left build base (\x y. reverse x)) - ; where base is - (make_pair empty (map (\h u. u h) right)) - ; and build is - (\h sofar. sofar (\x y. isempty y - sofar - (make_pair (make_list (\u. head y (u h)) x) (tail y)) - )) in - let all = \f lst. lst (\h sofar. and sofar (f h)) true in - let any = \f lst. lst (\h sofar. or sofar (f h)) false in - - - ; version 1 lists - - let empty = make_pair true junk in - let make_list = \h t. make_pair false (make_pair h t) in - let isempty = \lst. lst get_fst in - let head = \lst. isempty lst err (lst get_snd get_fst) in - let tail_empty = empty in - let tail = \lst. isempty lst tail_empty (lst get_snd get_snd) in - - - ; more math with Church numerals - let add = \m n. m succ n in ; or let add = \m n s z. m s (n s z) in let mul = \m n. m (\z. add n z) zero in ; or @@ -105,7 +50,6 @@ and all sorts of other places. Others of them are our own handiwork. ; exp b succ ; adds b^exp let pow = \b exp s z. exp b s z in - ; three strategies for predecessor let pred_zero = zero in let pred = (\shift n. n shift (make_pair zero pred_zero) get_snd) @@ -123,13 +67,11 @@ and all sorts of other places. Others of them are our own handiwork. ; from Bunder/Urbanek let pred = \n s z. n (\u v. v (u s)) (K z) I in ; or - ; inefficient but simple comparisons let leq = \m n. iszero (n pred m) in let lt = \m n. not (leq n m) in let eq = \m n. and (leq m n) (leq n m) in ; or - ; more efficient comparisons, Oleg's gt provided some simplifications let leq = (\base build consume. \m n. n consume (m build base) get_fst) ; where base is @@ -149,7 +91,7 @@ and all sorts of other places. Others of them are our own handiwork. (\p. make_pair false (K p)) ; and consume is (\p. p get_snd p) in - + ; -n is a fixedpoint of \x. add (add n x) x ; but unfortunately Y that_function doesn't normalize @@ -174,8 +116,8 @@ and all sorts of other places. Others of them are our own handiwork. (\p. p get_snd p) in - let min = \m n. sub m (sub m n) in - let max = \m n. add n (sub m n) in + let min = \m n. sub m (sub m n) in + let max = \m n. add n (sub m n) in ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x @@ -210,8 +152,7 @@ and all sorts of other places. Others of them are our own handiwork. ; and build is (\t. make_triple I succ (K t)) ; and mtail is - (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz)))) - in + (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz)))) in let div = \n d. divmod n d get_fst in let mod = \n d. divmod n d get_snd in @@ -234,9 +175,10 @@ and all sorts of other places. Others of them are our own handiwork. )) in - ; Rosenbloom's fixed point combinator - let Y = \f. (\h. f (h h)) (\h. f (h h)) in - ; Turing's fixed point combinator + ;; fixed point combinators + ; Curry/Rosenbloom's + let Y = \f. (\h. f (h h)) (\h. f (h h)) in + ; Turing's let Theta = (\u f. f (u u f)) (\u f. f (u u f)) in @@ -246,8 +188,121 @@ and all sorts of other places. Others of them are our own handiwork. let lcm = \m n. or (iszero m) (iszero n) 0 (mul (div m (gcd m n)) n) in - ; length for version 1 lists - let length = Y (\self lst. isempty lst 0 (succ (self (tail lst)))) in + ;; version 1 lists + let empty = make_pair true junk in + let make_list = \h t. make_pair false (make_pair h t) in + let isempty = \lst. lst get_fst in + let head = \lst. isempty lst err (lst get_snd get_fst) in + let tail_empty = empty in + let tail = \lst. isempty lst tail_empty (lst get_snd get_snd) in + + let length = Y (\length lst. isempty lst 0 (succ (length (tail lst)))) in + let fold = Y (\fold lst f z. isempty lst z (f (head lst) (fold (tail lst) f z))) in + let map = \f. Y (\map lst. isempty lst empty (make_list (f (head lst)) (map (tail lst)))) in + let filter = \f. Y (\filter lst. isempty lst empty (f (head lst) (make_list (head lst)) I (filter (tail lst)))) in + + + ;; version 3 (right-fold) lists + let empty = \f z. z in + let make_list = \h t f z. f h (t f z) in + let isempty = \lst. lst (\h sofar. false) true in + let head = \lst. lst (\h sofar. h) err in + let tail_empty = empty in + let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) get_snd) + ; where shift is + (\h p. p (\t y. make_pair (make_list h t) t)) in + let length = \lst. lst (\h sofar. succ sofar) 0 in + let map = \f lst. lst (\h sofar. make_list (f h) sofar) empty in + let filter = \f lst. lst (\h sofar. f h (make_list h sofar) sofar) empty in ; or + let filter = \f lst. lst (\h. f h (make_list h) I) empty in + let singleton = \x f z. f x z in + ; append [a;b;c] [x;y;z] ~~> [a;b;c;x;y;z] + let append = \left right. left make_list right in + ; very inefficient but correct reverse + let reverse = \lst. lst (\h sofar. append sofar (singleton h)) empty in ; or + ; more efficient revappend, reverse + ; revappend [a;b;c] [x;y] ~~> [c;b;a;x;y] + ; make_left_list a (make_left_list b (make_left_list c empty)) ~~> \f z. f c (f b (f a z)) + let revappend = (\make_left_lst left right. left make_left_list right) (\h t f z. t f (f h z)) in + ; from Oleg, of course it's the most elegant + let revappend = \left. left (\hd sofar. \right. sofar (make_list hd right)) I in + let rev = \lst. revappend lst empty in + ; zip [a;b;c] [x;y;z] ~~> [(a,x);(b,y);(c,z)] + let zip = \left right. (\base build. reverse left build base (\x y. reverse x)) + ; where base is + (make_pair empty (map (\h u. u h) right)) + ; and build is + (\h sofar. sofar (\x y. isempty y + sofar + (make_pair (make_list (\u. head y (u h)) x) (tail y)) + )) in + let all = \f lst. lst (\h sofar. and sofar (f h)) true in + let any = \f lst. lst (\h sofar. or sofar (f h)) false in + + + ;; left-fold lists + let make_list = \h t f z. t f (f h z) in + let head = \lst. lst (\h sofar. (K (sofar (K h))) ) (\k. k err) I in + let tail = \lst. (\shift. lst shift (\a b. a tail_empty) I I) + (\h p. p (\j a b. b empty) (\t a b. b (\f z. f h (t f z))) ) in + + + ;; version 5 (CPS right-fold) lists + ; [] is \f z c a. c z + ; [1] is \f z c a. f 1 z c a + ; [1;2] is \f z c a. f 2 z (\z. f 1 z c a) a + ; [1;2;3] is \f z c a. f 3 z (\z. f 2 z (\z. f 1 z c a) a) a + let empty = \f2 z continue_handler abort_handler. continue_handler z in + let isempty = \lst larger_computation. lst + ; here's our f2 + (\hd sofar continue_handler abort_handler. abort_handler false) + ; here's our z + true + ; here's the continue_handler for the leftmost application of f2 + larger_computation + ; here's the abort_handler + larger_computation in + let make_list = \h t. \f2 z continue_handler abort_handler. + t f2 z (\sofar. f2 h sofar continue_handler abort_handler) abort_handler in + let head = \lst larger_computation. lst + ; here's our f2 + (\hd sofar continue_handler abort_handler. continue_handler hd) + ; here's our z + err + ; here are our continue_handler and abort_handler + larger_computation unused in + let tail_empty = empty in + let tail = \lst larger_computation. lst + ; here's our f2 + (\h sofar continue_handler abort_handler. continue_handler (sofar (\t y. make_pair (make_list h t) t))) + ; here's our z + (make_pair empty tail_empty) + ; here are our continue_handler and abort_handler + (\sofar. sofar (\x y. larger_computation y)) unused in + + ;; CPS left-fold lists + ; [] is \f z c a. c z + ; [1] is \f z c a. f 1 z (\z. c z) a + ; [1;2] is \f z c a. f 1 z (\z. f 2 z (\z. c z) a) a + ; [1;2;3] is \f z c a. f 1 z (\z. f 2 z (\z. f 3 z (\z. c z) a) a) a + let make_right_list = make_list in + let make_list = \h t. \f2 z continue_handler abort_handler. + f2 h z (\z. t f2 z continue_handler abort_handler) abort_handler in + let head = \lst larger_computation. lst + ; here's our f2 + (\hd sofar continue_handler abort_handler. abort_handler hd) + ; here's our z + err + ; here are our continue_handler and abort_handler + larger_computation larger_computation in + let tail = \lst larger_computation. lst + ; here's our f2 + (\h sofar continue_handler abort_handler. continue_handler (sofar (\j a b. b empty) (\t a b. b (make_right_list h t)) ) ) + ; here's our z + (\a b. a tail_empty) + ; here are our continue_handler and abort_handler + (\sofar. sofar larger_computation larger_computation) unused in + true @@ -276,7 +331,7 @@ and all sorts of other places. Others of them are our own handiwork. (\p. p (\x y. make_pair (succ x) (K p))) ; supplying the made pair as an arg to its 2nd term returns p (the previous pair) ; and consume is (\p. p get_snd p) in - let lt = \m n. not (leq n m) in + let lt = \m n. not (leq n m) in let eq = (\base build consume. \m n. n consume (m build base) true (\x. false) true) ; where base is (make_pair zero (K (make_pair one I))) diff --git a/offsite_reading.mdwn b/offsite_reading.mdwn index d9c7f826..b82bd4bf 100644 --- a/offsite_reading.mdwn +++ b/offsite_reading.mdwn @@ -66,6 +66,11 @@ get more out of. (Rinse and repeat.) * [Chris Barker's Iota and Jot](http://semarch.linguistics.fas.nyu.edu/barker/Iota/)

+* [To Dissect a Mockingbird](http://dkeenan.com/Lambda/index.htm) +* [Combinator Birds](http://www.angelfire.com/tx4/cus/combinator/birds.html) +* [Les deux combinateurs et la totalite](http://www.paulbraffort.net/j_et_i/j_et_i.html) by Paul Braffort. + + ## Evaluation Order ## * [[!wikipedia Evaluation strategy]] @@ -94,6 +99,7 @@ get more out of. (Rinse and repeat.) * [The Y Combinator](http://dangermouse.brynmawr.edu/cs245/ycomb_jim.html) derives the applicative-order Y-combinator from scratch, in Scheme. This derivation is similar in flavor to the derivation found in The Little Schemer, but uses a slightly different starting approach... + ## Types ## * [[!wikipedia Tagged union]] diff --git a/week4.mdwn b/week4.mdwn index 49a2c1f0..ab4411fe 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -520,12 +520,11 @@ but really all we're in a position to mean by that are claims about the result of the complex expression semantically depending only on this, not on that. A demon evaluator who custom-picked the evaluation order to make things maximally bad for you could ensure that all the semantically unnecessary computations got -evaluated anyway. We don't have any way to prevent that. Later, -we'll see ways to *semantically guarantee* one evaluation order rather than -another. Though even then the demonic evaluation-order-chooser could make it -take unnecessarily long to compute the semantically guaranteed result. Of -course, in any real computing environment you'll know you're dealing with a -fixed evaluation order and you'll be able to program efficiently around that. +evaluated anyway. We don't yet know any way to prevent that. Later, we'll see +ways to *semantically guarantee* one evaluation order rather than another. Of +course, in any real computing environment you'll know in advance that you're +dealing with a fixed evaluation order and you'll be able to program efficiently +around that. In detail, then, here's what our v5 lists will look like: