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
32 let make_triple = \x y z f. f x y z in
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
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
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
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)
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
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
68 let pred = \n s z. n (\u v. v (u s)) (K z) I in ; or
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
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)
80 (\p. make_pair false p)
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
89 (make_pair true (K (make_pair false I)))
91 (\p. make_pair false (K p))
96 ; -n is a fixedpoint of \x. add (add n x) x
97 ; but unfortunately Y that_function doesn't normalize
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))
103 (make_triple n false zero)
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
110 let sub = (\base build consume. \m n. n consume (m build base) get_fst)
112 (make_pair zero I) ; see second defn of eq for explanation of 2nd element
114 (\p. p (\x y. make_pair (succ x) (K p)))
119 let min = \m n. sub m (sub m n) in
120 let max = \m n. add n (sub m n) in
123 ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x
124 ; but unfortunately Y that_function doesn't normalize
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))
129 (make_triple m true zero)
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
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))
140 (\p. p (\cur go. and go (leq n cur)
141 (make_pair (sub cur n) true) ; continue
142 (make_pair cur false) ; enough
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) )
151 (make_triple succ (K 0) I) ; see second defn of eq for explanation of 3rd element
153 (\t. make_triple I succ (K t))
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
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
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
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))
170 (make_triple b true 0)
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
178 ;; fixed point combinators
180 let Y = \f. (\h. f (h h)) (\h. f (h h)) in
182 let Theta = (\u f. f (u u f)) (\u f. f (u u f)) in
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
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
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
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)
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))
233 (make_pair empty (map (\h u. u h) right))
235 (\h sofar. sofar (\x y. isempty y
237 (make_pair (make_list (\u. head y (u h)) x) (tail y))
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
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
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
258 (\hd sofar continue_handler abort_handler. abort_handler false)
261 ; here's the continue_handler for the leftmost application of f2
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
269 (\hd sofar continue_handler abort_handler. continue_handler hd)
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
277 (\h sofar continue_handler abort_handler. continue_handler (sofar (\t y. make_pair (make_list h t) t)))
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
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
293 (\hd sofar continue_handler abort_handler. abort_handler hd)
296 ; here are our continue_handler and abort_handler
297 larger_computation larger_computation in
298 let tail = \lst larger_computation. lst
300 (\h sofar continue_handler abort_handler. continue_handler (sofar (\j a b. b empty) (\t a b. b (make_right_list h t)) ) )
303 ; here are our continue_handler and abort_handler
304 (\sofar. sofar larger_computation larger_computation) unused in
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
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
322 fact Theta 3 ; returns 6
326 ; my original efficient comparisons
327 let leq = (\base build consume. \m n. n consume (m build base) get_fst (\x. false) true)
329 (make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair
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)
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)
337 (make_pair zero (K (make_pair one I)))
339 (\p. p (\x y. make_pair (succ x) (K p)))
341 (\p. p get_snd p) in ; or
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)
356 sign_case = \int ifpos ifzero ifneg. int (K ifneg) (K ifpos) ifzero
358 negate_int = \int. sign_case int (church_to_negint (abs int)) zero (church_to_int (abs int))
360 for more, see http://okmij.org/ftp/Computation/lambda-calc.html#neg
370 ; deconstruct our sofar-pair
371 sofar (\might_be_equal right_tail.
374 (and (and might_be_equal (not (isempty right_tail))) (eq? hd (head right_tail)))
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
382 true ; for all we know so far, they might still be equal
385 ; when fold is finished, check sofar-pair
386 (\might_be_equal right_tail. and might_be_equal (isempty right_tail))
389 let list_equal = \left. left (\hd sofar. \right. and (and (not (isempty right)) (eq hd (head right))) (sofar (tail right))) isempty