tweaked arithmetic

[lambda.git] / arithmetic.mdwn

diff --git a/arithmetic.mdwn b/arithmetic.mdwn
index e948f0b..fc7249f 100644 (file)
--- 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