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=01185c40fcf53c5354557694aceba5734a859de1;hp=30b3745e1e6840c54fe3b5e511b7b48edf1f5826;hb=c755fb35412150c91b5dc7ec2efdc2a28aa6cac3;hpb=02807170e61a338b91cc8f094837372a3c55a359

diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn
index 30b3745e..01185c40 100644
--- a/topics/_week4_fixed_point_combinator.mdwn
+++ b/topics/_week4_fixed_point_combinator.mdwn
@@ -360,29 +360,52 @@ Works!
 Let's do one more example to illustrate.  We'll do `K`, since we
 wondered above whether it had a fixed point.
 
+Before we begin, we can reason a bit about what the fixed point must
+be like.  We're looking for a fixed point for `K`, i.e., `\xy.x`.  `K`
+ignores its second argument.  That means that no matter what we give
+`K` as its first argument, the result will ignore the next argument
+(that is, `KX` ignores its first argument, no matter what `X` is).  So
+if `KX <~~> X`, `X` had also better ignore its first argument.  But we
+also have `KX == (\xy.x)X ~~> \y.X`.  This means that if `X` ignores
+its first argument, then `\y.X` will ignore its first two arguments.
+So once again, if `KX <~~> X`, `X` also had better ignore at least its
+first two arguments.  Repeating this reasoning, we realize that `X`
+must be a function that ignores an infinite series of arguments.  
+Our expectation, then, is that our recipe for finding fixed points
+will build us a function that somehow manages to ignore an infinite
+series of arguments.
+
     h := \xy.x
     H := \f.h(ff) == \f.(\xy.x)(ff) ~~> \fy.ff
     H H := (\fy.ff)(\fy.ff) ~~> \y.(\fy.ff)(\fy.ff)
 
-Ok, it doesn't have a normal form.  But let's check that it is in fact
-a fixed point:
+Let's check that it is in fact a fixed point:
 
     K(H H) == (\xy.x)((\fy.ff)(\fy.ff)
            ~~> \y.(\fy.ff)(\fy.ff)
 
 Yep, `H H` and `K(H H)` both reduce to the same term.  
 
-This fixed point is bit wierd.  Let's reduce it a bit more:
+To see what this fixed point does, let's reduce it a bit more:
 
     H H == (\fy.ff)(\fy.ff)
         ~~> \y.(\fy.ff)(\fy.ff)
         ~~> \yy.(\fy.ff)(\fy.ff)
         ~~> \yyy.(\fy.ff)(\fy.ff)
     
-It appears that where `K` is a function that ignores (only) the first
-argument you feed to it, the fixed point of `K` ignores an endless,
-infinite series of arguments.  It's a write-only memory, a black hole.
+Sure enough, this fixed point ignores an endless, infinite series of
+arguments.  It's a write-only memory, a black hole.
+
+Now that we have one fixed point, we can find others, for instance,
+
+    (\fy.fff)(\fy.fff) 
+    ~~> \y.(\fy.fff)(\fy.fff)(\fy.fff)
+    ~~> \yy.(\fy.fff)(\fy.fff)(\fy.fff)(\fy.fff)
+    ~~> \yyy.(\fy.fff)(\fy.fff)(\fy.fff)(\fy.fff)(\fy.fff)
 
+Continuing in this way, you can now find an infinite number of fixed
+points, all of which have the crucial property of ignoring an infinite
+series of arguments.
 
 ##What is a fixed point for the successor function?##
 
@@ -403,18 +426,73 @@ 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.
 
-Moreover, 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 neither `X` nor `f X`
-have normal forms. (Indeed, what they give us for the square function
-isn't any of the Church numerals, but is rather an expression with no
-normal form.) However, if we take care we can ensure that we *do* get
-terminating fixed points. And this gives us a principled, fully
-general strategy for doing recursion. It lets us define even functions
-like the Ackermann function, which were until now out of our reach. It
-would also let us define arithmetic and list functions on the "version
-1" and "version 2" implementations, where it wasn't always clear how
-to force the computation to "keep going."
+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
+neither `X` nor `f X` have normal forms. (Indeed, what they give us
+for the square function isn't any of the Church numerals, but is
+rather an expression with no normal form.) However, if we take care we
+can ensure that we *do* get terminating fixed points. And this gives
+us a principled, fully general strategy for doing recursion. It lets
+us define even functions like the Ackermann function, which were until
+now out of our reach. It would also let us define arithmetic and list
+functions on the "version 1" and "version 2" implementations, where it
+wasn't always clear how to force the computation to "keep going."
 
 ###Varieties of fixed-point combinators###