Θ′ ≡ (\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))
+ +Θ′ 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 Θ′ to just `u u f`? 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))
+ +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: + +
Ψ (\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 + +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 ~~> + ... + +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))) ))