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
+
+ ; append list2 to list1 with: list1 make_list list2
+ let singleton = \x f z. f x z in
+ let reverse = \lst. lst (\h sofar. sofar make_list (singleton h)) empty in
+ let zip = \left right. left (\h sofar. sofar (\x y. isempty y
+ sofar
+ (make_pair (make_list () x) (tail y))
+ )
+ (make_pair empty (map right (\h u v. u v h)))
+ )
+ (\x y. reverse x) 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
; 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)
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)
; 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:
; 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:
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:
(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
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
+-->