index a1e79f5..4772842 100644 (file)
@@ -126,7 +126,10 @@ With sufficient ingenuity, a great many functions can be defined in the same way

##However...##

##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

A(m,n) =
| when m == 0 -> n + 1
@@ -333,16 +336,14 @@ Isn't that cool?

##Okay, then give me a fixed-point combinator, already!##

##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>&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>

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>

-<code>&Theta;&prime;</code> 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.
+<code>&Theta;&prime;</code> has the advantage that <code>f (&Theta;&prime; f)</code> really *reduces to* <code>&Theta;&prime; f</code>. Whereas <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>?

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>?