code/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