moved fixed point for succ to exercises

[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 b430f2f..c93a16b 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 second
-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,18 @@ 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."
+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###