2         ; booleans
3         let true = \y n. y  in ; aka K
4         let false = \y n. n  in ; aka K I
5         let and = \p q. p q false  in ; or
6         let and = \p q. p q p  in ; aka S C I
7         let or = \p q. p true q  in ; or
8         let or = \p q. p p q  in ; aka M
9         let not = \p. p false true  in ; or
10         let not = \p y n. p n y  in ; aka C
11         let xor = \p q. p (not q) q  in
12         let iff = \p q. not (xor p q)  in ; or
13         let iff = \p q. p q (not q)  in
15         ; pairs
16         let make_pair = \x y f. f x y  in
17         let get_1st = \x y. x  in ; aka true
18         let get_2nd = \x y. y  in ; aka false
20         ; triples
21         let make_triple = \x y z f. f x y z  in
24         ; Church numerals
25         let zero = \s z. z  in ; aka false
26         let one = \s z. s z  in ; aka I
27         let succ = \n s z. s (n s z)  in
28         ; for any Church numeral n > zero : n (K y) z ~~> y
29         let iszero = \n. n (\x. false) true  in
30         let add = \m n. m succ n  in ; or
31         let add = \m n s z. m s (n s z)  in
32         let mul = \m n. m (\z. add n z) zero  in ; or
33         let mul = \m n s. m (n s)  in
34         let pow = \b exp. exp (mul b) one  in ; or
35         ; b succ : adds b
36         ; b (b succ) ; adds b b times, ie adds b^2
37         ; b (b (b succ)) ; adds b^2 b times, ie adds b^3
38         ; exp b succ ; adds b^exp
39         let pow = \b exp s z. exp b s z  in
41         ; three strategies for predecessor
42         let pred_zero = zero  in
43         let pred = (\shift n. n shift (make_pair zero pred_zero) get_2nd)
44                 ; where shift is
45                 (\p. p (\x y. make_pair (succ x) x))  in ; or
46         ; from Oleg; observe that for any Church numeral n: n I ~~> I
47         let pred = \n. iszero n zero
48                                         ; else
49                                         (n (\x. x I ; when x is the base term, this will be K zero
50                                                           ; when x is a Church numeral, it will be I
51                                                 (succ x))
52                                           ; base term
53                                           (K (K zero))
54                                         )  in
55         ; from Bunder/Urbanek
56         let pred = \n s z. n (\u v. v (u s)) (K z) I  in ; or
59         ; inefficient but simple comparisons
60         let leq = \m n. iszero (n pred m)  in
61         let lt = \m n. not (leq n m)  in
62         let eq = \m n. and (leq m n) (leq n m)  in ; or
65         ; more efficient comparisons
66         let leq = (\base build consume. \m n. n consume (m build base) get_1st (\x. false) true)
67                         ; where base is
68                         (make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair
69                         ; and build is
70                         (\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)
71                         ; and consume is
72                         (\p. p get_2nd p)  in
73         let lt = \m n. not (leq n m) in
74         let eq = (\base build consume. \m n. n consume (m build base) true (\x. false) true)
75                         ; where base is
76                         (make_pair zero (K (make_pair one I)))
77                         ; and build is
78                         (\p. p (\x y. make_pair (succ x) (K p)))
79                         ; and consume is
80                         (\p. p get_2nd p)  in ; or
83         ; more efficient comparisons, Oleg's gt provided some simplification
84         let leq = (\base build consume. \m n. n consume (m build base) get_1st)
85                         ; where base is
86                         (make_pair true junk)
87                         ; and build is
88                         (\p. make_pair false p)
89                         ; and consume is
90                         (\p. p get_1st p (p get_2nd))  in
91         let lt = \m n. not (leq n m)  in
92         let eq = (\base build consume. \m n. n consume (m build base) get_1st)
93                         ; 2nd element of a pair will now be of the form (K sthg) or I
94                         ; we supply the pair being consumed itself as an argument
95                         ; getting back either sthg or the pair we just consumed
96                         ; base is
97                         (make_pair true (K (make_pair false I)))
98                         ; and build is
99                         (\p. make_pair false (K p))
100                         ; and consume is
101                         (\p. p get_2nd p)  in
103         ; -n is a fixedpoint of \x. add (add n x) x
104         ; but unfortunately Y that_function doesn't normalize
106         let sub = \m n. n pred m  in ; or
107         ; how many times we can succ n until m <= result
108         let sub = \m n. (\base build. m build base (\cur fin sofar. sofar))
109                                 ; where base is
110                                 (make_triple n false zero)
111                                 ; and build is
112                                 (\t. t (\cur fin sofar. or fin (leq m cur)
113                                                 (make_triple cur true sofar) ; enough
114                                                 (make_triple (succ cur) false (succ sofar)) ; continue
115                                 ))  in
116         ; or
117         let sub = (\base build consume. \m n. n consume (m build base) get_1st)
118                         ; where base is
119                         (make_pair zero I) ; see second defn of eq for explanation of 2nd element
120                         ; and build is
121                         (\p. p (\x y. make_pair (succ x) (K p)))
122                         ; and consume is
123                         (\p. p get_2nd p)  in
125         let min = \m n. sub m (sub m n) in
126         let max = \m n. add n (sub m n) in
128         ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x
129         ; but unfortunately Y that_function doesn't normalize
131         ; how many times we can sub n from m while n <= result
132         let div = \m n. (\base build. m build base (\cur go sofar. sofar))
133                                 ; where base is
134                                 (make_triple m true zero)
135                                 ; and build is
136                                 (\t. t (\cur go sofar. and go (leq n cur)
137                                                 (make_triple (sub cur n) true (succ sofar)) ; continue
138                                                 (make_triple cur false sofar) ; enough
139                                 ))  in
140     ; what's left after sub n from m while n <= result
141     let mod = \m n. (\base build. m build base (\cur go. cur))
142                 ; where base is
143                 (make_pair m true)
144                 ; and build is
145                 (\p. p (\cur go. and go (leq n cur)
146                         (make_pair (sub cur n) true) ; continue
147                         (make_pair cur false) ; enough
148                 ))  in
150         ; or
151         let divmod = (\base build mtail. \m n.
153                                                         (n build base (\x y z. z junk))
154                                                         (\t u x y z. make_pair t u) )
155                                 ; where base is
156                                 (make_triple succ (K 0) I) ; see second defn of eq for explanation of 3rd element
157                                 ; and build is
158                         (\t. make_triple I succ (K t))
159                                 ; and mtail is
160                                 (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz))))
161         in
162         let div = \n d. divmod n d get_1st  in
163         let mod = \n d. divmod n d get_2nd  in
165         ; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x
166         ; but unfortunately Y that_function doesn't normalize
168         ; (log base b of m) is a fixedpoint of \x. add (sub (pow b x) m) x
169         ; but unfortunately Y that_function doesn't normalize
171         ; how many times we can mul b by b while result <= m
172         let log = \m b. (\base build. m build base (\cur go sofar. sofar))
173                 ; where base is
174                 (make_triple b true 0)
175                 ; and build is
176                 (\t. t (\cur go sofar. and go (leq cur m)
177                            (make_triple (mul cur b) true (succ sofar)) ; continue
178                            (make_triple cur false sofar) ; enough
179                 ))  in
181         ; Curry's fixed point combinator
182         let Y = \f. (\h. f (h h)) (\h. f (h h)) in
183         ; Turing's fixed point combinator
184         let Z = (\u f. f (u u f)) (\u f. f (u u f))  in
189         ; version 3 lists
190         let empty = \f z. z  in
191         let make_list = \h t f z. f h (t f z)  in
192         let isempty = \lst. lst (\h sofar. false) true  in
193         let head = \lst. lst (\h sofar. h) junk  in
194         let tail = \lst. (\shift lst. lst shift (make_pair empty junk) get_2nd)
195                                 ; where shift is
196                                 (\h p. p (\t y. make_pair (make-list h t) t))  in
197         let length = \lst. lst (\h sofar. succ sofar) zero  in
198         let map = \f lst. lst (\h sofar. make_list (f h) sofar) empty  in
199         let filter = \f lst. lst (\h sofar. f h (make_list h sofar) sofar) empty  in ; or
200         let filter = \f lst. lst (\h. f h (make_list h) I) empty  in
203         ; version 1 lists
204         let empty = make_pair true junk  in
205         let make_list = \h t. make_pair false (make_pair h t)  in
206         let isempty = \lst. lst get_1st  in
207         let head = \lst. isempty lst error (lst get_2nd get_1st)  in
208         let tail_empty = empty  in
209         let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd)  in
211         let length = Y (\self lst. isempty lst 0 (succ (self (tail lst))))  in
215         ; numhelper 0 f z ~~> z
216         ; when n > 0: numhelper n f z ~~> f (pred n)
217         ; compare Bunder/Urbanek pred
218         let numhelper = \n. n (\u v. v (u succ)) (K 0) (\p f z. f p)  in
220         ; accepts fixed point combinator as a parameter, so you can use different ones
221         let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1)  in
224         fact Z 3  ; returns 6