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

diff --git a/assignment4.mdwn b/assignment4.mdwn
index 9f56675..54a3bf2 100644 (file)
--- 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 (file)
index 0000000..c2cd1fd
--- /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 a30b486..9cfef8a 100644 (file)
--- 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.
+
+