+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 make_triple = \x y z f. f x y z in
- ; Church numerals
+ ; Church numerals: basic operations
+
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_2nd)
+ ; 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
+ ; 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_1st in
+ let head = \lst. isempty lst err (lst get_2nd get_1st) in
+ let tail_empty = empty in
+ let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd) 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
; 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_2nd)
let eq = \m n. and (leq m n) (leq n m) in ; or
- ; more efficient comparisons
- let leq = (\base build consume. \m n. n consume (m build base) get_1st (\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_2nd 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_2nd p) in ; or
-
-
- ; more efficient comparisons, Oleg's gt provided some simplification
+ ; more efficient comparisons, Oleg's gt provided some simplifications
let leq = (\base build consume. \m n. n consume (m build base) get_1st)
; where base is
(make_pair true junk)
; and consume is
(\p. p get_2nd p) in
+
; -n is a fixedpoint of \x. add (add n x) x
; but unfortunately Y that_function doesn't normalize
; instead:
; and consume is
(\p. p get_2nd 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:
let div = \n d. divmod n d get_1st in
let mod = \n d. divmod n d get_2nd 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:
(make_triple cur false sofar) ; enough
)) in
- ; Curry's fixed point combinator
+
+ ; Rosenbloom's fixed point combinator
let Y = \f. (\h. f (h h)) (\h. f (h h)) in
; Turing's fixed point combinator
- let Z = (\u f. f (u u f)) (\u f. f (u u f)) in
-
-
+ let Theta = (\u f. f (u u f)) (\u f. f (u u f)) 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 = \lst. (\shift lst. lst shift (make_pair empty junk) get_2nd)
- ; where shift is
- (\h p. p (\t y. make_pair (make-list h t) t)) in
- let length = \lst. lst (\h sofar. succ sofar) zero 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
-
-
- ; 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_1st in
- let head = \lst. isempty lst error (lst get_2nd get_1st) in
- let tail_empty = empty in
- let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd) in
-
+ ; length for version 1 lists
let length = Y (\self lst. isempty lst 0 (succ (self (tail lst)))) in
+ true
+
+<!--
; numhelper 0 f z ~~> z
; when n > 0: numhelper n f z ~~> f (pred n)
let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1) in
- fact Z 3 ; returns 6
+
+ fact Theta 3 ; returns 6
+-->
+
+<!--
+ ; my original efficient comparisons
+ let leq = (\base build consume. \m n. n consume (m build base) get_1st (\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_2nd 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_2nd 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
+-->