X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek4_fixed_point_combinators.mdwn;h=41a5273751c7fc6ca4fcf5c5e01d8f23f176f6e8;hp=601ad813bdd87e87521b80a0965e8803cbc1219a;hb=7d5f235b46a5fb4ac8d6aaeffa65d0244522bdd0;hpb=a29958c3e11fa8ae383aacff54ce7f405def0705

diff --git a/topics/week4_fixed_point_combinators.mdwn b/topics/week4_fixed_point_combinators.mdwn
index 601ad813..41a52737 100644
--- a/topics/week4_fixed_point_combinators.mdwn
+++ b/topics/week4_fixed_point_combinators.mdwn
@@ -281,7 +281,7 @@ saying that we are looking for a fixed point for `h`:
 
     h LENGTH <~~> LENGTH
 
-Replacing `h` with its definition, we have
+Replacing `h` with its definition, we have:
 
     (\xs. (empty? xs) 0 (succ (LENGTH (tail xs)))) <~~> LENGTH
 
@@ -289,10 +289,21 @@ If we can find a value for `LENGTH` that satisfies this constraint, we'll
 have a function we can use to compute the length of an arbitrary list.
 All we have to do is find a fixed point for `h`.
 
-The strategy we will present will turn out to be a general way of
+Let's reinforce this. The left-hand side has the form:
+
+    (\body. Φ[...body...]) LENGTH
+
+which beta-reduces to:
+
+    Φ[...LENGTH...]
+
+where that whole formula is convertible with the term `LENGTH` itself. In other words, the term `Φ[...LENGTH...]` contains (a term that convertible with) itself --- despite being only finitely long. (If it had to contain a term *syntactically identical to* itself, this could not be achieved.)
+
+The key to achieving all this is finding a fixed point for `h`. The strategy we will present will turn out to be a general way of
 finding a fixed point for any lambda term.
 
 
+<a id=deriving-y></a>
 ## Deriving Y, a fixed point combinator ##
 
 How shall we begin?  Well, we need to find an argument to supply to
@@ -303,7 +314,7 @@ work, but examining the way in which it fails will lead to a solution.
 
     h h <~~> \xs. (empty? xs) 0 (succ (h (tail xs)))
 
-The problem is that in the subexpression `h (tail list)`, we've
+The problem is that in the subexpression `h (tail xs)`, we've
 applied `h` to a list, but `h` expects as its first argument the
 length function.
 
@@ -318,7 +329,7 @@ to discuss generalizations of this strategy.)
 
 Shifting to `H` is the key creative step.  Instead of applying `u` to a list, as happened
 when we self-applied `h`, `H` applies its argument `u` first to *itself*: `u u`.
-After `u` gets an argument, the *result* is ready to apply to a list, so we've solved the problem noted above with `h (tail list)`.
+After `u` gets an argument, the *result* is ready to apply to a list, so we've solved the problem noted above with `h (tail xs)`.
 We're not done yet, of course; we don't yet know what argument `u` to give
 to `H` that will behave in the desired way.
 
@@ -533,7 +544,7 @@ to *the tail* of the list we were evaluating its application to at the previous
 
 ## Fixed-point Combinators Are a Bit Intoxicating ##
 
-[[tatto|/images/y-combinator-fixed.jpg]]
+[[tatto|/images/y-combinator-fixed.png]]
 
 There's a tendency for people to say "Y-combinator" to refer to fixed-point combinators generally. We'll probably fall into that usage ourselves. Speaking correctly, though, the Y-combinator is only one of many fixed-point combinators.
 
@@ -553,16 +564,16 @@ then this is a fixed-point combinator:
 For those of you who like to watch ultra slow-mo movies of bullets
 piercing apples, here's a stepwise computation of the application of a
 recursive function.  We'll use a function `sink`, which takes one
-argument.  If the argument is boolean true (i.e., `\x y. x`), it
+argument.  If the argument is boolean true (i.e., `\y n. y`), it
 returns itself (a copy of `sink`); if the argument is boolean false
-(`\x y. y`), it returns `I`.  That is, we want the following behavior:
+(`\y n. n`), it returns `I`.  That is, we want the following behavior:
 
     sink false <~~> I
     sink true false <~~> I
     sink true true false <~~> I
     sink true true true false <~~> I
 
-Evidently, then, `sink true <~~> sink`. So we want `sink` to be the fixed point
+To get this behavior, we want `sink` to be the fixed point
 of `\sink. \b. b sink I`. That is, `sink ≡ Y (\sb.bsI)`:
 
     1. sink false