From: Chris Barker <barker@kappa.(none)>
Date: Mon, 4 Oct 2010 00:37:14 +0000 (-0400)
Subject: Merge branch 'master' of ssh://server.philosophy.fas.nyu.edu/Users/lambda/lambda
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=bea2932d9f91273c294112b7c896229fa7398158;hp=d7c9144dc2558e867db336c1c36961fb0d19fdad

Merge branch 'master' of ssh://server.philosophy.fas.nyu.edu/Users/lambda/lambda
---

diff --git a/assignment4.mdwn b/assignment4.mdwn
index 9f566758..54a3bf20 100644
--- a/assignment4.mdwn
+++ b/assignment4.mdwn
@@ -81,7 +81,7 @@ Suppose we had a pair of fixed point operators, `Y1` and `Y2`, that operated on
 If we gave you such a `Y1` and `Y2`, how would you implement the above definitions of `even` and `odd`?
 
 					
-<LI>(More challenging.) Using our derivation of Y from the [[Week2]] notes as a model, construct a pair `Y1` and `Y2` that behave in the way described.
+<LI>(More challenging.) Using our derivation of Y from the [Week3 notes](/week3/#index4h2) as a model, construct a pair `Y1` and `Y2` that behave in the way described.
 
 (See [[hints/Assignment 4 hint 4]] if you need some hints.)
 
diff --git a/hints/assignment_4_answer_4.mdwn b/hints/assignment_4_answer_4.mdwn
new file mode 100644
index 00000000..c2cd1fd7
--- /dev/null
+++ b/hints/assignment_4_answer_4.mdwn
@@ -0,0 +1,29 @@
+
+
+	let Y1 = \t1 t2.
+				(\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem1
+				(\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem1
+				(\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem2
+			in
+
+	let Y2 = \t1 t2.
+				(\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem2
+				(\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem1
+				(\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elem2)) ; elem2
+			in
+
+
+	X1 === Y1 t1 t2 ~~> elem1 elem1 elem2
+			 === (\elem1 elem2. t1 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
+			 ~~> t1 (elem1 elem1 elem2) (elem2 elem1 elem2)
+			<~~> t1 (Y1 t1 t2) (Y2 t1 t2)
+			 === t1 X1 X2
+
+			and
+
+	X2 === Y2 t1 t2 ~~> elem2 elem1 elem2
+			 === (\elem1 elem2. t2 (elem1 elem1 elem2) (elem2 elem1 elems2)) elem1 elem2
+			 ~~> t2 (elem1 elem1 elem2) (elem2 elem1 elem2)
+			<~~> t2 (Y1 t1 t2) (Y2 t1 t2)
+			 === t2 X1 X2
+
diff --git a/hints/assignment_4_hint_4.mdwn b/hints/assignment_4_hint_4.mdwn
index a30b4861..9cfef8ad 100644
--- a/hints/assignment_4_hint_4.mdwn
+++ b/hints/assignment_4_hint_4.mdwn
@@ -1,2 +1,26 @@
 Hints for Y1,Y2. 
 
+*	Begin by trying to define `X1` and `X2` directly, then once they're working, you can abstract back to a pair of combinators `Y1` and `Y2` that generate `X1` and `X2` for a given pair of arguments `T1` and `T2`.
+
+	You want:
+
+		X1 <~~> T1 X1 X2 and
+		X2 <~~> T2 X1 X2
+
+*	X1 is presumably going to have some form like:
+
+		(\elem1 elem2 ... (T1
+							(do-something-with-the-elems-to-make-X1)
+							(do-something-with-the-elems-to-make-X2)
+						  ))
+		some-elem1 some-elem2 ...
+	
+	Right? What will the form of X2 be?
+
+*	Can you see how to go on?
+
+*	Call the displayed abstract above `(\elem1 elem2 ... (...))` "elem0". What's the relation between `X1`, `elem0`, `elem1`, `elem2`...?
+
+*	Go on, now you can do it.
+
+