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.)
15         ; booleans
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
28         ; pairs
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
33         ; triples
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
46         ; version 3 lists
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)
54                                 ; where shift is
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         ; zip [a;b;c] [x;y;z] ~~> [(a,x);(b,y);(c,z)]
69         let zip = \left right. (\base build. reverse left build base (\x y. reverse x))
70                        ; where base is
71                        (make_pair empty (map (\h u. u h) right))
72                        ; and build is
73                        (\h sofar. sofar (\x y. isempty y
74                                                sofar
75                                                (make_pair (make_list (\u. head y (u h)) x)  (tail y))
76                        ))  in
77         let all = \f lst. lst (\h sofar. and sofar (f h)) true  in
78         let any = \f lst. lst (\h sofar. or sofar (f h)) false  in
81         ; version 1 lists
83         let empty = make_pair true junk  in
84         let make_list = \h t. make_pair false (make_pair h t)  in
85         let isempty = \lst. lst get_fst  in
86         let head = \lst. isempty lst err (lst get_snd get_fst)  in
87         let tail_empty = empty  in
88         let tail = \lst. isempty lst tail_empty (lst get_snd get_snd)  in
91         ; more math with Church numerals
93         let add = \m n. m succ n  in ; or
94         let add = \m n s z. m s (n s z)  in
95         let mul = \m n. m (\z. add n z) zero  in ; or
96         let mul = \m n s. m (n s)  in
97         let pow = \b exp. exp (mul b) one  in ; or
98         ; b succ : adds b
99         ; b (b succ) ; adds b b times, ie adds b^2
100         ; b (b (b succ)) ; adds b^2 b times, ie adds b^3
101         ; exp b succ ; adds b^exp
102         let pow = \b exp s z. exp b s z  in
105         ; three strategies for predecessor
106         let pred_zero = zero  in
107         let pred = (\shift n. n shift (make_pair zero pred_zero) get_snd)
108                 ; where shift is
109                 (\p. p (\x y. make_pair (succ x) x))  in ; or
110         ; from Oleg; observe that for any Church numeral n: n I ~~> I
111         let pred = \n. iszero n zero
112                                         ; else
113                                         (n (\x. x I ; when x is the base term, this will be K zero
114                                                           ; when x is a Church numeral, it will be I
115                                                 (succ x))
116                                           ; base term
117                                           (K (K zero))
118                                         )  in
119         ; from Bunder/Urbanek
120         let pred = \n s z. n (\u v. v (u s)) (K z) I  in ; or
123         ; inefficient but simple comparisons
124         let leq = \m n. iszero (n pred m)  in
125         let lt = \m n. not (leq n m)  in
126         let eq = \m n. and (leq m n) (leq n m)  in ; or
129         ; more efficient comparisons, Oleg's gt provided some simplifications
130         let leq = (\base build consume. \m n. n consume (m build base) get_fst)
131                         ; where base is
132                         (make_pair true junk)
133                         ; and build is
134                         (\p. make_pair false p)
135                         ; and consume is
136                         (\p. p get_fst p (p get_snd))  in
137         let lt = \m n. not (leq n m)  in
138         let eq = (\base build consume. \m n. n consume (m build base) get_fst)
139                         ; 2nd element of a pair will now be of the form (K sthg) or I
140                         ; we supply the pair being consumed itself as an argument
141                         ; getting back either sthg or the pair we just consumed
142                         ; base is
143                         (make_pair true (K (make_pair false I)))
144                         ; and build is
145                         (\p. make_pair false (K p))
146                         ; and consume is
147                         (\p. p get_snd p)  in
150         ; -n is a fixedpoint of \x. add (add n x) x
151         ; but unfortunately Y that_function doesn't normalize
153         let sub = \m n. n pred m  in ; or
154         ; how many times we can succ n until m <= result
155         let sub = \m n. (\base build. m build base (\cur fin sofar. sofar))
156                                 ; where base is
157                                 (make_triple n false zero)
158                                 ; and build is
159                                 (\t. t (\cur fin sofar. or fin (leq m cur)
160                                                 (make_triple cur true sofar) ; enough
161                                                 (make_triple (succ cur) false (succ sofar)) ; continue
162                                 ))  in
163         ; or
164         let sub = (\base build consume. \m n. n consume (m build base) get_fst)
165                         ; where base is
166                         (make_pair zero I) ; see second defn of eq for explanation of 2nd element
167                         ; and build is
168                         (\p. p (\x y. make_pair (succ x) (K p)))
169                         ; and consume is
170                         (\p. p get_snd p)  in
173         let min = \m n. sub m (sub m n) in
174         let max = \m n. add n (sub m n) in
177         ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x
178         ; but unfortunately Y that_function doesn't normalize
180         ; how many times we can sub n from m while n <= result
181         let div = \m n. (\base build. m build base (\cur go sofar. sofar))
182                                 ; where base is
183                                 (make_triple m true zero)
184                                 ; and build is
185                                 (\t. t (\cur go sofar. and go (leq n cur)
186                                                 (make_triple (sub cur n) true (succ sofar)) ; continue
187                                                 (make_triple cur false sofar) ; enough
188                                 ))  in
189     ; what's left after sub n from m while n <= result
190     let mod = \m n. (\base build. m build base (\cur go. cur))
191                 ; where base is
192                 (make_pair m true)
193                 ; and build is
194                 (\p. p (\cur go. and go (leq n cur)
195                         (make_pair (sub cur n) true) ; continue
196                         (make_pair cur false) ; enough
197                 ))  in
199         ; or
200         let divmod = (\base build mtail. \m n.
202                                                         (n build base (\x y z. z junk))
203                                                         (\t u x y z. make_pair t u) )
204                                 ; where base is
205                                 (make_triple succ (K 0) I) ; see second defn of eq for explanation of 3rd element
206                                 ; and build is
207                         (\t. make_triple I succ (K t))
208                                 ; and mtail is
209                                 (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz))))
210         in
211         let div = \n d. divmod n d get_fst  in
212         let mod = \n d. divmod n d get_snd  in
215         ; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x
216         ; but unfortunately Y that_function doesn't normalize
219         ; (log base b of m) is a fixedpoint of \x. add (sub (pow b x) m) x
220         ; but unfortunately Y that_function doesn't normalize
222         ; how many times we can mul b by b while result <= m
223         let log = \m b. (\base build. m build base (\cur go sofar. sofar))
224                 ; where base is
225                 (make_triple b true 0)
226                 ; and build is
227                 (\t. t (\cur go sofar. and go (leq cur m)
228                            (make_triple (mul cur b) true (succ sofar)) ; continue
229                            (make_triple cur false sofar) ; enough
230                 ))  in
233         ; Rosenbloom's fixed point combinator
234         let Y = \f. (\h. f (h h)) (\h. f (h h)) in
235         ; Turing's fixed point combinator
236         let Theta = (\u f. f (u u f)) (\u f. f (u u f))  in
239         ; now you can search for primes, do encryption :-)
240         let gcd = Y (\gcd m n. iszero n m (gcd n (mod m n))) in
241         let lcm = \m n. or (iszero m) (iszero n) 0 (mul (div m (gcd m n)) n) in
244         ; length for version 1 lists
245         let length = Y (\self lst. isempty lst 0 (succ (self (tail lst))))  in
248         true
250 <!--
252         ; numhelper 0 f z ~~> z
253         ; when n > 0: numhelper n f z ~~> f (pred n)
254         ; compare Bunder/Urbanek pred
255         let numhelper = \n. n (\u v. v (u succ)) (K 0) (\p f z. f p)  in
257         ; accepts fixed point combinator as a parameter, so you can use different ones
258         let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1)  in
262         fact Theta 3  ; returns 6
263 -->
265 <!--
266         ; my original efficient comparisons
267         let leq = (\base build consume. \m n. n consume (m build base) get_fst (\x. false) true)
268                         ; where base is
269                         (make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair
270                         ; and build is
271                         (\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)
272                         ; and consume is
273                         (\p. p get_snd p)  in
274         let lt = \m n. not (leq n m) in
275         let eq = (\base build consume. \m n. n consume (m build base) true (\x. false) true)
276                         ; where base is
277                         (make_pair zero (K (make_pair one I)))
278                         ; and build is
279                         (\p. p (\x y. make_pair (succ x) (K p)))
280                         ; and consume is
281                         (\p. p get_snd p)  in ; or
282 -->
284 <!--
285         gcd
286         pow_mod
289         show Oleg's definition of integers:
290                 church_to_int = \n sign. n
291                 church_to_negint = \n sign s z. sign (n s z)
293                 ; int_to_church
294                 abs = \int. int I
296                 sign_case = \int ifpos ifzero ifneg. int (K ifneg) (K ifpos) ifzero
298                 negate_int = \int. sign_case int (church_to_negint (abs int)) zero (church_to_int (abs int))
300         for more, see http://okmij.org/ftp/Computation/lambda-calc.html#neg
303 -->
305 <!--
306 let list_equal =
307     \left right. left
308                 ; here's our f
309                 (\hd sofar.
310                     ; deconstruct our sofar-pair
311                     sofar (\might_be_equal right_tail.
312                         ; our new sofar
313                         make_pair
314                         (and (and might_be_equal (not (isempty right_tail))) (eq? hd (head right_tail)))
315                         (tail right_tail)
316                     ))
317                 ; here's our z
318                 ; we pass along the fold a pair
319                 ; (might_for_all_i_know_still_be_equal?, tail_of_reversed_right)
320                 ; when left is empty, the lists are equal if right is empty
321                 (make_pair
322                     true ; for all we know so far, they might still be equal
323                     (reverse right)
324                 )
325                 ; when fold is finished, check sofar-pair
326                 (\might_be_equal right_tail. and might_be_equal (isempty right_tail))
327 -->