the succ fixed point as arithmetic infinity

[lambda.git] / topics / _week4_fixed_point_combinator.mdwn

diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn
index 30b3745..01185c4 100644 (file)
--- 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.
 
 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)
 
     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.  
 
 
     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)
     
 
     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?##
 
 
 ##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.
 
 
 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###
 
 
 ###Varieties of fixed-point combinators###