author jim Thu, 19 Feb 2015 15:24:56 +0000 (10:24 -0500) committer Linux User Thu, 19 Feb 2015 15:24:56 +0000 (10:24 -0500)

index 4f2691e..14bba4c 100644 (file)
@@ -457,23 +457,23 @@ more, non-equivalent fixed-point combinators.)

Two of the simplest:

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>
+    Θ′ ≡ (\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>&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.
+`Θ′` has the advantage that `f (Θ′ f)` really *reduces to* `Θ′ f`. Whereas `f (Y′ f)` is only *convertible with* `Y′ f`; 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 `Θ′` to just `u u f`? And similarly for `Y′`?

Indeed you can, getting the simpler:

Indeed you can, getting the simpler:

-<pre><code>&Theta; &equiv; (\u f. f (u u f)) (\u f. f (u u f))
-Y &equiv; \f. (\u. f (u u)) (\u. f (u u))</code></pre>
+    Θ ≡ (\u f. f (u u f)) (\u f. f (u u f))
+    Y ≡ \f. (\u. f (u u)) (\u. f (u u))

-I stated the more complex formulas for the following reason: in a language whose evaluation order is *call-by-value*, the evaluation of <code>&Theta; (\self. BODY)</code> and `Y (\self. BODY)` will in general not terminate. But evaluation of the eta-unreduced primed versions will.
+I stated the more complex formulas for the following reason: in a language whose evaluation order is *call-by-value*, the evaluation of `Θ (\self. BODY)` and `Y (\self. BODY)` will in general not terminate. But evaluation of the eta-unreduced primed versions will.

-Of course, if you define your `\self. BODY` stupidly, your formula will never terminate. For example, it doesn't matter what fixed point combinator you use for <code>&Psi;</code> in:
+Of course, if you define your `\self. BODY` stupidly, your formula will never terminate. For example, it doesn't matter what fixed point combinator you use for `Ψ` in:

-<pre><code>&Psi; (\self. \n. self n)</code></pre>
+    Ψ (\self. \n. self n)

When you try to evaluate the application of that to some argument `M`, it's going to try to give you back:

When you try to evaluate the application of that to some argument `M`, it's going to try to give you back:

@@ -491,7 +491,7 @@ You've written an infinite loop!

However, when we evaluate the application of our:

However, when we evaluate the application of our:

-<pre><code>&Psi; (\self (\xs. (empty? xs) 0 (succ (self (tail xs))) ))</code></pre>
+    Ψ (\self (\xs. (empty? xs) 0 (succ (self (tail xs))) ))

to some list `L`, we're not going to go into an infinite evaluation loop of that sort. At each cycle, we're going to be evaluating the application of:

to some list `L`, we're not going to go into an infinite evaluation loop of that sort. At each cycle, we're going to be evaluating the application of:

@@ -505,7 +505,7 @@ to *the tail* of the list we were evaluating its application to at the previous

There's a tendency for people to say "Y-combinator" to refer to fixed-point combinators generally. We'll probably fall into that usage ourselves. Speaking correctly, though, the Y-combinator is only one of many fixed-point combinators.

There's a tendency for people to say "Y-combinator" to refer to fixed-point combinators generally. We'll probably fall into that usage ourselves. Speaking correctly, though, the Y-combinator is only one of many fixed-point combinators.

-I used <code>&Psi;</code> above to stand in for an arbitrary fixed-point combinator. I don't know of any broad conventions for this. But this seems a useful one.
+I used `Ψ` above to stand in for an arbitrary fixed-point combinator. I don't know of any broad conventions for this. But this seems a useful one.

As we said, there are many other fixed-point combinators as well. For example, Jan Willem Klop pointed out that if we define `L` to be:

As we said, there are many other fixed-point combinators as well. For example, Jan Willem Klop pointed out that if we define `L` to be:

@@ -635,17 +635,16 @@ sentence in which it occurs, the sentence denotes a fixed point for
the identity function.  Here's a fixed point for the identity
function:

the identity function.  Here's a fixed point for the identity
function:

-<pre><code>Y I
-(\f. (\h. f (h h)) (\h. f (h h))) I
-(\h. I (h h)) (\h. I (h h)))
-(\h. (h h)) (\h. (h h)))
-&omega; &omega;
-&Omega
-</code></pre>
+    Y I
+    (\f. (\h. f (h h)) (\h. f (h h))) I
+    (\h. I (h h)) (\h. I (h h)))
+    (\h. (h h)) (\h. (h h)))
+    ω ω
+    Ω

Oh.  Well!  That feels right.  The meaning of *This sentence is true*
in a context in which *this sentence* refers to the sentence in which

Oh.  Well!  That feels right.  The meaning of *This sentence is true*
in a context in which *this sentence* refers to the sentence in which
-it occurs is <code>&Omega;</code>, our prototypical infinite loop...
+it occurs is `Ω`, our prototypical infinite loop...

@@ -677,7 +676,7 @@ rather than recursive functions.

You should be cautious about feeling too comfortable with
these results.  Thinking again of the truth-teller paradox, yes,

You should be cautious about feeling too comfortable with
these results.  Thinking again of the truth-teller paradox, yes,
-<code>&Omega;</code> is *a* fixed point for `I`, and perhaps it has
+`Ω` is *a* fixed point for `I`, and perhaps it has
some a privileged status among all the fixed points for `I`, being the
one delivered by Y and all (though it is not obvious why Y should have
any special status).
some a privileged status among all the fixed points for `I`, being the
one delivered by Y and all (though it is not obvious why Y should have
any special status).