X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=arithmetic.mdwn;h=289b28438916da6ca8a35ff9d23b34e772e43177;hp=f7406ccb66f7a1da09841d65d2a8274fd0e1c61a;hb=e1860468dc97e6249ecd19e96a2e7fffe9430d0e;hpb=1b71f17d39016a953ec7f2bac55f159e716521b4

diff --git a/arithmetic.mdwn b/arithmetic.mdwn
index f7406ccb..289b2843 100644
--- a/arithmetic.mdwn
+++ b/arithmetic.mdwn
@@ -1,5 +1,17 @@
 Here are a bunch of pre-tested operations for the untyped lambda calculus. In some cases multiple versions are offered.
 
+Some of these are drawn from:
+
+*	[[!wikipedia Lambda calculus]]
+*	[[!wikipedia Church encoding]]
+*	Oleg's [Basic Lambda Calculus Terms](http://okmij.org/ftp/Computation/lambda-calc.html#basic)
+
+and all sorts of other places. Others of them are our own handiwork.
+
+
+**Spoilers!** Below you'll find implementations of map and filter for v3 lists, and several implementations of leq for Church numerals. Those were all requested in Assignment 2; so if you haven't done that yet, you should try to figure them out on your own. (You can find implementations of these all over the internet, if you look for them, so these are no great secret. In fact, we'll be delighted if you're interested enough in the problem to try to think through alternative implementations.)
+
+
 	; booleans
 	let true = \y n. y  in ; aka K
 	let false = \y n. n  in ; aka K I
@@ -37,14 +49,34 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so
 	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)
+	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
 
@@ -198,16 +230,20 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so
 		))  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
 
 
 	; length for version 1 lists
 	let length = Y (\self lst. isempty lst 0 (succ (self (tail lst))))  in
 
 
+	true
+
+<!--
+
 	; numhelper 0 f z ~~> z
 	; when n > 0: numhelper n f z ~~> f (pred n)
 	; compare Bunder/Urbanek pred
@@ -218,8 +254,8 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so
 
 
 
-	fact Z 3  ; returns 6
-
+	fact Theta 3  ; returns 6
+-->
 
 <!--
 	; my original efficient comparisons
@@ -239,3 +275,24 @@ Here are a bunch of pre-tested operations for the untyped lambda calculus. In so
 			; 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-calc.html#neg
+
+
+-->