From: Chris <chris.barker@nyu.edu>
Date: Tue, 17 Feb 2015 21:56:13 +0000 (-0500)
Subject: edits
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=40a9e529a03f11246b1f6fba8e98a670c4631639;ds=sidebyside

edits
---

diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn
index b430f2fd..da2771a0 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 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?##