3 ms·

"if you are allowed to name things at all, getting the function to refer to itself is pretty straightforward" The neat thing about the Y-combinator is that it

"if you are allowed to name things at all, getting the function to refer to itself is pretty straightforward" The neat thing about the Y-combinator is that it allows recursion to be defined in systems, such as the lambda calculus, which don't have naming and therefore a function can't refer to itself by name.

Joker_vD 5y ago
Well, lambda calculus does have names, but yes, I agree, it's a very neat trick in environments where naming is heavily restricted, it gives you "anonymous recursion", so to speak. Church-encoding is another similarly neat trick, for environments with substitutions/applications but without built-in natural numbers. It's just that it seems there are not that many such systems used in practice except for "advanced type systems".
- kragen 5y ago
  The applicative-order Y-combinator that Mike derives at the end, λf.(λx.f λy.x x y)(λx.f λy.x x y), can be straightforwardly compiled into SKI-combinators, which don't have naming at all. I agree that it's rarely justifiable to actually run a translated version of this code, but sometimes it gives you an easy proof of non-termination for some kind of formal system, which often gives you an easy proof of undecidability, which can save you a lot of time trying to figure out how to compute the uncomputable. Or it may persuade you that adding some feature to your design is a bad idea because it eliminates termination guarantees.
  - Joker_vD 5y ago
    If all you need is a proof of non-termination, then encoding a whole of Y combinator is entirely superfluous: "(\f. f f) (\f. f f)" is quite enough already. In case of SKI calculus, that translates to "SII(SII)".
    - kragen 5y ago
      That's true! But it's easy to think that that's something you can fix (no pun intended) because each reduction just takes you back to the same state again, which is easy to recognize as an infinite loop. After all, there are lots of things like finite state machines that can have infinite loops but no decidability difficulties. By contrast, the Y-combinator (together with the rest of the usual suspects) means you can write programs whose termination behavior is undecidable.

Joker_vD 5y ago

Well, lambda calculus does have names, but yes, I agree, it's a very neat trick in environments where naming is heavily restricted, it gives you "anonymous recursion", so to speak. Church-encoding is another similarly neat trick, for environments with substitutions/applications but without built-in natural numbers. It's just that it seems there are not that many such systems used in practice except for "advanced type systems".

kragen 5y ago
The applicative-order Y-combinator that Mike derives at the end, λf.(λx.f λy.x x y)(λx.f λy.x x y), can be straightforwardly compiled into SKI-combinators, which don't have naming at all. I agree that it's rarely justifiable to actually run a translated version of this code, but sometimes it gives you an easy proof of non-termination for some kind of formal system, which often gives you an easy proof of undecidability, which can save you a lot of time trying to figure out how to compute the uncomputable. Or it may persuade you that adding some feature to your design is a bad idea because it eliminates termination guarantees.
- Joker_vD 5y ago
  If all you need is a proof of non-termination, then encoding a whole of Y combinator is entirely superfluous: "(\f. f f) (\f. f f)" is quite enough already. In case of SKI calculus, that translates to "SII(SII)".
  - kragen 5y ago
    That's true! But it's easy to think that that's something you can fix (no pun intended) because each reduction just takes you back to the same state again, which is easy to recognize as an infinite loop. After all, there are lots of things like finite state machines that can have infinite loops but no decidability difficulties. By contrast, the Y-combinator (together with the rest of the usual suspects) means you can write programs whose termination behavior is undecidable.