index 74a354d..fafecaf 100644 (file)
@@ -22,12 +22,62 @@ 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_empty = empty  in
+       let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) 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
+       let singleton = \x f z. f x z  in
+       ; append [a;b;c] [x;y;z] ~~> [a;b;c;x;y;z]
+       let append = \left right. left make_list right  in
+       ; very inefficient but correct reverse
+       let reverse = \lst. lst (\h sofar. append sofar (singleton h)) empty  in ; or
+       ; more efficient reverse builds a left-fold instead
+       ; (make_left_list a (make_left_list b (make_left_list c empty)) ~~> \f z. f c (f b (f a z))
+       let reverse = (\make_left_list lst. lst make_left_list empty) (\h t f z. t f (f h z))  in
+       ; zip [a;b;c] [x; y; z] ~~> [(a,x);(b,y);(c,z)]
+       let zip = \left right. (\base build. reverse left build base (\x y. reverse x))
+                       ; where base is
+                       (make_pair empty (map (\h u. u h) right))
+                       ; and build is
+                       (\h sofar. sofar (\x y. isempty y
+                                               sofar
+                                               (make_pair (make_list (\u. head y (u h)) x)  (tail y))
+                       ))  in
+       let all = \f lst. lst (\h sofar. and sofar (f h)) true  in
+       let any = \f lst. lst (\h sofar. or sofar (f h)) false  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 +89,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 +114,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 +134,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
@@ -123,9 +157,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
@@ -163,9 +199,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
@@ -179,40 +217,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
+
+       ; Rosenbloom'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
-
+       let Theta = (\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 +237,45 @@ 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

+       fact Theta 3  ; returns 6
+
+
+<!--
+       ; my original 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
+-->
+
+<!--
+       gcd
+       pow_mod
+
+
+       show Oleg's definition of integers:
+               church_to_int = \n sign. n
+               church_to_negint = \n sign s z. sign (n s z)
+
+               ; int_to_church
+               abs = \int. int I
+
+               sign_case = \int ifpos ifzero ifneg. int (K ifneg) (K ifpos) ifzero
+
+               negate_int = \int. sign_case int (church_to_negint (abs int)) zero (church_to_int (abs int))
+
+       for more, see http://okmij.org/ftp/Computation/lambda-arithm-neg.scm

+-->