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
| else -> A(m-1, A(m,n-1))
A(0,y) = y+1
- A(1,y) = y+2
- A(2,y) = 2y + 3
+ A(1,y) = 2+(y+3) - 3
+ A(2,y) = 2(y+3) - 3
A(3,y) = 2^(y+3) - 3
A(4,y) = 2^(2^(2^...2)) [where there are y+3 2s] - 3
...
##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>?