but as you can see, we'd still have to plug the formula back into itself again, and again, and again... No dice.
+[At this point, some of you will recall the discussion in the first
+class concerning the conception of functions as sets of ordered pairs.
+The problem, as you will recall, was that in the untyped lambda
+calculus, we wanted a function to be capable of taking itself as an
+argument. For instance, we wanted to be able to apply the identity
+function to itself. And since the identity function always returns
+its argument unchanged, the value it should return in that case is
+itself:
+
+ (\x.x)(\x.x) ~~> (\x.x)
+
+If we conceive of a function as a set of ordered pairs, we would start
+off like this:
+
+ 1 -> 1
+ 2 -> 2
+ 3 -> 3
+ ...
+ [1 -> 1, 2 -> 2, 3 -> 3, ..., [1 -> 1, 2 -> 2, 3 -> 3, ...,
+
+Eventually, we would get to the point where we want to say what the
+identity function itself gets mapped to. But in order to say that, we
+need to write down the identity function in the argument position as a
+set of ordered pairs. The need to insert a copy of the entire
+function definition inside of a copy of the entire function definition
+inside of... is the same problem as the need to insert a complete
+graph of the identity function inside of the graph for the identity function.]
+
So how could we do it? And how do OCaml and Scheme manage to do it, with their `let rec` and `letrec`?
1. OCaml and Scheme do it using a trick. Well, not a trick. Actually an impressive, conceptually deep technique, which we haven't yet developed. Since we want to build up all the techniques we're using by hand, then, we shouldn't permit ourselves to rely on `let rec` or `letrec` until we thoroughly understand what's going on under the hood.
##However...##
-Some computable functions are just not definable in this way. The simplest function that *simply cannot* be defined using the resources we've so far developed is the [[!wikipedia Ackermann function]]:
+Some computable functions are just not definable in this way. We can't, for example, define a function that tells us, for whatever function `f` we supply it, what is the smallest integer `x` where `f x` is `true`.
+
+Neither do the resources we've so far developed suffice to define the
+[[!wikipedia Ackermann function]]:
A(m,n) =
| when m == 0 -> n + 1
What is a fixed point of the identity combinator I?
+What is a fixed point of the false combinator, KI?
+
It's a theorem of the lambda calculus that every formula has a fixed point. In fact, it will have infinitely many, non-equivalent fixed points. And we don't just know that they exist: for any given formula, we can name many of them.
Yes, even the formula that you're using the define the successor function will have a fixed point. Isn't that weird? Think about how it might be true.
##Okay, then give me a fixed-point combinator, already!##
-Many fixed-point combinators have been discovered. (And given a fixed-point combinator, there are ways to use it as a model to build infinitely many more, non-equivalent fixed-point combinators.)
+Many fixed-point combinators have been discovered. (And some fixed-point combinators give us models for building infinitely many more, non-equivalent fixed-point combinators.)
Two of the simplest:
<pre><code>Θ′ ≡ (\u f. f (\n. u u f n)) (\u f. f (\n. u u f n))
Y′ ≡ \f. (\u. f (\n. u u n)) (\u. f (\n. u u n))</code></pre>
-Θ′ has the advantage that <code>f (Θ′ f)</code> really *reduces to* <code>Θ′ f</code>.
-
-<code>f (Y′ f)</code> is only convertible with <code>Y′ f</code>; that is, there's a common formula they both reduce to. For most purposes, though, either will do.
+<code>Θ′</code> has the advantage that <code>f (Θ′ f)</code> really *reduces to* <code>Θ′ f</code>. Whereas <code>f (Y′ f)</code> is only *convertible with* <code>Y′ f</code>; that is, there's a common formula they both reduce to. For most purposes, though, either will do.
You may notice that both of these formulas have eta-redexes inside them: why can't we simplify the two `\n. u u f n` inside <code>Θ′</code> to just `u u f`? And similarly for <code>Y′</code>?
L L L L L L L L L L L L L L L L L L L L L L L L L L
+##Watching Y in action##
+
+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
+returns itself (a copy of `sink`); if the argument is boolean false,
+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
+
+So we make sink = Y (\fb.bfI):
+
+ 1. sink false
+ 2. Y (\fb.bfI) false
+ 3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) false
+ 4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) false
+ 5. [\fb.bfI] ((\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))) false
+ 6. (\b.b[(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))]I) false
+ 7. false [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] I
+ --------------------------------------------
+ 8. I
+
+So far so good. The crucial thing to note is that as long as we
+always reduce the outermost redex first, we never have to get around
+to computing the underlined redex: because `false` ignores its first
+argument, we can throw it away unreduced.
+
+Now we try the next most complex example:
+
+ 1. sink true false
+ 2. Y (\fb.bfI) true false
+ 3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) true false
+ 4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) true false
+ 5. [\fb.bfI] ((\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))) true false
+ 6. (\b.b[(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))]I) true false
+ 7. true [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] I false
+ 8. [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] false
+
+We've now arrived at line (4) of the first computation, so the result
+is again I.
+
+You should be able to see that `sink` will consume as many `true`s as
+we throw at it, then turn into the identity function after it
+encounters the first `false`.
+
+The key to the recursion is that, thanks to Y, the definition of
+`sink` contains within it the ability to fully regenerate itself as
+many times as is necessary. The key to *ending* the recursion is that
+the behavior of `sink` is sensitive to the nature of the input: if the
+input is the magic function `false`, the self-regeneration machinery
+will be discarded, and the recursion will stop.
+