From: Chris <chris.barker@nyu.edu>
Date: Sun, 22 Feb 2015 14:51:00 +0000 (-0500)
Subject: edits
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=14cda93136c935ddbe8004120e4842b3808c107a;hp=4d2c89f1c1993a93eeac0bf2887ad8cbbd94a937

edits
---

diff --git a/topics/week4_more_about_fixed_point_combinators.mdwn b/topics/week4_more_about_fixed_point_combinators.mdwn
index 78ffc89d..17d8eaba 100644
--- a/topics/week4_more_about_fixed_point_combinators.mdwn
+++ b/topics/week4_more_about_fixed_point_combinators.mdwn
@@ -310,3 +310,62 @@ so `A 4 x` is to `A 3 x` as hyper-exponentiation is to exponentiation...
 *    I hear that `Y` delivers the/a *least* fixed point.  Least
      according to what ordering?  How do you know it's least?
      Is leastness important?
+
+## 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
+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
+
+    X <~~> f 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
+contains at least one redex.  The simplest way to satisfy this
+constraint would be for the fixed point to itself be a redex:
+
+    X == ((\u.M) N) ~~> f 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
+can refine the picture as follows:
+
+    X == ((\u.f(___)) N) ~~> f 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
+"u" in the body of the head abstract:
+
+    X == ((\u.f(__u__)) N) ~~> f X
+
+After reduction of the redex, we're going to have
+
+    X == f(__N__) ~~> f 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:
+
+    X == ((\u.f(__u__)) (\u.f(__u__))) ~~> f 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
+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,
+we simply make a second copy of `u`:
+
+    X == ((\u.f(uu))(\u.f(uu))) ~~> f((\u.f(uu))(\u.f(uu))) == f X
+
+Success.  
+
+So the function `\f.(\u.f(uu))(\u.f(uu))` maps an arbtirary function
+`f` to a fixed point for `f`.