X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week4_fixed_point_combinator.mdwn;h=c93a16ba2c887ff8fb64bc8c320f3e8d99fb3bff;hp=eca5fc999827f3111786c2576370c8bd31d47a52;hb=ebbcaf727cfdc7d8f183a2b6af0b77262efb691f;hpb=4a07497cdbb0a542147be199747b10a689396837

diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn
index eca5fc99..c93a16ba 100644
--- 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.
 
-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