index 26760eb..c9e2675 100644 (file)
@@ -146,7 +146,7 @@ But functions like the Ackermann function require us to develop a more general t

##How to do recursion with lower-case omega##

-...
+[TODO]

##Generalizing##

@@ -261,7 +261,9 @@ Two of the simplest:
<pre><code>&Theta;&prime; &equiv; (\u f. f (\n. u u f n)) (\u f. f (\n. u u f n))
Y&prime; &equiv; \f. (\u. f (\n. u u n)) (\u. f (\n. u u n))</code></pre>

-&Theta;&prime; has the advantage that <code>f (&Theta;&prime; f)</code> really *reduces to* <code>&Theta;&prime; f</code>. <code>f (Y&prime; f)</code> is only convertible with <code>Y&prime; f</code>; that is, there's a common formula they both reduce to. For most purposes, though, either will do.
+&Theta;&prime; has the advantage that <code>f (&Theta;&prime; f)</code> really *reduces to* <code>&Theta;&prime; f</code>.
+
+<code>f (Y&prime; f)</code> is only convertible with <code>Y&prime; 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>&Theta;&prime;</code> to just `u u f`? And similarly for <code>Y&prime;</code>?