Θ′ ≡ (\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))
+ Îâ² â¡ (\u h. h (\n. u u h n)) (\u h. h (\n. u u h n)) + Yâ² â¡ \h. (\u. h (\n. u u n)) (\u. h (\n. u u n)) -Θ′ 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. +Applying either of these to a term `h` gives a fixed point `Î¾` for `h`, meaning that `h Î¾` <~~> `Î¾`. `Îâ²` has the advantage that `h (Îâ² h)` really *reduces to* `Îâ² h`. Whereas `h (Yâ² h)` is only *convertible with* `Yâ² h`; 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 Θ′ to just `u u f`? And similarly for Y′? +You may notice that both of these formulas have eta-redexes inside them: why can't we simplify the two `\n. u u h n` inside `Îâ²` to just `u u h`? And similarly for `Yâ²`? Indeed you can, getting the simpler: -
Θ ≡ (\u f. f (u u f)) (\u f. f (u u f))
-Y ≡ \f. (\u. f (u u)) (\u. f (u u))
+ Î â¡ (\u h. h (u u h)) (\u h. h (u u h)) + Y â¡ \h. (\u. h (u u)) (\u. h (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 Θ (\self. BODY) 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 Ψ 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: -
Ψ (\self. \n. self n)
+ Î¨ (\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: - (\n. self n) M + (\n. self n) M where `self` is equivalent to the very formula `\n. self n` that contains it. So the evaluation will proceed: - (\n. self n) M ~~> - self M ~~> - (\n. self n) M ~~> - self M ~~> - ... + (\n. self n) M ~~> + self M <~~> + (\n. self n) M ~~> + self M <~~> + ... You've written an infinite loop! However, when we evaluate the application of our: -
Ψ (\self (\lst. (isempty lst) zero (add one (self (extract-tail lst))) ))
+ Î¨ (\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, 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: - \lst. (isempty lst) zero (add one (self (extract-tail lst))) + \xs. (empty? xs) 0 (succ (self (tail xs))) -to *the tail* of the list we were evaluating its application to at the previous stage. Assuming our lists are finite (and the implementations we're using don't permit otherwise), at some point one will get a list whose tail is empty, and then the evaluation of that formula to that tail will return `zero`. So the recursion eventually bottoms out in a base value. +to *the tail* of the list we were evaluating its application to at the previous stage. Assuming our lists are finite (and the encodings we've been using so far don't permit otherwise), at some point one will get a list whose tail is empty, and then the evaluation of that formula to that tail will return `0`. So the recursion eventually bottoms out in a base value. ##Fixed-point Combinators Are a Bit Intoxicating## -![tatoo](/y-combinator-fixed.jpg) +[[tatto|/images/y-combinator-fixed.jpg]] 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 Ψ 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. +We used `Î¨` above to stand in for an arbitrary fixed-point combinator. We 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: - \a b c d e f g h i j k l m n o p q s t u v w x y z r. (r (t h i s i s a f i x e d p o i n t c o m b i n a t o r)) + \a b c d e f g h i j k l m n o p q s t u v w x y z r. (r (t h i s i s a f i x e d p o i n t c o m b i n a t o r)) then this is a fixed-point combinator: - L L L L L L L L L L L L L L L L L L L L L L L L L L + L L L L L L L L L L L L L L L L L L L L L L L L L L ##Watching Y in action## @@ -577,15 +543,15 @@ returns itself (a copy of `sink`); if the argument is boolean false sink true true false ~~> I sink true true true false ~~> I -So we make `sink = Y (\f b. b f I)`: +So we make `sink = Y (\s b. b s I)`: 1. sink false - 2. Y (\fb.bfI) false - 3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) false - 4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) false - 5. [\fb.bfI] ((\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))) false - 6. (\b.b[(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))]I) false - 7. false [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] I + 2. Y (\sb.bsI) false + 3. (\h. (\u. h [u u]) (\u. h (u u))) (\sb.bsI) false + 4. (\u. (\sb.bsI) [u u]) (\u. (\sb.bsI) (u u)) false + 5. (\sb.bsI) [(\u. (\sb.bsI) (u u)) (\u. (\sb.bsI) (u u))] false + 6. (\b. b [(\u. (\sb.bsI) (u u))(\u. (\sb.bsI) (u u))] I) false + 7. false [(\u. (\sb.bsI) (u u))(\u. (\sb.bsI) (u u))] I -------------------------------------------- 8. I @@ -597,22 +563,22 @@ argument, we can throw it away unreduced. Now we try the next most complex example: 1. sink true false - 2. Y (\fb.bfI) true false - 3. (\f. (\h. f (h h)) (\h. f (h h))) (\fb.bfI) true false - 4. (\h. [\fb.bfI] (h h)) (\h. [\fb.bfI] (h h)) true false - 5. [\fb.bfI] ((\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))) true false - 6. (\b.b[(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))]I) true false - 7. true [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] I false - 8. [(\h. [\fb.bsI] (h h))(\h. [\fb.bsI] (h h))] false + 2. Y (\sb.bsI) true false + 3. (\h. (\u. h [u u]) (\u. h (u u))) (\sb.bsI) true false + 4. (\u. (\sb.bsI) [u u]) (\u. (\sb.bsI) (u u)) true false + 5. (\sb.bsI) [(\u. (\sb.bsI) (u u)) (\u. (\sb.bsI) (u u))] true false + 6. (\b.b [(\u. (\sb.bsI) (u u)) (\u. (\sb.bsI) (u u))] I) true false + 7. true [(\u. (\sb.bsI) (u u)) (\u. (\sb.bsI) (u u))] I false + 8. [(\u. (\sb.bsI) (u u)) (\u. (\sb.bsI) (u u))] false We've now arrived at line (4) of the first computation, so the result -is again I. +is again `I`. You should be able to see that `sink` will consume as many `true`s as we throw at it, then turn into the identity function after it encounters the first `false`. -The key to the recursion is that, thanks to Y, the definition of +The key to the recursion is that, thanks to `Y`, the definition of `sink` contains within it the ability to fully regenerate itself as many times as is necessary. The key to *ending* the recursion is that the behavior of `sink` is sensitive to the nature of the input: if the @@ -637,18 +603,17 @@ factorial of `n-1`. But if we leave out the base case, we get 3! = 3 * 2! = 3 * 2 * 1! = 3 * 2 * 1 * 0! = 3 * 2 * 1 * 0 * -1! ... -That's why it's crucial to declare that 0! = 1, in which case the +That's why it's crucial to declare that `0!` = `1`, in which case the recursive rule does not apply. In our terms, - fac = Y (\fac n. iszero n 1 (fac (predecessor n))) + fact â¡ Y (\fact n. zero? n 1 (fact (predecessor n))) -If `n` is 0, `fac` reduces to 1, without computing the recursive case. +If `n` is `0`, `fact` reduces to `1`, without computing the recursive case. -Curry originally called `Y` the paradoxical combinator, and discussed +Curry originally called `Y` the "paradoxical" combinator, and discussed it in connection with certain well-known paradoxes from the philosophy -literature. The truth teller paradox has the flavor of a recursive -function without a base case: the truth-teller paradox (and related -paradoxes). +literature. The truth-teller paradox has the flavor of a recursive +function without a base case: (1) This sentence is true. @@ -664,6 +629,8 @@ assume that sentences can have for their meaning boolean functions like the ones we have been working with here. Then the sentence *John is John* might denote the function `\x y. x`, our `true`. + + Then (1) denotes a function from whatever the referent of *this sentence* is to a boolean. So (1) denotes `\f. f true false`, where the argument `f` is the referent of *this sentence*. Of course, if @@ -682,33 +649,32 @@ sentence in which it occurs, the sentence denotes a fixed point for the identity function. Here's a fixed point for the identity function: -
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
-
+ Y I â¡ + (\h. (\u. h (u u)) (\u. h (u u))) I ~~> + (\u. I (u u)) (\u. I (u u))) ~~> + (\u. (u u)) (\u. (u u))) â¡ + Ï Ï + Î© 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 Ω, our prototypical infinite loop... +it occurs is `Î©`, our prototypical infinite loop... What about the liar paradox? (2) This sentence is false. Used in a context in which *this sentence* refers to the utterance of -(2) in which it occurs, (2) will denote a fixed point for `\f.neg f`, +(2) in which it occurs, (2) will denote a fixed point for `\f. neg f`, or `\f l r. f r l`, which is the `C` combinator. So in such a context, (2) might denote Y C - (\f. (\h. f (h h)) (\h. f (h h))) I - (\h. C (h h)) (\h. C (h h))) - C ((\h. C (h h)) (\h. C (h h))) - C (C ((\h. C (h h))(\h. C (h h)))) - C (C (C ((\h. C (h h))(\h. C (h h))))) + (\h. (\u. h (u u)) (\u. h (u u))) C + (\u. C (u u)) (\u. C (u u))) + C ((\u. C (u u)) (\u. C (u u))) + C (C ((\u. C (u u)) (\u. C (u u)))) + C (C (C ((\u. C (u u)) (\u. C (u u))))) ... And infinite sequence of `C`s, each one negating the remainder of the @@ -724,23 +690,23 @@ rather than recursive functions. You should be cautious about feeling too comfortable with these results. Thinking again of the truth-teller paradox, yes, -Ω 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). +`Î©` is *a* fixed point for `I`, and perhaps it has +some 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, versus other fixed point combinators). But one could ask: look, literally every formula is a fixed point for `I`, since X <~~> I X -for any choice of X whatsoever. +for any choice of `X` whatsoever. -So the Y combinator is only guaranteed to give us one fixed point out -of infinitely many---and not always the intuitively most useful -one. (For instance, the squaring function has zero as a fixed point, -since 0 * 0 = 0, and 1 as a fixed point, since 1 * 1 = 1, but `Y -(\x. mul x x)` doesn't give us 0 or 1.) So with respect to the +So the `Y` combinator is only guaranteed to give us one fixed point out +of infinitely many --- and not always the intuitively most useful +one. (For instance, the squaring function `\x. mul x x` has `0` as a fixed point, +since `0 * 0 = 0`, and `1` as a fixed point, since `1 * 1 = 1`, but `Y +(\x. mul x x)` doesn't give us `0` or `1`.) So with respect to the truth-teller paradox, why in the reasoning we've just gone through should we be reaching for just this fixed point at just this juncture?