leafs->leaves
[lambda.git] / lambda_library.mdwn
1 Here are a bunch of pre-tested operations for the untyped lambda calculus. In some cases multiple versions are offered.
2
3 Some of these are drawn from:
4
5 *       [[!wikipedia Lambda calculus]]
6 *       [[!wikipedia Church encoding]]
7 *       Oleg's [Basic Lambda Calculus Terms](http://okmij.org/ftp/Computation/lambda-calc.html#basic)
8
9 and all sorts of other places. Others of them are our own handiwork.
10
11
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.)
13
14
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
27
28         ;; tuples
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
32         let make_triple = \x y z f. f x y z  in
33
34
35         ;; Church numerals
36         let zero = \s z. z  in ; aka false
37         let one = \s z. s z  in ; aka I
38         let succ = \n s z. s (n s z)  in
39         ; for any Church numeral n > zero : n (K y) z ~~> y
40         let iszero = \n. n (\x. false) true  in
41
42         let add = \m n. m succ n  in ; or
43         let add = \m n s z. m s (n s z)  in
44         let mul = \m n. m (\z. add n z) zero  in ; or
45         let mul = \m n s. m (n s)  in
46         let pow = \b exp. exp (mul b) one  in ; or
47         ; b succ : adds b
48         ; b (b succ) ; adds b b times, ie adds b^2
49         ; b (b (b succ)) ; adds b^2 b times, ie adds b^3
50         ; exp b succ ; adds b^exp
51         let pow = \b exp s z. exp b s z  in
52
53         ; three strategies for predecessor
54         let pred_zero = zero  in
55         let pred = (\shift n. n shift (make_pair zero pred_zero) get_snd)
56                 ; where shift is
57                 (\p. p (\x y. make_pair (succ x) x))  in ; or
58         ; from Oleg; observe that for any Church numeral n: n I ~~> I
59         let pred = \n. iszero n zero
60                                         ; else
61                                         (n (\x. x I ; when x is the base term, this will be K zero
62                                                           ; when x is a Church numeral, it will be I
63                                                 (succ x))
64                                           ; base term
65                                           (K (K zero))
66                                         )  in
67         ; from Bunder/Urbanek
68         let pred = \n s z. n (\u v. v (u s)) (K z) I  in ; or
69
70         ; inefficient but simple comparisons
71         let leq = \m n. iszero (n pred m)  in
72         let lt = \m n. not (leq n m)  in
73         let eq = \m n. and (leq m n) (leq n m)  in ; or
74
75         ; more efficient comparisons, Oleg's gt provided some simplifications
76         let leq = (\base build consume. \m n. n consume (m build base) get_fst)
77                         ; where base is
78                         (make_pair true junk)
79                         ; and build is
80                         (\p. make_pair false p)
81                         ; and consume is
82                         (\p. p get_fst p (p get_snd))  in
83         let lt = \m n. not (leq n m)  in
84         let eq = (\base build consume. \m n. n consume (m build base) get_fst)
85                         ; 2nd element of a pair will now be of the form (K sthg) or I
86                         ; we supply the pair being consumed itself as an argument
87                         ; getting back either sthg or the pair we just consumed
88                         ; base is
89                         (make_pair true (K (make_pair false I)))
90                         ; and build is
91                         (\p. make_pair false (K p))
92                         ; and consume is
93                         (\p. p get_snd p)  in
94
95
96         ; -n is a fixedpoint of \x. add (add n x) x
97         ; but unfortunately Y that_function doesn't normalize
98         ; instead:
99         let sub = \m n. n pred m  in ; or
100         ; how many times we can succ n until m <= result
101         let sub = \m n. (\base build. m build base (\cur fin sofar. sofar))
102                                 ; where base is
103                                 (make_triple n false zero)
104                                 ; and build is
105                                 (\t. t (\cur fin sofar. or fin (leq m cur)
106                                                 (make_triple cur true sofar) ; enough
107                                                 (make_triple (succ cur) false (succ sofar)) ; continue
108                                 ))  in
109         ; or
110         let sub = (\base build consume. \m n. n consume (m build base) get_fst)
111                         ; where base is
112                         (make_pair zero I) ; see second defn of eq for explanation of 2nd element
113                         ; and build is
114                         (\p. p (\x y. make_pair (succ x) (K p)))
115                         ; and consume is
116                         (\p. p get_snd p)  in
117
118
119         let min = \m n. sub m (sub m n)  in
120         let max = \m n. add n (sub m n)  in
121
122
123         ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x
124         ; but unfortunately Y that_function doesn't normalize
125         ; instead:
126         ; how many times we can sub n from m while n <= result
127         let div = \m n. (\base build. m build base (\cur go sofar. sofar))
128                                 ; where base is
129                                 (make_triple m true zero)
130                                 ; and build is
131                                 (\t. t (\cur go sofar. and go (leq n cur)
132                                                 (make_triple (sub cur n) true (succ sofar)) ; continue
133                                                 (make_triple cur false sofar) ; enough
134                                 ))  in
135     ; what's left after sub n from m while n <= result
136     let mod = \m n. (\base build. m build base (\cur go. cur))
137                 ; where base is
138                 (make_pair m true)
139                 ; and build is
140                 (\p. p (\cur go. and go (leq n cur)
141                         (make_pair (sub cur n) true) ; continue
142                         (make_pair cur false) ; enough
143                 ))  in
144
145         ; or
146         let divmod = (\base build mtail. \m n.
147                                         (\dhead. m (mtail dhead) (\sel. dhead (sel 0 0)))
148                                                         (n build base (\x y z. z junk))
149                                                         (\t u x y z. make_pair t u) )
150                                 ; where base is
151                                 (make_triple succ (K 0) I) ; see second defn of eq for explanation of 3rd element
152                                 ; and build is
153                         (\t. make_triple I succ (K t))
154                                 ; and mtail is
155                                 (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz))))  in
156         let div = \n d. divmod n d get_fst  in
157         let mod = \n d. divmod n d get_snd  in
158
159
160         ; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x
161         ; but unfortunately Y that_function doesn't normalize
162
163
164         ; (log base b of m) is a fixedpoint of \x. add (sub (pow b x) m) x
165         ; but unfortunately Y that_function doesn't normalize
166         ; instead:
167         ; how many times we can mul b by b while result <= m
168         let log = \m b. (\base build. m build base (\cur go sofar. sofar))
169                 ; where base is
170                 (make_triple b true 0)
171                 ; and build is
172                 (\t. t (\cur go sofar. and go (leq cur m)
173                            (make_triple (mul cur b) true (succ sofar)) ; continue
174                            (make_triple cur false sofar) ; enough
175                 ))  in
176
177
178         ;; fixed point combinators
179         ; Curry/Rosenbloom's
180         let Y = \f. (\h. f (h h)) (\h. f (h h))  in
181         ; Turing's
182         let Theta = (\u f. f (u u f)) (\u f. f (u u f))  in
183
184
185         ; now you can search for primes, do encryption :-)
186         let gcd = Y (\gcd m n. iszero n m (gcd n (mod m n)))  in ; or
187         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
188         let lcm = \m n. or (iszero m) (iszero n) 0 (mul (div m (gcd m n)) n)  in
189
190
191         ;; version 1 lists
192         let empty = make_pair true junk  in
193         let make_list = \h t. make_pair false (make_pair h t)  in
194         let isempty = \lst. lst get_fst  in
195         let head = \lst. isempty lst err (lst get_snd get_fst)  in
196         let tail_empty = empty  in
197         let tail = \lst. isempty lst tail_empty (lst get_snd get_snd)  in
198
199         let length = Y (\length lst. isempty lst 0 (succ (length (tail lst))))  in
200         let fold = Y (\fold lst f z. isempty lst z (f (head lst) (fold (tail lst) f z)))  in
201         let map = \f. Y (\map lst. isempty lst empty (make_list (f (head lst)) (map (tail lst))))  in
202         let filter = \f. Y (\filter lst. isempty lst empty (f (head lst) (make_list (head lst)) I (filter (tail lst))))  in
203
204
205         ;; version 3 (right-fold) lists
206         let empty = \f z. z  in
207         let make_list = \h t f z. f h (t f z)  in
208         let isempty = \lst. lst (\h sofar. false) true  in
209         let head = \lst. lst (\h sofar. h) err  in
210         let tail_empty = empty  in
211         let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) get_snd)
212                                 ; where shift is
213                                 (\h p. p (\t y. make_pair (make_list h t) t))  in
214         let length = \lst. lst (\h sofar. succ sofar) 0  in
215         let map = \f lst. lst (\h sofar. make_list (f h) sofar) empty  in
216         let filter = \f lst. lst (\h sofar. f h (make_list h sofar) sofar) empty  in ; or
217         let filter = \f lst. lst (\h. f h (make_list h) I) empty  in
218         let singleton = \x f z. f x z  in
219         ; append [a;b;c] [x;y;z] ~~> [a;b;c;x;y;z]
220         let append = \left right. left make_list right  in
221         ; very inefficient but correct reverse
222         let reverse = \lst. lst (\h sofar. append sofar (singleton h)) empty  in ; or
223         ; more efficient revappend, reverse
224         ; revappend [a;b;c] [x;y] ~~> [c;b;a;x;y]
225         ; make_left_list a (make_left_list b (make_left_list c empty)) ~~> \f z. f c (f b (f a z))
226         let revappend = (\make_left_lst left right. left make_left_list right) (\h t f z. t f (f h z))  in
227         ; from Oleg, of course it's the most elegant
228         let revappend = \left. left (\hd sofar. \right. sofar (make_list hd right)) I  in
229         let rev = \lst. revappend lst empty  in
230         ; zip [a;b;c] [x;y;z] ~~> [(a,x);(b,y);(c,z)]
231         let zip = \left right. (\base build. reverse left build base (\x y. reverse x))
232                                            ; where base is
233                                            (make_pair empty (map (\h u. u h) right))
234                                            ; and build is
235                                            (\h sofar. sofar (\x y. isempty y
236                                                                                            sofar
237                                                                                            (make_pair (make_list (\u. head y (u h)) x)  (tail y))
238                                            ))  in
239         let all = \f lst. lst (\h sofar. and sofar (f h)) true  in
240         let any = \f lst. lst (\h sofar. or sofar (f h)) false  in
241
242
243         ;; left-fold lists
244         let make_list = \h t f z. t f (f h z)  in
245         let head = \lst. lst (\h sofar. (K (sofar (K h))) ) (\k. k err) I  in
246         let tail = \lst. (\shift. lst shift (\a b. a tail_empty) I I)
247                                 (\h p. p (\j a b. b empty) (\t a b. b (\f z. f h (t f z))) )  in
248
249
250         ;; version 5 (CPS right-fold) lists
251         ; [] is \f z c a. c z
252         ; [1] is \f z c a. f 1 z c a
253         ; [1;2] is \f z c a. f 2 z (\z. f 1 z c a) a
254         ; [1;2;3] is \f z c a. f 3 z (\z. f 2 z (\z. f 1 z c a) a) a
255         let empty = \f2 z continue_handler abort_handler. continue_handler z  in
256         let isempty = \lst larger_computation. lst
257                         ; here's our f2
258                         (\hd sofar continue_handler abort_handler. abort_handler false)
259                         ; here's our z
260                         true
261                         ; here's the continue_handler for the leftmost application of f2
262                         larger_computation
263                         ; here's the abort_handler
264                         larger_computation  in
265         let make_list = \h t. \f2 z continue_handler abort_handler.
266                 t f2 z (\sofar. f2 h sofar continue_handler abort_handler) abort_handler  in
267         let head = \lst larger_computation. lst
268                         ; here's our f2
269                         (\hd sofar continue_handler abort_handler. continue_handler hd)
270                         ; here's our z
271                         err
272                         ; here are our continue_handler and abort_handler
273                         larger_computation unused  in
274         let tail_empty = empty  in
275         let tail = \lst larger_computation. lst
276                         ; here's our f2
277                         (\h sofar continue_handler abort_handler. continue_handler (sofar (\t y. make_pair (make_list h t) t)))
278                         ; here's our z
279                         (make_pair empty tail_empty)
280                         ; here are our continue_handler and abort_handler
281                         (\sofar. sofar (\x y. larger_computation y)) unused  in
282
283         ;; CPS left-fold lists
284         ; [] is \f z c a. c z
285         ; [1] is \f z c a. f 1 z  (\z. c z) a
286         ; [1;2] is \f z c a. f 1 z (\z. f 2 z (\z. c z) a) a
287         ; [1;2;3] is \f z c a. f 1 z (\z. f 2 z (\z. f 3 z (\z. c z) a) a) a
288         let make_right_list = make_list  in
289         let make_list = \h t. \f2 z continue_handler abort_handler.
290                 f2 h z (\z. t f2 z continue_handler abort_handler) abort_handler  in
291         let head = \lst larger_computation. lst
292                         ; here's our f2
293                         (\hd sofar continue_handler abort_handler. abort_handler hd)
294                         ; here's our z
295                         err
296                         ; here are our continue_handler and abort_handler
297                         larger_computation larger_computation  in
298         let tail = \lst larger_computation. lst
299                         ; here's our f2
300                         (\h sofar continue_handler abort_handler. continue_handler (sofar (\j a b. b empty) (\t a b. b (make_right_list h t)) ) )
301                         ; here's our z
302                         (\a b. a tail_empty)
303                         ; here are our continue_handler and abort_handler
304                         (\sofar. sofar larger_computation larger_computation) unused  in
305
306
307
308         true
309
310 <!--
311
312         ; numhelper 0 f z ~~> z
313         ; when n > 0: numhelper n f z ~~> f (pred n)
314         ; compare Bunder/Urbanek pred
315         let numhelper = \n. n (\u v. v (u succ)) (K 0) (\p f z. f p)  in
316
317         ; accepts fixed point combinator as a parameter, so you can use different ones
318         let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1)  in
319
320
321
322         fact Theta 3  ; returns 6
323 -->
324
325 <!--
326         ; my original efficient comparisons
327         let leq = (\base build consume. \m n. n consume (m build base) get_fst (\x. false) true)
328                         ; where base is
329                         (make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair
330                         ; and build is
331                         (\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)
332                         ; and consume is
333                         (\p. p get_snd p)  in
334         let lt = \m n. not (leq n m)  in
335         let eq = (\base build consume. \m n. n consume (m build base) true (\x. false) true)
336                         ; where base is
337                         (make_pair zero (K (make_pair one I)))
338                         ; and build is
339                         (\p. p (\x y. make_pair (succ x) (K p)))
340                         ; and consume is
341                         (\p. p get_snd p)  in ; or
342 -->
343
344 <!--
345         gcd
346         pow_mod
347
348
349         show Oleg's definition of integers:
350                 church_to_int = \n sign. n
351                 church_to_negint = \n sign s z. sign (n s z)
352
353                 ; int_to_church
354                 abs = \int. int I
355
356                 sign_case = \int ifpos ifzero ifneg. int (K ifneg) (K ifpos) ifzero
357
358                 negate_int = \int. sign_case int (church_to_negint (abs int)) zero (church_to_int (abs int))
359
360         for more, see http://okmij.org/ftp/Computation/lambda-calc.html#neg
361
362
363 -->
364
365 <!--
366 let list_equal =
367     \left right. left
368                 ; here's our f
369                 (\hd sofar.
370                     ; deconstruct our sofar-pair
371                     sofar (\might_be_equal right_tail.
372                         ; our new sofar
373                         make_pair
374                         (and (and might_be_equal (not (isempty right_tail))) (eq? hd (head right_tail)))
375                         (tail right_tail)
376                     ))
377                 ; here's our z
378                 ; we pass along the fold a pair
379                 ; (might_for_all_i_know_still_be_equal?, tail_of_reversed_right)
380                 ; when left is empty, the lists are equal if right is empty
381                 (make_pair
382                     true ; for all we know so far, they might still be equal
383                     (reverse right)
384                 )
385                 ; when fold is finished, check sofar-pair
386                 (\might_be_equal right_tail. and might_be_equal (isempty right_tail))
387
388 ; most elegant
389 let list_equal = \left. left (\hd sofar. \right. and (and (not (isempty right)) (eq hd (head right))) (sofar (tail right))) isempty
390
391 -->
392