moved fixed point for succ to exercises

diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn
index eca5fc9..c93a16b 100644 (file)
--- a/topics/_week4_fixed_point_combinator.mdwn
+++ b/topics/_week4_fixed_point_combinator.mdwn
@@ -426,61 +426,6 @@ who knows what we'd get back? Perhaps there's some non-number-representing formu
 
 Yes! That's exactly right. And which formula this is will depend on the particular way you've implemented the successor function.
 
 
 Yes! That's exactly right. And which formula this is will depend on the particular way you've implemented the successor function.
 

-Let's pick a way of defining the successor function and reason about it.
-Here is one way that is compatible with the constraints given in
-homework 2: `succ := \nfz.f(nfz)`.  This takes a Church
-number, and returns the next Church number.  For instance, 
-
-    succ 2 == succ (\fz.f(fz)) 
-           == (\nfz.f(nfz)) (\fz.f(fz))
-           ~~> \fz.f((\fz.f(fz))fz)
-           ~~> \fz.f(f(fz))
-           == 3
-
-Using logic similar to the discussion above of the fixed point for K,
-we can say that for any Church number argument to the successor
-function, the result will be the next Church number.  Assume that
-there is some Church number `n` that is a fixed point.  Then
-`succ n <~~> n` (because `n` is a fixed point) and `succ n <~~> n + 1`
-(since that's what the successor function does).  By the Church Rosser
-theorem, `n <~~> n + 1`.  What kind of `n` could satisfy that
-requirement?
-
-Let's run the recipe:
-
-    H := \f . succ (ff)
-      == \f . (\nfz.f(nfz)) (ff)
-      ~~> \h . (\nfz.f(nfz)) (hh)
-      ~~> \hfz.f(hhfz)
-
-    H H == (\hfz.f(hhfz)) (\hfz.f(hhfz))
-        ~~> \fz.f((\hfz.f(hhfz))(\hfz.f(hhfz))fz)
-        ~~> \fz.f(f((\hfz.f(hhfz))(\hfz.f(hhfz))fz))
-        ~~> \fz.f(f(f((\hfz.f(hhfz))(\hfz.f(hhfz))fz))
-
-We can see that the fixed point generates an endless series of `f`'s.
-In terms of Church numbers, this is a way of representing infinity:
-if the size of a Church number is the number `f`'s it contains, and
-this Church number contains an unbounded number of `f`'s, then its
-size is unbounded.  
-
-We can also see how this candidate for infinity behaves with respect
-to our other arithmetic operators.
-
-    add 2 (HH) == (\mnfz.mf(nfz)) (\fz.f(fz)) (H H)
-               ~~> \fz.(\fz.f(fz)) f ((HH)fz)
-               ~~> \fz.\z.f(fz) ((HH)fz)
-               ~~> \fz.f(f((HH)fz))
-               ==  \fz.f(f(((\hfz.f(hhfz)) (\hfz.f(hhfz)))fz))
-               ~~> \fz.f(f((\fz.f((\hfz.f(hhfz)) (\hfz.f(hhfz))))fz))
-               ~~> \fz.f(f(f((\hfz.f(hhfz)) (\hfz.f(hhfz)))))
-
-So `2 + (HH) <~~> (HH)`.  This is what we expect from arithmetic infinity.
-You can check to see if `2 * (HH) <~~> (HH)`.
-
-So our fixed point recipe has delivere a reasonable candidate for
-arithmetic infinity. 
-

 One (by now obvious) upshot is that the recipes that enable us to name
 fixed points for any given formula aren't *guaranteed* to give us
 *terminating* fixed points. They might give us formulas X such that
 One (by now obvious) upshot is that the recipes that enable us to name
 fixed points for any given formula aren't *guaranteed* to give us
 *terminating* fixed points. They might give us formulas X such that