X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=arithmetic.mdwn;h=f7406ccb66f7a1da09841d65d2a8274fd0e1c61a;hp=74a354d5d242ac424aeb60def78b909c1f4a8df5;hb=1b71f17d39016a953ec7f2bac55f159e716521b4;hpb=0b6773ac5f9a85495b837f80a39ad84e60a77854 diff --git a/arithmetic.mdwn b/arithmetic.mdwn index 74a354d5..f7406ccb 100644 --- a/arithmetic.mdwn +++ b/arithmetic.mdwn @@ -22,12 +22,42 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so let make_triple = \x y z f. f x y z in - ; Church numerals + ; Church numerals: basic operations + 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 + + + ; 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) 0 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 err (lst get_2nd get_1st) in + let tail_empty = empty in + let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd) in + + + ; more math with Church numerals + 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 @@ -39,6 +69,7 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so ; 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) @@ -63,25 +94,7 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so 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 + ; more efficient comparisons, Oleg's gt provided some simplifications let leq = (\base build consume. \m n. n consume (m build base) get_1st) ; where base is (make_pair true junk) @@ -101,6 +114,7 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so ; 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: @@ -123,9 +137,11 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so ; 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: @@ -163,9 +179,11 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so 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: @@ -179,40 +197,17 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so (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 - + ; length for version 1 lists 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 @@ -222,6 +217,25 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1) in + fact Z 3 ; returns 6 +