1 Here are a bunch of pre-tested operations for the untyped lambda calculus. In some cases multiple versions are offered.
3 Some of these are drawn from:
5 * [[!wikipedia Lambda calculus]]
6 * [[!wikipedia Church encoding]]
7 * Oleg's [Basic Lambda Calculus Terms](http://okmij.org/ftp/Computation/lambda-calc.html#basic)
9 and all sorts of other places. Others of them are our own handiwork.
12 **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.)
16 let true = \y n. y in ; aka K
17 let false = \y n. n in ; aka K I
18 let and = \p q. p q false in ; or
19 let and = \p q. p q p in ; aka S C I
20 let or = \p q. p true q in ; or
21 let or = \p q. p p q in ; aka M
22 let not = \p. p false true in ; or
23 let not = \p y n. p n y in ; aka C
24 let xor = \p q. p (not q) q in
25 let iff = \p q. not (xor p q) in ; or
26 let iff = \p q. p q (not q) in
29 let make_pair = \x y f. f x y in
30 let get_fst = \x y. x in ; aka true
31 let get_snd = \x y. y in ; aka false
34 let make_triple = \x y z f. f x y z in
37 ; Church numerals: basic operations
39 let zero = \s z. z in ; aka false
40 let one = \s z. s z in ; aka I
41 let succ = \n s z. s (n s z) in
42 ; for any Church numeral n > zero : n (K y) z ~~> y
43 let iszero = \n. n (\x. false) true in
48 let empty = \f z. z in
49 let make_list = \h t f z. f h (t f z) in
50 let isempty = \lst. lst (\h sofar. false) true in
51 let head = \lst. lst (\h sofar. h) junk in
52 let tail_empty = empty in
53 let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) get_snd)
55 (\h p. p (\t y. make_pair (make_list h t) t)) in
56 let length = \lst. lst (\h sofar. succ sofar) 0 in
57 let map = \f lst. lst (\h sofar. make_list (f h) sofar) empty in
58 let filter = \f lst. lst (\h sofar. f h (make_list h sofar) sofar) empty in ; or
59 let filter = \f lst. lst (\h. f h (make_list h) I) empty in
60 let singleton = \x f z. f x z in
61 ; append [a;b;c] [x;y;z] ~~> [a;b;c;x;y;z]
62 let append = \left right. left make_list right in
63 ; very inefficient but correct reverse
64 let reverse = \lst. lst (\h sofar. append sofar (singleton h)) empty in ; or
65 ; more efficient reverse builds a left-fold instead
66 ; make_left_list a (make_left_list b (make_left_list c empty)) ~~> \f z. f c (f b (f a z))
67 let reverse = (\make_left_list lst. lst make_left_list empty) (\h t f z. t f (f h z)) in
68 ; from Oleg, of course it's the most elegant
69 ; revappend [a;b;c] [x;y] ~~> [c;b;a;x;y]
70 let revappend = \left. left (\hd sofar. \right. sofar (make_list hd right)) I in
71 let rev = \lst. revappend lst empty in
72 ; zip [a;b;c] [x;y;z] ~~> [(a,x);(b,y);(c,z)]
73 let zip = \left right. (\base build. reverse left build base (\x y. reverse x))
75 (make_pair empty (map (\h u. u h) right))
77 (\h sofar. sofar (\x y. isempty y
79 (make_pair (make_list (\u. head y (u h)) x) (tail y))
81 let all = \f lst. lst (\h sofar. and sofar (f h)) true in
82 let any = \f lst. lst (\h sofar. or sofar (f h)) false in
87 let empty = make_pair true junk in
88 let make_list = \h t. make_pair false (make_pair h t) in
89 let isempty = \lst. lst get_fst in
90 let head = \lst. isempty lst err (lst get_snd get_fst) in
91 let tail_empty = empty in
92 let tail = \lst. isempty lst tail_empty (lst get_snd get_snd) in
95 ; more math with Church numerals
97 let add = \m n. m succ n in ; or
98 let add = \m n s z. m s (n s z) in
99 let mul = \m n. m (\z. add n z) zero in ; or
100 let mul = \m n s. m (n s) in
101 let pow = \b exp. exp (mul b) one in ; or
103 ; b (b succ) ; adds b b times, ie adds b^2
104 ; b (b (b succ)) ; adds b^2 b times, ie adds b^3
105 ; exp b succ ; adds b^exp
106 let pow = \b exp s z. exp b s z in
109 ; three strategies for predecessor
110 let pred_zero = zero in
111 let pred = (\shift n. n shift (make_pair zero pred_zero) get_snd)
113 (\p. p (\x y. make_pair (succ x) x)) in ; or
114 ; from Oleg; observe that for any Church numeral n: n I ~~> I
115 let pred = \n. iszero n zero
117 (n (\x. x I ; when x is the base term, this will be K zero
118 ; when x is a Church numeral, it will be I
123 ; from Bunder/Urbanek
124 let pred = \n s z. n (\u v. v (u s)) (K z) I in ; or
127 ; inefficient but simple comparisons
128 let leq = \m n. iszero (n pred m) in
129 let lt = \m n. not (leq n m) in
130 let eq = \m n. and (leq m n) (leq n m) in ; or
133 ; more efficient comparisons, Oleg's gt provided some simplifications
134 let leq = (\base build consume. \m n. n consume (m build base) get_fst)
136 (make_pair true junk)
138 (\p. make_pair false p)
140 (\p. p get_fst p (p get_snd)) in
141 let lt = \m n. not (leq n m) in
142 let eq = (\base build consume. \m n. n consume (m build base) get_fst)
143 ; 2nd element of a pair will now be of the form (K sthg) or I
144 ; we supply the pair being consumed itself as an argument
145 ; getting back either sthg or the pair we just consumed
147 (make_pair true (K (make_pair false I)))
149 (\p. make_pair false (K p))
154 ; -n is a fixedpoint of \x. add (add n x) x
155 ; but unfortunately Y that_function doesn't normalize
157 let sub = \m n. n pred m in ; or
158 ; how many times we can succ n until m <= result
159 let sub = \m n. (\base build. m build base (\cur fin sofar. sofar))
161 (make_triple n false zero)
163 (\t. t (\cur fin sofar. or fin (leq m cur)
164 (make_triple cur true sofar) ; enough
165 (make_triple (succ cur) false (succ sofar)) ; continue
168 let sub = (\base build consume. \m n. n consume (m build base) get_fst)
170 (make_pair zero I) ; see second defn of eq for explanation of 2nd element
172 (\p. p (\x y. make_pair (succ x) (K p)))
177 let min = \m n. sub m (sub m n) in
178 let max = \m n. add n (sub m n) in
181 ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x
182 ; but unfortunately Y that_function doesn't normalize
184 ; how many times we can sub n from m while n <= result
185 let div = \m n. (\base build. m build base (\cur go sofar. sofar))
187 (make_triple m true zero)
189 (\t. t (\cur go sofar. and go (leq n cur)
190 (make_triple (sub cur n) true (succ sofar)) ; continue
191 (make_triple cur false sofar) ; enough
193 ; what's left after sub n from m while n <= result
194 let mod = \m n. (\base build. m build base (\cur go. cur))
198 (\p. p (\cur go. and go (leq n cur)
199 (make_pair (sub cur n) true) ; continue
200 (make_pair cur false) ; enough
204 let divmod = (\base build mtail. \m n.
205 (\dhead. m (mtail dhead) (\sel. dhead (sel 0 0)))
206 (n build base (\x y z. z junk))
207 (\t u x y z. make_pair t u) )
209 (make_triple succ (K 0) I) ; see second defn of eq for explanation of 3rd element
211 (\t. make_triple I succ (K t))
213 (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz))))
215 let div = \n d. divmod n d get_fst in
216 let mod = \n d. divmod n d get_snd in
219 ; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x
220 ; but unfortunately Y that_function doesn't normalize
223 ; (log base b of m) is a fixedpoint of \x. add (sub (pow b x) m) x
224 ; but unfortunately Y that_function doesn't normalize
226 ; how many times we can mul b by b while result <= m
227 let log = \m b. (\base build. m build base (\cur go sofar. sofar))
229 (make_triple b true 0)
231 (\t. t (\cur go sofar. and go (leq cur m)
232 (make_triple (mul cur b) true (succ sofar)) ; continue
233 (make_triple cur false sofar) ; enough
237 ; Rosenbloom's fixed point combinator
238 let Y = \f. (\h. f (h h)) (\h. f (h h)) in
239 ; Turing's fixed point combinator
240 let Theta = (\u f. f (u u f)) (\u f. f (u u f)) in
243 ; now you can search for primes, do encryption :-)
244 let gcd = Y (\gcd m n. iszero n m (gcd n (mod m n))) in ; or
245 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
246 let lcm = \m n. or (iszero m) (iszero n) 0 (mul (div m (gcd m n)) n) in
249 ; length for version 1 lists
250 let length = Y (\self lst. isempty lst 0 (succ (self (tail lst)))) in
257 ; numhelper 0 f z ~~> z
258 ; when n > 0: numhelper n f z ~~> f (pred n)
259 ; compare Bunder/Urbanek pred
260 let numhelper = \n. n (\u v. v (u succ)) (K 0) (\p f z. f p) in
262 ; accepts fixed point combinator as a parameter, so you can use different ones
263 let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1) in
267 fact Theta 3 ; returns 6
271 ; my original efficient comparisons
272 let leq = (\base build consume. \m n. n consume (m build base) get_fst (\x. false) true)
274 (make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair
276 (\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)
279 let lt = \m n. not (leq n m) in
280 let eq = (\base build consume. \m n. n consume (m build base) true (\x. false) true)
282 (make_pair zero (K (make_pair one I)))
284 (\p. p (\x y. make_pair (succ x) (K p)))
286 (\p. p get_snd p) in ; or
294 show Oleg's definition of integers:
295 church_to_int = \n sign. n
296 church_to_negint = \n sign s z. sign (n s z)
301 sign_case = \int ifpos ifzero ifneg. int (K ifneg) (K ifpos) ifzero
303 negate_int = \int. sign_case int (church_to_negint (abs int)) zero (church_to_int (abs int))
305 for more, see http://okmij.org/ftp/Computation/lambda-calc.html#neg
315 ; deconstruct our sofar-pair
316 sofar (\might_be_equal right_tail.
319 (and (and might_be_equal (not (isempty right_tail))) (eq? hd (head right_tail)))
323 ; we pass along the fold a pair
324 ; (might_for_all_i_know_still_be_equal?, tail_of_reversed_right)
325 ; when left is empty, the lists are equal if right is empty
327 true ; for all we know so far, they might still be equal
330 ; when fold is finished, check sofar-pair
331 (\might_be_equal right_tail. and might_be_equal (isempty right_tail))
334 let list_equal = \left. left (\hd sofar. \right. and (and (not (isempty right)) (eq hd (head right))) (sofar (tail right))) isempty