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>
+ Θ′ ≡ (\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>Θ′</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.
+`Θ′` 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>Θ′</code> to just `u u f`? And similarly for <code>Y′</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:
-<pre><code>Θ ≡ (\u f. f (u u f)) (\u f. f (u u f))
-Y ≡ \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>Θ (\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>Ψ</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>Ψ (\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:
However, when we evaluate the application of our:
-<pre><code>Ψ (\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:
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>Ψ</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:
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
-</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
-it occurs is <code>Ω</code>, our prototypical infinite loop...
+it occurs is `Ω`, our prototypical infinite loop...
What about the liar paradox?
You should be cautious about feeling too comfortable with
these results. Thinking again of the truth-teller paradox, yes,
-<code>Ω</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).