1 Here are a bunch of pre-tested operations for the untyped lambda calculus. In some cases multiple versions are offered.
4 let true = \y n. y in ; aka K
5 let false = \y n. n in ; aka K I
6 let and = \p q. p q false in ; or
7 let and = \p q. p q p in ; aka S C I
8 let or = \p q. p true q in ; or
9 let or = \p q. p p q in ; aka M
10 let not = \p. p false true in ; or
11 let not = \p y n. p n y in ; aka C
12 let xor = \p q. p (not q) q in
13 let iff = \p q. not (xor p q) in ; or
14 let iff = \p q. p q (not q) in
17 let make_pair = \x y f. f x y in
18 let get_1st = \x y. x in ; aka true
19 let get_2nd = \x y. y in ; aka false
22 let make_triple = \x y z f. f x y z in
25 ; Church numerals: basic operations
27 let zero = \s z. z in ; aka false
28 let one = \s z. s z in ; aka I
29 let succ = \n s z. s (n s z) in
30 ; for any Church numeral n > zero : n (K y) z ~~> y
31 let iszero = \n. n (\x. false) true in
36 let empty = \f z. z in
37 let make_list = \h t f z. f h (t f z) in
38 let isempty = \lst. lst (\h sofar. false) true in
39 let head = \lst. lst (\h sofar. h) junk in
40 let tail_empty = empty in
41 let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) get_2nd)
43 (\h p. p (\t y. make_pair (make_list h t) t)) in
44 let length = \lst. lst (\h sofar. succ sofar) 0 in
45 let map = \f lst. lst (\h sofar. make_list (f h) sofar) empty in
46 let filter = \f lst. lst (\h sofar. f h (make_list h sofar) sofar) empty in ; or
47 let filter = \f lst. lst (\h. f h (make_list h) I) empty in
48 let singleton = \x f z. f x z in
49 ; append [a;b;c] [x;y;z] ~~> [a;b;c;x;y;z]
50 let append = \left right. left make_list right in
51 ; very inefficient but correct reverse
52 let reverse = \lst. lst (\h sofar. append sofar (singleton h)) empty in ; or
53 ; more efficient reverse builds a left-fold instead
54 ; (make_left_list a (make_left_list b (make_left_list c empty)) ~~> \f z. f c (f b (f a z))
55 let reverse = (\make_left_list lst. lst make_left_list empty) (\h t f z. t f (f h z)) in
56 ; zip [a;b;c] [x; y; z] ~~> [(a,x);(b,y);(c,z)]
57 let zip = \left right. (\base build. reverse left build base (\x y. reverse x))
59 (make_pair empty (map (\h u. u h) right))
61 (\h sofar. sofar (\x y. isempty y
63 (make_pair (make_list (\u. head y (u h)) x) (tail y))
65 let all = \f lst. lst (\h sofar. and sofar (f h)) true in
66 let any = \f lst. lst (\h sofar. or sofar (f h)) false in
71 let empty = make_pair true junk in
72 let make_list = \h t. make_pair false (make_pair h t) in
73 let isempty = \lst. lst get_1st in
74 let head = \lst. isempty lst err (lst get_2nd get_1st) in
75 let tail_empty = empty in
76 let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd) in
79 ; more math with Church numerals
81 let add = \m n. m succ n in ; or
82 let add = \m n s z. m s (n s z) in
83 let mul = \m n. m (\z. add n z) zero in ; or
84 let mul = \m n s. m (n s) in
85 let pow = \b exp. exp (mul b) one in ; or
87 ; b (b succ) ; adds b b times, ie adds b^2
88 ; b (b (b succ)) ; adds b^2 b times, ie adds b^3
89 ; exp b succ ; adds b^exp
90 let pow = \b exp s z. exp b s z in
93 ; three strategies for predecessor
94 let pred_zero = zero in
95 let pred = (\shift n. n shift (make_pair zero pred_zero) get_2nd)
97 (\p. p (\x y. make_pair (succ x) x)) in ; or
98 ; from Oleg; observe that for any Church numeral n: n I ~~> I
99 let pred = \n. iszero n zero
101 (n (\x. x I ; when x is the base term, this will be K zero
102 ; when x is a Church numeral, it will be I
107 ; from Bunder/Urbanek
108 let pred = \n s z. n (\u v. v (u s)) (K z) I in ; or
111 ; inefficient but simple comparisons
112 let leq = \m n. iszero (n pred m) in
113 let lt = \m n. not (leq n m) in
114 let eq = \m n. and (leq m n) (leq n m) in ; or
117 ; more efficient comparisons, Oleg's gt provided some simplifications
118 let leq = (\base build consume. \m n. n consume (m build base) get_1st)
120 (make_pair true junk)
122 (\p. make_pair false p)
124 (\p. p get_1st p (p get_2nd)) in
125 let lt = \m n. not (leq n m) in
126 let eq = (\base build consume. \m n. n consume (m build base) get_1st)
127 ; 2nd element of a pair will now be of the form (K sthg) or I
128 ; we supply the pair being consumed itself as an argument
129 ; getting back either sthg or the pair we just consumed
131 (make_pair true (K (make_pair false I)))
133 (\p. make_pair false (K p))
138 ; -n is a fixedpoint of \x. add (add n x) x
139 ; but unfortunately Y that_function doesn't normalize
141 let sub = \m n. n pred m in ; or
142 ; how many times we can succ n until m <= result
143 let sub = \m n. (\base build. m build base (\cur fin sofar. sofar))
145 (make_triple n false zero)
147 (\t. t (\cur fin sofar. or fin (leq m cur)
148 (make_triple cur true sofar) ; enough
149 (make_triple (succ cur) false (succ sofar)) ; continue
152 let sub = (\base build consume. \m n. n consume (m build base) get_1st)
154 (make_pair zero I) ; see second defn of eq for explanation of 2nd element
156 (\p. p (\x y. make_pair (succ x) (K p)))
161 let min = \m n. sub m (sub m n) in
162 let max = \m n. add n (sub m n) in
165 ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x
166 ; but unfortunately Y that_function doesn't normalize
168 ; how many times we can sub n from m while n <= result
169 let div = \m n. (\base build. m build base (\cur go sofar. sofar))
171 (make_triple m true zero)
173 (\t. t (\cur go sofar. and go (leq n cur)
174 (make_triple (sub cur n) true (succ sofar)) ; continue
175 (make_triple cur false sofar) ; enough
177 ; what's left after sub n from m while n <= result
178 let mod = \m n. (\base build. m build base (\cur go. cur))
182 (\p. p (\cur go. and go (leq n cur)
183 (make_pair (sub cur n) true) ; continue
184 (make_pair cur false) ; enough
188 let divmod = (\base build mtail. \m n.
189 (\dhead. m (mtail dhead) (\sel. dhead (sel 0 0)))
190 (n build base (\x y z. z junk))
191 (\t u x y z. make_pair t u) )
193 (make_triple succ (K 0) I) ; see second defn of eq for explanation of 3rd element
195 (\t. make_triple I succ (K t))
197 (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz))))
199 let div = \n d. divmod n d get_1st in
200 let mod = \n d. divmod n d get_2nd in
203 ; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x
204 ; but unfortunately Y that_function doesn't normalize
207 ; (log base b of m) is a fixedpoint of \x. add (sub (pow b x) m) x
208 ; but unfortunately Y that_function doesn't normalize
210 ; how many times we can mul b by b while result <= m
211 let log = \m b. (\base build. m build base (\cur go sofar. sofar))
213 (make_triple b true 0)
215 (\t. t (\cur go sofar. and go (leq cur m)
216 (make_triple (mul cur b) true (succ sofar)) ; continue
217 (make_triple cur false sofar) ; enough
221 ; Rosenbloom's fixed point combinator
222 let Y = \f. (\h. f (h h)) (\h. f (h h)) in
223 ; Turing's fixed point combinator
224 let Theta = (\u f. f (u u f)) (\u f. f (u u f)) in
227 ; length for version 1 lists
228 let length = Y (\self lst. isempty lst 0 (succ (self (tail lst)))) in
231 ; numhelper 0 f z ~~> z
232 ; when n > 0: numhelper n f z ~~> f (pred n)
233 ; compare Bunder/Urbanek pred
234 let numhelper = \n. n (\u v. v (u succ)) (K 0) (\p f z. f p) in
236 ; accepts fixed point combinator as a parameter, so you can use different ones
237 let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1) in
241 fact Theta 3 ; returns 6
245 ; my original efficient comparisons
246 let leq = (\base build consume. \m n. n consume (m build base) get_1st (\x. false) true)
248 (make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair
250 (\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)
253 let lt = \m n. not (leq n m) in
254 let eq = (\base build consume. \m n. n consume (m build base) true (\x. false) true)
256 (make_pair zero (K (make_pair one I)))
258 (\p. p (\x y. make_pair (succ x) (K p)))
260 (\p. p get_2nd p) in ; or
268 show Oleg's definition of integers:
269 church_to_int = \n sign. n
270 church_to_negint = \n sign s z. sign (n s z)
275 sign_case = \int ifpos ifzero ifneg. int (K ifneg) (K ifpos) ifzero
277 negate_int = \int. sign_case int (church_to_negint (abs int)) zero (church_to_int (abs int))
279 for more, see http://okmij.org/ftp/Computation/lambda-arithm-neg.scm