+++ /dev/null
-Here are a bunch of pre-tested operations for the untyped lambda calculus. In some cases multiple versions are offered.
-
-Some of these are drawn from:
-
-* [[!wikipedia Lambda calculus]]
-* [[!wikipedia Church encoding]]
-* Oleg's [Basic Lambda Calculus Terms](http://okmij.org/ftp/Computation/lambda-calc.html#basic)
-
-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
- 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
- let and = \p q. p q p in ; aka S C I
- let or = \p q. p true q in ; or
- let or = \p q. p p q in ; aka M
- let not = \p. p false true in ; or
- let not = \p y n. p n y in ; aka C
- let xor = \p q. p (not q) q in
- let iff = \p q. not (xor p q) in ; or
- let iff = \p q. p q (not q) in
-
- ;; 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
- let make_triple = \x y z f. f x y z in
-
-
- ;; 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
-
- 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
- let mul = \m n s. m (n s) in
- let pow = \b exp. exp (mul b) one in ; or
- ; b succ : adds b
- ; b (b succ) ; adds b b times, ie adds b^2
- ; b (b (b succ)) ; adds b^2 b times, ie adds b^3
- ; 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)
- ; where shift is
- (\p. p (\x y. make_pair (succ x) x)) in ; or
- ; from Oleg; observe that for any Church numeral n: n I ~~> I
- let pred = \n. iszero n zero
- ; else
- (n (\x. x I ; when x is the base term, this will be K zero
- ; when x is a Church numeral, it will be I
- (succ x))
- ; base term
- (K (K zero))
- ) in
- ; 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
- (make_pair true junk)
- ; and build is
- (\p. make_pair false p)
- ; and consume is
- (\p. p get_fst p (p get_snd)) in
- let lt = \m n. not (leq n m) in
- let eq = (\base build consume. \m n. n consume (m build base) get_fst)
- ; 2nd element of a pair will now be of the form (K sthg) or I
- ; we supply the pair being consumed itself as an argument
- ; getting back either sthg or the pair we just consumed
- ; base is
- (make_pair true (K (make_pair false I)))
- ; and build is
- (\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
- ; instead:
- let sub = \m n. n pred m in ; or
- ; how many times we can succ n until m <= result
- let sub = \m n. (\base build. m build base (\cur fin sofar. sofar))
- ; where base is
- (make_triple n false zero)
- ; and build is
- (\t. t (\cur fin sofar. or fin (leq m cur)
- (make_triple cur true sofar) ; enough
- (make_triple (succ cur) false (succ sofar)) ; continue
- )) in
- ; or
- let sub = (\base build consume. \m n. n consume (m build base) get_fst)
- ; where base is
- (make_pair zero I) ; see second defn of eq for explanation of 2nd element
- ; and build is
- (\p. p (\x y. make_pair (succ x) (K p)))
- ; and consume is
- (\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
-
-
- ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x
- ; but unfortunately Y that_function doesn't normalize
- ; instead:
- ; how many times we can sub n from m while n <= result
- let div = \m n. (\base build. m build base (\cur go sofar. sofar))
- ; where base is
- (make_triple m true zero)
- ; and build is
- (\t. t (\cur go sofar. and go (leq n cur)
- (make_triple (sub cur n) true (succ sofar)) ; continue
- (make_triple cur false sofar) ; enough
- )) in
- ; what's left after sub n from m while n <= result
- let mod = \m n. (\base build. m build base (\cur go. cur))
- ; where base is
- (make_pair m true)
- ; and build is
- (\p. p (\cur go. and go (leq n cur)
- (make_pair (sub cur n) true) ; continue
- (make_pair cur false) ; enough
- )) in
-
- ; or
- let divmod = (\base build mtail. \m n.
- (\dhead. m (mtail dhead) (\sel. dhead (sel 0 0)))
- (n build base (\x y z. z junk))
- (\t u x y z. make_pair t u) )
- ; where base is
- (make_triple succ (K 0) I) ; see second defn of eq for explanation of 3rd element
- ; 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
- let div = \n d. divmod n d get_fst in
- let mod = \n d. divmod n d get_snd in
-
-
- ; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x
- ; but unfortunately Y that_function doesn't normalize
-
-
- ; (log base b of m) is a fixedpoint of \x. add (sub (pow b x) m) x
- ; but unfortunately Y that_function doesn't normalize
- ; instead:
- ; how many times we can mul b by b while result <= m
- let log = \m b. (\base build. m build base (\cur go sofar. sofar))
- ; where base is
- (make_triple b true 0)
- ; and build is
- (\t. t (\cur go sofar. and go (leq cur m)
- (make_triple (mul cur b) true (succ sofar)) ; continue
- (make_triple cur false sofar) ; enough
- )) in
-
-
- ;; 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
-
-
- ; now you can search for primes, do encryption :-)
- let gcd = Y (\gcd m n. iszero n m (gcd n (mod m n))) in ; or
- let gcd = \m n. iszero m n (Y (\gcd m n. iszero n m (lt n m (gcd (sub m n) n) (gcd m (sub n m)))) m n) in
- let lcm = \m n. or (iszero m) (iszero n) 0 (mul (div m (gcd m n)) n) 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
-
-<!--
-
- ; numhelper 0 f z ~~> z
- ; when n > 0: numhelper n f z ~~> f (pred n)
- ; compare Bunder/Urbanek pred
- let numhelper = \n. n (\u v. v (u succ)) (K 0) (\p f z. f p) in
-
- ; accepts fixed point combinator as a parameter, so you can use different ones
- let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1) in
-
-
-
- fact Theta 3 ; returns 6
--->
-
-<!--
- ; my original efficient comparisons
- let leq = (\base build consume. \m n. n consume (m build base) get_fst (\x. false) true)
- ; where base is
- (make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair
- ; and build is
- (\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 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)))
- ; and build is
- (\p. p (\x y. make_pair (succ x) (K p)))
- ; and consume is
- (\p. p get_snd p) in ; or
--->
-
-<!--
- gcd
- pow_mod
-
-
- show Oleg's definition of integers:
- church_to_int = \n sign. n
- church_to_negint = \n sign s z. sign (n s z)
-
- ; int_to_church
- abs = \int. int I
-
- sign_case = \int ifpos ifzero ifneg. int (K ifneg) (K ifpos) ifzero
-
- negate_int = \int. sign_case int (church_to_negint (abs int)) zero (church_to_int (abs int))
-
- for more, see http://okmij.org/ftp/Computation/lambda-calc.html#neg
-
-
--->
-
-<!--
-let list_equal =
- \left right. left
- ; here's our f
- (\hd sofar.
- ; deconstruct our sofar-pair
- sofar (\might_be_equal right_tail.
- ; our new sofar
- make_pair
- (and (and might_be_equal (not (isempty right_tail))) (eq? hd (head right_tail)))
- (tail right_tail)
- ))
- ; here's our z
- ; we pass along the fold a pair
- ; (might_for_all_i_know_still_be_equal?, tail_of_reversed_right)
- ; when left is empty, the lists are equal if right is empty
- (make_pair
- true ; for all we know so far, they might still be equal
- (reverse right)
- )
- ; when fold is finished, check sofar-pair
- (\might_be_equal right_tail. and might_be_equal (isempty right_tail))
-
-; most elegant
-let list_equal = \left. left (\hd sofar. \right. and (and (not (isempty right)) (eq hd (head right))) (sofar (tail right))) isempty
-
--->
-