3 ms·

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 recu

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.

3 ms·

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 recu

by Joker_vD 5y ago

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.