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