From: Jim Pryor Date: Thu, 30 Sep 2010 18:14:19 +0000 (-0400) Subject: tweaked arithmetic X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=af844d6cdbd502a2fe9aa0756ab83a84ff66909d tweaked arithmetic Signed-off-by: Jim Pryor --- diff --git a/arithmetic.mdwn b/arithmetic.mdwn index e948f0b4..fc7249f6 100644 --- a/arithmetic.mdwn +++ b/arithmetic.mdwn @@ -22,6 +22,15 @@ 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: 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 @@ -31,7 +40,7 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so 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 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 @@ -42,19 +51,13 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so 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 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 - ; Church numerals: easy 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 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