; pairs
let make_pair = \x y f. f x y in
- let get_1st = \x y. x in ; aka true
- let get_2nd = \x y. y in ; aka false
+ let get_fst = \x y. x in ; aka true
+ let get_snd = \x y. y in ; aka false
; triples
let make_triple = \x y z f. f x y 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)
+ let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) get_snd)
; 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
; 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))
+ ; 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
+ ; from Oleg, of course it's the most elegant
+ ; revappend [a;b;c] [x;y] ~~> [c;b;a;x;y]
+ let revappend = \left. left (\hd sofar. \right. sofar (make_list hd right)) I in
+ let rev = \lst. revappend lst empty 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
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 isempty = \lst. lst get_fst in
+ let head = \lst. isempty lst err (lst get_snd get_fst) in
let tail_empty = empty in
- let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd) in
+ let tail = \lst. isempty lst tail_empty (lst get_snd get_snd) in
; more math with Church numerals
; three strategies for predecessor
let pred_zero = zero in
- let pred = (\shift n. n shift (make_pair zero pred_zero) get_2nd)
+ let pred = (\shift n. n shift (make_pair zero pred_zero) get_snd)
; where shift is
(\p. p (\x y. make_pair (succ x) x)) in ; or
; from Oleg; observe that for any Church numeral n: n I ~~> I
; more efficient comparisons, Oleg's gt provided some simplifications
- let leq = (\base build consume. \m n. n consume (m build base) get_1st)
+ let leq = (\base build consume. \m n. n consume (m build base) get_fst)
; where base is
(make_pair true junk)
; and build is
(\p. make_pair false p)
; and consume is
- (\p. p get_1st p (p get_2nd)) in
+ (\p. p get_fst p (p get_snd)) in
let lt = \m n. not (leq n m) in
- let eq = (\base build consume. \m n. n consume (m build base) get_1st)
+ let eq = (\base build consume. \m n. n consume (m build base) get_fst)
; 2nd element of a pair will now be of the form (K sthg) or I
; we supply the pair being consumed itself as an argument
; getting back either sthg or the pair we just consumed
; and build is
(\p. make_pair false (K p))
; and consume is
- (\p. p get_2nd p) in
+ (\p. p get_snd p) in
; -n is a fixedpoint of \x. add (add n x) x
(make_triple (succ cur) false (succ sofar)) ; continue
)) in
; or
- let sub = (\base build consume. \m n. n consume (m build base) get_1st)
+ let sub = (\base build consume. \m n. n consume (m build base) get_fst)
; where base is
(make_pair zero I) ; see second defn of eq for explanation of 2nd element
; and build is
(\p. p (\x y. make_pair (succ x) (K p)))
; and consume is
- (\p. p get_2nd p) in
+ (\p. p get_snd p) in
let min = \m n. sub m (sub m n) in
; and mtail is
(\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz))))
in
- let div = \n d. divmod n d get_1st in
- let mod = \n d. divmod n d get_2nd in
+ let div = \n d. divmod n d get_fst in
+ let mod = \n d. divmod n d get_snd in
; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x
let Theta = (\u f. f (u u f)) (\u f. f (u u f)) in
+ ; now you can search for primes, do encryption :-)
+ let gcd = Y (\gcd m n. iszero n m (gcd n (mod m n))) in ; or
+ let gcd = \m n. iszero m n (Y (\gcd m n. iszero n m (lt n m (gcd (sub m n) n) (gcd m (sub n m)))) m n) in
+ let lcm = \m n. or (iszero m) (iszero n) 0 (mul (div m (gcd m n)) n) in
+
+
; length for version 1 lists
let length = Y (\self lst. isempty lst 0 (succ (self (tail lst)))) in
<!--
; my original efficient comparisons
- let leq = (\base build consume. \m n. n consume (m build base) get_1st (\x. false) true)
+ let leq = (\base build consume. \m n. n consume (m build base) get_fst (\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
+ (\p. p get_snd 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
; and build is
(\p. p (\x y. make_pair (succ x) (K p)))
; and consume is
- (\p. p get_2nd p) in ; or
+ (\p. p get_snd p) in ; or
-->
<!--
; (might_for_all_i_know_still_be_equal?, tail_of_reversed_right)
; when left is empty, the lists are equal if right is empty
(make_pair
- (not (isempty right))
+ true ; for all we know so far, they might still be equal
(reverse right)
)
; when fold is finished, check sofar-pair
(\might_be_equal right_tail. and might_be_equal (isempty right_tail))
+
+; most elegant
+let list_equal = \left. left (\hd sofar. \right. and (and (not (isempty right)) (eq hd (head right))) (sofar (tail right))) isempty
+
-->