d27248754b7832b7c5edadb702823f11a35c3457
[lambda.git] / arithmetic.mdwn
1 Here are a bunch of pre-tested operations for the untyped lambda calculus. In some cases multiple versions are offered.
2
3         ; booleans
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
15
16         ; pairs
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
20
21         ; triples
22         let make_triple = \x y z f. f x y z  in
23
24
25         ; Church numerals: basic operations
26
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
32
33
34         ; version 3 lists
35
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 = \lst. (\shift lst. lst shift (make_pair empty junk) get_2nd)
41                                 ; where shift is
42                                 (\h p. p (\t y. make_pair (make_list h t) t))  in
43         let length = \lst. lst (\h sofar. succ sofar) 0  in
44         let map = \f lst. lst (\h sofar. make_list (f h) sofar) empty  in
45         let filter = \f lst. lst (\h sofar. f h (make_list h sofar) sofar) empty  in ; or
46         let filter = \f lst. lst (\h. f h (make_list h) I) empty  in
47         
48
49         ; version 1 lists
50
51         let empty = make_pair true junk  in
52         let make_list = \h t. make_pair false (make_pair h t)  in
53         let isempty = \lst. lst get_1st  in
54         let head = \lst. isempty lst err (lst get_2nd get_1st)  in
55         let tail_empty = empty  in
56         let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd)  in
57         
58
59         ; more math with Church numerals
60
61         let add = \m n. m succ n  in ; or
62         let add = \m n s z. m s (n s z)  in
63         let mul = \m n. m (\z. add n z) zero  in ; or
64         let mul = \m n s. m (n s)  in
65         let pow = \b exp. exp (mul b) one  in ; or
66         ; b succ : adds b
67         ; b (b succ) ; adds b b times, ie adds b^2
68         ; b (b (b succ)) ; adds b^2 b times, ie adds b^3
69         ; exp b succ ; adds b^exp
70         let pow = \b exp s z. exp b s z  in
71
72
73         ; three strategies for predecessor
74         let pred_zero = zero  in
75         let pred = (\shift n. n shift (make_pair zero pred_zero) get_2nd)
76                 ; where shift is
77                 (\p. p (\x y. make_pair (succ x) x))  in ; or
78         ; from Oleg; observe that for any Church numeral n: n I ~~> I
79         let pred = \n. iszero n zero
80                                         ; else
81                                         (n (\x. x I ; when x is the base term, this will be K zero
82                                                           ; when x is a Church numeral, it will be I
83                                                 (succ x))
84                                           ; base term
85                                           (K (K zero))
86                                         )  in
87         ; from Bunder/Urbanek
88         let pred = \n s z. n (\u v. v (u s)) (K z) I  in ; or
89
90                                         
91         ; inefficient but simple comparisons
92         let leq = \m n. iszero (n pred m)  in
93         let lt = \m n. not (leq n m)  in
94         let eq = \m n. and (leq m n) (leq n m)  in ; or
95
96
97         ; more efficient comparisons, Oleg's gt provided some simplifications
98         let leq = (\base build consume. \m n. n consume (m build base) get_1st)
99                         ; where base is
100                         (make_pair true junk)
101                         ; and build is
102                         (\p. make_pair false p)
103                         ; and consume is
104                         (\p. p get_1st p (p get_2nd))  in
105         let lt = \m n. not (leq n m)  in
106         let eq = (\base build consume. \m n. n consume (m build base) get_1st)
107                         ; 2nd element of a pair will now be of the form (K sthg) or I
108                         ; we supply the pair being consumed itself as an argument
109                         ; getting back either sthg or the pair we just consumed
110                         ; base is
111                         (make_pair true (K (make_pair false I)))
112                         ; and build is
113                         (\p. make_pair false (K p))
114                         ; and consume is
115                         (\p. p get_2nd p)  in
116         
117
118         ; -n is a fixedpoint of \x. add (add n x) x
119         ; but unfortunately Y that_function doesn't normalize
120         ; instead:
121         let sub = \m n. n pred m  in ; or
122         ; how many times we can succ n until m <= result
123         let sub = \m n. (\base build. m build base (\cur fin sofar. sofar))
124                                 ; where base is
125                                 (make_triple n false zero)
126                                 ; and build is
127                                 (\t. t (\cur fin sofar. or fin (leq m cur)
128                                                 (make_triple cur true sofar) ; enough
129                                                 (make_triple (succ cur) false (succ sofar)) ; continue
130                                 ))  in
131         ; or
132         let sub = (\base build consume. \m n. n consume (m build base) get_1st)
133                         ; where base is
134                         (make_pair zero I) ; see second defn of eq for explanation of 2nd element
135                         ; and build is
136                         (\p. p (\x y. make_pair (succ x) (K p)))
137                         ; and consume is
138                         (\p. p get_2nd p)  in
139
140
141         let min = \m n. sub m (sub m n) in
142         let max = \m n. add n (sub m n) in
143
144
145         ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x
146         ; but unfortunately Y that_function doesn't normalize
147         ; instead:
148         ; how many times we can sub n from m while n <= result
149         let div = \m n. (\base build. m build base (\cur go sofar. sofar))
150                                 ; where base is
151                                 (make_triple m true zero)
152                                 ; and build is
153                                 (\t. t (\cur go sofar. and go (leq n cur)
154                                                 (make_triple (sub cur n) true (succ sofar)) ; continue
155                                                 (make_triple cur false sofar) ; enough
156                                 ))  in
157     ; what's left after sub n from m while n <= result
158     let mod = \m n. (\base build. m build base (\cur go. cur))
159                 ; where base is
160                 (make_pair m true)
161                 ; and build is
162                 (\p. p (\cur go. and go (leq n cur)
163                         (make_pair (sub cur n) true) ; continue
164                         (make_pair cur false) ; enough
165                 ))  in
166
167         ; or
168         let divmod = (\base build mtail. \m n.
169                                         (\dhead. m (mtail dhead) (\sel. dhead (sel 0 0)))
170                                                         (n build base (\x y z. z junk))
171                                                         (\t u x y z. make_pair t u) )
172                                 ; where base is
173                                 (make_triple succ (K 0) I) ; see second defn of eq for explanation of 3rd element
174                                 ; and build is
175                         (\t. make_triple I succ (K t))
176                                 ; and mtail is
177                                 (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz))))
178         in
179         let div = \n d. divmod n d get_1st  in
180         let mod = \n d. divmod n d get_2nd  in
181
182
183         ; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x
184         ; but unfortunately Y that_function doesn't normalize
185
186
187         ; (log base b of m) is a fixedpoint of \x. add (sub (pow b x) m) x
188         ; but unfortunately Y that_function doesn't normalize
189         ; instead:
190         ; how many times we can mul b by b while result <= m
191         let log = \m b. (\base build. m build base (\cur go sofar. sofar))
192                 ; where base is
193                 (make_triple b true 0)
194                 ; and build is
195                 (\t. t (\cur go sofar. and go (leq cur m)
196                            (make_triple (mul cur b) true (succ sofar)) ; continue
197                            (make_triple cur false sofar) ; enough
198                 ))  in
199
200
201         ; Rosenbloom's fixed point combinator
202         let Y = \f. (\h. f (h h)) (\h. f (h h)) in
203         ; Turing's fixed point combinator
204         let Theta = (\u f. f (u u f)) (\u f. f (u u f))  in
205
206
207         ; length for version 1 lists
208         let length = Y (\self lst. isempty lst 0 (succ (self (tail lst))))  in
209
210
211         ; numhelper 0 f z ~~> z
212         ; when n > 0: numhelper n f z ~~> f (pred n)
213         ; compare Bunder/Urbanek pred
214         let numhelper = \n. n (\u v. v (u succ)) (K 0) (\p f z. f p)  in
215
216         ; accepts fixed point combinator as a parameter, so you can use different ones
217         let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1)  in
218
219
220
221         fact Theta 3  ; returns 6
222
223
224 <!--
225         ; my original efficient comparisons
226         let leq = (\base build consume. \m n. n consume (m build base) get_1st (\x. false) true)
227                         ; where base is
228                         (make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair
229                         ; and build is
230                         (\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)
231                         ; and consume is
232                         (\p. p get_2nd p)  in
233         let lt = \m n. not (leq n m) in
234         let eq = (\base build consume. \m n. n consume (m build base) true (\x. false) true)
235                         ; where base is
236                         (make_pair zero (K (make_pair one I)))
237                         ; and build is
238                         (\p. p (\x y. make_pair (succ x) (K p)))
239                         ; and consume is
240                         (\p. p get_2nd p)  in ; or
241 -->
242
243 <!--
244         gcd
245         pow_mod
246
247
248         show Oleg's definition of integers:
249                 church_to_int = \n sign. n
250                 church_to_negint = \n sign s z. sign (n s z)
251
252                 ; int_to_church
253                 abs = \int. int I
254
255                 sign_case = \int ifpos ifzero ifneg. int (K ifneg) (K ifpos) ifzero
256
257                 negate_int = \int. sign_case int (church_to_negint (abs int)) zero (church_to_int (abs int))
258
259         for more, see http://okmij.org/ftp/Computation/lambda-arithm-neg.scm
260
261 -->