X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=lambda_library.mdwn;h=5623b9fa219b4cf9ef0fca41b8fe098768b803df;hp=f0b4f44157193f09f2620d32ca556ba649cd0dfc;hb=48b6ae024e8268541a5b6be4d87f4894e357e4a1;hpb=273f2590356318a9d496b49b48af330711382a3c

diff --git a/lambda_library.mdwn b/lambda_library.mdwn
index f0b4f441..5623b9fa 100644
--- a/lambda_library.mdwn
+++ b/lambda_library.mdwn
@@ -27,8 +27,8 @@ and all sorts of other places. Others of them are our own handiwork.
 
 	; 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
@@ -50,7 +50,7 @@ and all sorts of other places. Others of them are our own handiwork.
 	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
@@ -82,10 +82,10 @@ and all sorts of other places. Others of them are our own handiwork.
 
 	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
@@ -104,7 +104,7 @@ and all sorts of other places. Others of them are our own handiwork.
 
 	; 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
@@ -127,15 +127,15 @@ and all sorts of other places. Others of them are our own handiwork.
 
 
 	; 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
@@ -144,7 +144,7 @@ and all sorts of other places. Others of them are our own handiwork.
 			; 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
@@ -161,13 +161,13 @@ and all sorts of other places. Others of them are our own handiwork.
 						(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
@@ -208,8 +208,8 @@ and all sorts of other places. Others of them are our own handiwork.
 				; 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
@@ -259,13 +259,13 @@ and all sorts of other places. Others of them are our own handiwork.
 
 <!--
 	; 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
@@ -273,7 +273,7 @@ and all sorts of other places. Others of them are our own handiwork.
 			; 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
 -->
 
 <!--
@@ -296,3 +296,28 @@ and all sorts of other places. Others of them are our own handiwork.
 
 
 -->
+
+<!--
+let list_equal =
+    \left right. left
+                ; here's our f
+                (\hd sofar.
+                    ; deconstruct our sofar-pair
+                    sofar (\might_be_equal right_tail.
+                        ; our new sofar
+                        make_pair
+                        (and (and might_be_equal (not (isempty right_tail))) (eq? hd (head right_tail)))
+                        (tail right_tail)
+                    ))
+                ; here's our z
+                ; we pass along the fold a pair
+                ; (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))
+                    (reverse right)
+                )
+                ; when fold is finished, check sofar-pair
+                (\might_be_equal right_tail. and might_be_equal (isempty right_tail))
+-->
+