##How to do recursion with lower-case omega##
-[TODO]
+Recall our initial, abortive attempt above to define the `get_length` function in the lambda calculus. We said "What we really want to do is something like this:
+
+ \lst. (isempty lst) zero (add one (... (extract-tail lst)))
+
+where this very same formula occupies the `...` position."
+
+We are not going to exactly that, at least not yet. But we are going to do something close to it.
+
+Consider a formula of the following form (don't worry yet about exactly how we'll fill the `...`s):
+
+ \h \lst. (isempty lst) zero (add one (... (extract-tail lst)))
+
+Call that formula `H`. Now what would happen if we applied `H` to itself? Then we'd get back:
+
+ \lst. (isempty lst) zero (add one (... (extract-tail lst)))
+
+where any occurrences of `h` inside the `...` were substituted with `H`. Call this `F`. `F` looks pretty close to what we're after: a function that takes a list and returns zero if it's empty, and so on. And `F` is the result of applying `H` to itself. But now inside `F`, the occurrences of `h` are substituted with the very formula `H` we started with.So if we want to get `F` again, all we have to do is apply `h` to itself---since as we said, the self-application of `H` is how we created `F` in the first place.
+
+So, the way `F` should be completed is:
+
+ \lst. (isempty lst) zero (add one ((h h) (extract-tail lst)))
+
+and our original `H` is:
+
+ \h \lst. (isempty lst) zero (add one ((h h) (extract-tail lst)))
+
+The self-application of `H` will give us `F` with `H` substituted in for its free variable `h`.
+
+Instead of writing out a long formula twice, we could write:
+
+ (\x. x x) LONG-FORMULA
+
+and the initial `(\x. x x)` is just what we earlier called the <code>ω</code> combinator (lower-case omega, not the non-termination <code>Ω</code>). So the self-application of `H` can be written:
+
+<pre><code>ω (\h \lst. (isempty lst) zero (add one ((h h) (extract-tail lst))))</code></pre>
+
+and this will indeed implement the recursive function we couldn't earlier figure out how to define.
+
+In broad brush-strokes, `H` is half of the `get_length` function we're seeking, and H has the form:
+
+ \h other-arguments. ... (h h) ...
+
+We get the whole `get_length` function by applying `H` to itself. Then `h` is replaced by the half `H`, and when we later apply `h` to itself, we re-create the whole `get_length` again.
+
+Now suppose you wanted to wrap this up in a pretty interface, so that the programmer didn't need to write `(h h)` but could just write `g` for some function `g`. How could you do it?
+
+Now the `F`-like expression we'd be aiming for---call it `F*`---would look like this:
+
+ \lst. (isempty lst) zero (add one (g (extract-tail lst)))
+
+or, abbreviating:
+
+ \lst. ...g...
+
+Here we have just a single `g` instead of `(h h)`. We'd want `F*` to be the result of self-applying some `H*`, and then binding to `g` that very self-application of `H*`. We'd get this if `H*` had the form:
+
+ \h. (\g lst. ...g...) (h h)
+
+The self-application of `H*` would be:
+
+ (\h. (\g lst. ...g...) (h h)) (\h. (\g lst. ...g...) (h h))
+
+or:
+
+ (\f. (\h. f (h h)) (\h. f (h h))) (\g lst. ...g...)
+
+The left-hand side of this is known as **the Y-combinator** and so this could be written more compactly as:
+
+ Y (\g lst. ...g...)
+
+or, replacing the abbreviated bits:
+
+ Y (\g lst. (isempty lst) zero (add one (g (extract-tail lst))))
+
+So this is another way to implement the recursive function we couldn't earlier figure out how to define.
+
##Generalizing##
-In general, a **fixed point** of a function f is a value *x* such that f<em>x</em> is equivalent to *x*. For example, what is a fixed point of the function from natural numbers to their squares? What is a fixed point of the successor function?
+Let's step back and fill in some theory to help us understand why these tricks work.
+
+In general, we call a **fixed point** of a function f any value *x* such that f <em>x</em> is equivalent to *x*. For example, what is a fixed point of the function from natural numbers to their squares? What is a fixed point of the successor function?
In the lambda calculus, we say a fixed point of an expression `f` is any formula `X` such that:
OK, so how do we make use of this?
-Recall our initial, abortive attempt above to define the `get_length` function in the lambda calculus. We said "What we really want to do is something like this:
+Recall again our initial, abortive attempt above to define the `get_length` function in the lambda calculus. We said "What we really want to do is something like this:
\lst. (isempty lst) zero (add one (... (extract-tail lst)))
where this very same formula occupies the `...` position."
-Now, what if we *were* somehow able to get ahold of this formula, as an additional argument? We could take that argument and plug it into the `...` position. Something like this:
+If we could somehow get ahold of this formula, as an additional argument, then we could take the argument and plug it into the `...` position. Something like this:
\self (\lst. (isempty lst) zero (add one (self (extract-tail lst))) )