From: Jim Pryor Date: Thu, 30 Sep 2010 18:02:34 +0000 (-0400) Subject: added a bunch of math etc X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=14458e59f4e02fa020bc26a30512cbfa35eec2e2;ds=sidebyside added a bunch of math etc Signed-off-by: Jim Pryor --- diff --git a/arithmetic.mdwn b/arithmetic.mdwn new file mode 100644 index 00000000..dd59863e --- /dev/null +++ b/arithmetic.mdwn @@ -0,0 +1,226 @@ + + ; booleans + let true = \y n. y in ; aka K + let false = \y n. n in ; aka K I + let and = \p q. p q false in ; or + let and = \p q. p q p in ; aka S C I + let or = \p q. p true q in ; or + let or = \p q. p p q in ; aka M + let not = \p. p false true in ; or + let not = \p y n. p n y in ; aka C + let xor = \p q. p (not q) q in + let iff = \p q. not (xor p q) in ; or + let iff = \p q. p q (not q) in + + ; pairs + let make_pair = \x y f. f x y in + let get_1st = \x y. x in ; aka true + let get_2nd = \x y. y in ; aka false + + ; triples + let make_triple = \x y z f. f x y z in + + + ; Church numerals + let zero = \s z. z in ; aka false + let one = \s z. s z in ; aka I + let succ = \n s z. s (n s z) in + ; for any Church numeral n > zero : n (K y) z ~~> y + let iszero = \n. n (\x. false) true in + let add = \m n. m succ n in ; or + let add = \m n s z. m s (n s z) in + let mul = \m n. m (\z. add n z) zero in ; or + let mul = \m n s. m (n s) in + let pow = \b exp. exp (mul b) one in ; or + ; b succ : adds b + ; b (b succ) ; adds b b times, ie adds b^2 + ; b (b (b succ)) ; adds b^2 b times, ie adds b^3 + ; exp b succ ; adds b^exp + let pow = \b exp s z. exp b s z in + + ; three strategies for predecessor + let pred_zero = zero in + let pred = (\shift n. n shift (make_pair zero pred_zero) get_2nd) + ; where shift is + (\p. p (\x y. make_pair (succ x) x)) in ; or + ; from Oleg; observe that for any Church numeral n: n I ~~> I + let pred = \n. iszero n zero + ; else + (n (\x. x I ; when x is the base term, this will be K zero + ; when x is a Church numeral, it will be I + (succ x)) + ; base term + (K (K zero)) + ) in + ; from Bunder/Urbanek + let pred = \n s z. n (\u v. v (u s)) (K z) I in ; or + + + ; inefficient but simple comparisons + let leq = \m n. iszero (n pred m) in + let lt = \m n. not (leq n m) in + let eq = \m n. and (leq m n) (leq n m) in ; or + + + ; more efficient comparisons + let leq = (\base build consume. \m n. n consume (m build base) get_1st (\x. false) true) + ; where base is + (make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair + ; and build is + (\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) + ; and consume is + (\p. p get_2nd p) in + let lt = \m n. not (leq n m) in + let eq = (\base build consume. \m n. n consume (m build base) true (\x. false) true) + ; where base is + (make_pair zero (K (make_pair one I))) + ; and build is + (\p. p (\x y. make_pair (succ x) (K p))) + ; and consume is + (\p. p get_2nd p) in ; or + + + ; more efficient comparisons, Oleg's gt provided some simplification + let leq = (\base build consume. \m n. n consume (m build base) get_1st) + ; where base is + (make_pair true junk) + ; and build is + (\p. make_pair false p) + ; and consume is + (\p. p get_1st p (p get_2nd)) in + let lt = \m n. not (leq n m) in + let eq = (\base build consume. \m n. n consume (m build base) get_1st) + ; 2nd element of a pair will now be of the form (K sthg) or I + ; we supply the pair being consumed itself as an argument + ; getting back either sthg or the pair we just consumed + ; base is + (make_pair true (K (make_pair false I))) + ; and build is + (\p. make_pair false (K p)) + ; and consume is + (\p. p get_2nd p) in + + ; -n is a fixedpoint of \x. add (add n x) x + ; but unfortunately Y that_function doesn't normalize + ; instead: + let sub = \m n. n pred m in ; or + ; how many times we can succ n until m <= result + let sub = \m n. (\base build. m build base (\cur fin sofar. sofar)) + ; where base is + (make_triple n false zero) + ; and build is + (\t. t (\cur fin sofar. or fin (leq m cur) + (make_triple cur true sofar) ; enough + (make_triple (succ cur) false (succ sofar)) ; continue + )) in + ; or + let sub = (\base build consume. \m n. n consume (m build base) get_1st) + ; where base is + (make_pair zero I) ; see second defn of eq for explanation of 2nd element + ; and build is + (\p. p (\x y. make_pair (succ x) (K p))) + ; and consume is + (\p. p get_2nd p) in + + let min = \m n. sub m (sub m n) in + let max = \m n. add n (sub m n) in + + ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x + ; but unfortunately Y that_function doesn't normalize + ; instead: + ; how many times we can sub n from m while n <= result + let div = \m n. (\base build. m build base (\cur go sofar. sofar)) + ; where base is + (make_triple m true zero) + ; and build is + (\t. t (\cur go sofar. and go (leq n cur) + (make_triple (sub cur n) true (succ sofar)) ; continue + (make_triple cur false sofar) ; enough + )) in + ; what's left after sub n from m while n <= result + let mod = \m n. (\base build. m build base (\cur go. cur)) + ; where base is + (make_pair m true) + ; and build is + (\p. p (\cur go. and go (leq n cur) + (make_pair (sub cur n) true) ; continue + (make_pair cur false) ; enough + )) in + + ; or + let divmod = (\base build mtail. \m n. + (\dhead. m (mtail dhead) (\sel. dhead (sel 0 0))) + (n build base (\x y z. z junk)) + (\t u x y z. make_pair t u) ) + ; where base is + (make_triple succ (K 0) I) ; see second defn of eq for explanation of 3rd element + ; and build is + (\t. make_triple I succ (K t)) + ; and mtail is + (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz)))) + in + let div = \n d. divmod n d get_1st in + let mod = \n d. divmod n d get_2nd in + + ; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x + ; but unfortunately Y that_function doesn't normalize + + ; (log base b of m) is a fixedpoint of \x. add (sub (pow b x) m) x + ; but unfortunately Y that_function doesn't normalize + ; instead: + ; how many times we can mul b by b while result <= m + let log = \m b. (\base build. m build base (\cur go sofar. sofar)) + ; where base is + (make_triple b true 0) + ; and build is + (\t. t (\cur go sofar. and go (leq cur m) + (make_triple (mul cur b) true (succ sofar)) ; continue + (make_triple cur false sofar) ; enough + )) in + + ; Curry's fixed point combinator + let Y = \f. (\h. f (h h)) (\h. f (h h)) in + ; Turing's fixed point combinator + let Z = (\u f. f (u u f)) (\u f. f (u u f)) in + + + + + ; version 3 lists + let empty = \f z. z in + let make_list = \h t f z. f h (t f z) in + let isempty = \lst. lst (\h sofar. false) true in + let head = \lst. lst (\h sofar. h) junk in + let tail = \lst. (\shift lst. lst shift (make_pair empty junk) get_2nd) + ; where shift is + (\h p. p (\t y. make_pair (make-list h t) t)) in + let length = \lst. lst (\h sofar. succ sofar) zero in + let map = \f lst. lst (\h sofar. make_list (f h) sofar) empty in + let filter = \f lst. lst (\h sofar. f h (make_list h sofar) sofar) empty in ; or + let filter = \f lst. lst (\h. f h (make_list h) I) empty in + + + ; version 1 lists + let empty = make_pair true junk in + let make_list = \h t. make_pair false (make_pair h t) in + let isempty = \lst. lst get_1st in + let head = \lst. isempty lst error (lst get_2nd get_1st) in + let tail_empty = empty in + let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd) in + + let length = Y (\self lst. isempty lst 0 (succ (self (tail lst)))) in + + + + ; numhelper 0 f z ~~> z + ; when n > 0: numhelper n f z ~~> f (pred n) + ; compare Bunder/Urbanek pred + let numhelper = \n. n (\u v. v (u succ)) (K 0) (\p f z. f p) in + + ; accepts fixed point combinator as a parameter, so you can use different ones + let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1) in + + + fact Z 3 ; returns 6 + +