clean up last Q&A

diff --git a/topics/week4_more_about_fixed_point_combinators.mdwn b/topics/week4_more_about_fixed_point_combinators.mdwn
index 51d8b88..11754dd 100644 (file)
--- a/topics/week4_more_about_fixed_point_combinators.mdwn
+++ b/topics/week4_more_about_fixed_point_combinators.mdwn
@@ -313,58 +313,60 @@ so `A 4 x` is to `A 3 x` as hyper-exponentiation is to exponentiation...
 
 ## Q: I still don't fully understand the Y combinator.  Can you explain it in a different way?
 
 
 ## Q: I still don't fully understand the Y combinator.  Can you explain it in a different way?
 

-Sure!  Here is another way to derive Y.  We'll start by choosing a
+Sure!  Here is another way to derive `Y`.  We'll start by choosing a

 specific goal, and at each decision point, we'll make a reasonable
 guess.  The guesses will all turn out to be lucky, and we'll arrive at
 a fixed point combinator.
 
 specific goal, and at each decision point, we'll make a reasonable
 guess.  The guesses will all turn out to be lucky, and we'll arrive at
 a fixed point combinator.
 

-Given an arbitrary term f, we want to find a fixed point X such that
+Given an arbitrary term `h`, we want to find a fixed point `X` such that:

 
 

-    X <~~> f X
+    X <~~> h X

 
 

-Our strategy will be to seek an X such that X ~~> f X. Because X and
-f X are not the same, the only way that X can reduce to f X is if X
+Our strategy will be to seek an `X` such that `X ~~> h X` (this is just a guess). Because `X` and
+`h X` are syntactically different, the only way that `X` can reduce to `h X` is if `X`

 contains at least one redex.  The simplest way to satisfy this
 contains at least one redex.  The simplest way to satisfy this

-constraint would be for the fixed point to itself be a redex:
+constraint would be for the fixed point to itself be a redex (again, just a guess):

 
 

-    X == ((\u.M) N) ~~> f X
+    X ≡ ((\u. M) N) ~~> h X

 
 

-The result of beta reduction on this redex will be M with some
-substitutions.  We know that after these substitutions, M will have
-the form `f X`, since that is what the reduction arrow tells us. So we
+The result of beta reduction on this redex will be `M` with some
+substitutions.  We know that after these substitutions, `M` will have
+the form `h X`, since that is what the reduction arrow tells us. So we

 can refine the picture as follows:
 
 can refine the picture as follows:
 

-    X == ((\u.f(___)) N) ~~> f X
+    X ≡ ((\u. h (___)) N) ~~> h X

 
 

-Here, the ___ has to be something that reduces to the fixed point X.
+Here, the `___` has to be something that reduces to the fixed point `X`.

 It's natural to assume that there will be at least one occurrence of
 It's natural to assume that there will be at least one occurrence of

-"u" in the body of the head abstract:
+`u` in the body of the head abstract:

 
 

-    X == ((\u.f(__u__)) N) ~~> f X
+    X ≡ ((\u. h (__u__)) N) ~~> h X

 
 After reduction of the redex, we're going to have
 
 
 After reduction of the redex, we're going to have
 

-    X == f(__N__) ~~> f X
+    X ≡ h (__N__) ~~> h X

 
 

-Apparently, `__N__` will have to reduce to X.  Therefore we should
-choose a skeleton for N that is consistent with what we have decided
-so far about the internal structure of X.  We might like for N to
-match X in its entirety, but this would require N to contain itself as
-a subpart.  So we'll settle for the more modest assumption that N
-matches the head of X:
+Apparently, `__N__` will have to reduce to `X`.  Therefore we should
+choose a skeleton for `N` that is consistent with what we have decided
+so far about the internal structure of `X`.  We might like for `N` to
+syntactically match the whole of `X`, but this would require `N` to contain itself as
+a subpart.  So we'll settle for the more modest assumption (or guess) that `N`
+matches the head of `X`:

 
 

-    X == ((\u.f(__u__)) (\u.f(__u__))) ~~> f X
+    X ≡ ((\u. h (__u__)) (\u. h (__u__))) ~~> h X

 
 At this point, we've derived a skeleton for X on which it contains two
 so-far identical halves.  We'll guess that the halves will be exactly
 identical.  Note that at the point at which we perform the first
 
 At this point, we've derived a skeleton for X on which it contains two
 so-far identical halves.  We'll guess that the halves will be exactly
 identical.  Note that at the point at which we perform the first

-reduction, `u` will get bound N, which now corresponds to a term
-representing one of the halves of X.  So in order to produce a full X,
+reduction, `u` will get bound to `N`, which now corresponds to a term
+representing one of the halves of `X`.  So in order to produce a full `X`,

 we simply make a second copy of `u`:
 
 we simply make a second copy of `u`:
 

-    X == ((\u.f(uu))(\u.f(uu))) ~~> f((\u.f(uu))(\u.f(uu))) == f X
+    X ≡ ((\u. h (u u)) (\u. h (u u)))
+    ~~>       h ((\u. h (u u)) (\u. h (u u)))
+      ≡       h X

 
 Success.  
 
 
 Success.  
 

-So the function `\f.(\u.f(uu))(\u.f(uu))` maps an arbtirary function
-`f` to a fixed point for `f`.
+So the function `\h. (\u. h (u u)) (\u. h (u u))` maps an arbitrary term
+`h` to a fixed point for `h`.