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