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