X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek4_more_about_fixed_point_combinators.mdwn;h=11754dde61bc6bee63675eba2ed12e2ce51f0345;hp=78ffc89d3f124d48a00bf9b66a5555224f84c77b;hb=a95160473037089ea4deb34eceff948391b0cee4;hpb=6694165ac4d6edab602b3ad3651d0a5931b36a0e diff --git a/topics/week4_more_about_fixed_point_combinators.mdwn b/topics/week4_more_about_fixed_point_combinators.mdwn index 78ffc89d..11754dde 100644 --- a/topics/week4_more_about_fixed_point_combinators.mdwn +++ b/topics/week4_more_about_fixed_point_combinators.mdwn @@ -310,3 +310,63 @@ 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 `h`, we want to find a fixed point `X` such that: + + X <~~> h 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 +constraint would be for the fixed point to itself be a redex (again, just a guess): + + 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 `h X`, since that is what the reduction arrow tells us. So we +can refine the picture as follows: + + X â¡ ((\u. h (___)) N) ~~> h 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. h (__u__)) N) ~~> h X + +After reduction of the redex, we're going to have + + 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 +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. 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 +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`: + + X â¡ ((\u. h (u u)) (\u. h (u u))) + ~~> h ((\u. h (u u)) (\u. h (u u))) + â¡ h X + +Success. + +So the function `\h. (\u. h (u u)) (\u. h (u u))` maps an arbitrary term +`h` to a fixed point for `h`.