Here are a bunch of pre-tested operations for the untyped lambda calculus. In some cases multiple versions are offered.
; 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
; pairs
let make_pair = \x y f. f x y in
let get_1st = \x y. x in ; aka true
let get_2nd = \x y. y in ; aka false
; triples
let make_triple = \x y z f. f x y z 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
; Church numerals: easy 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
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_2nd)
; 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_1st)
; where base is
(make_pair true junk)
; and build is
(\p. make_pair false p)
; and consume is
(\p. p get_1st p (p get_2nd)) in
let lt = \m n. not (leq n m) in
let eq = (\base build consume. \m n. n consume (m build base) get_1st)
; 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_2nd 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_1st)
; 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_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:
; 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_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:
; 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
; Curry'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
; length for version 1 lists
let length = Y (\self lst. isempty lst 0 (succ (self (tail lst)))) in
; 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 Z 3 ; returns 6