Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Y Combinator

mvanier.livejournal.com

Post reply on HN
Print view View original

21–30 of 39 posts

Re: The Y Combinator

#24

Post by kragen »

Joker_vD wrote: post #17
arethuza wrote: post #14

Earlier quoted context omitted.

"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.

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…

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.

Re: The Y Combinator

#25

Post by kragen »

tromp wrote: post #3

Curiously, the graphical lambda calculus notation for the Y combinator slightly resembles a Y, especially when bent a little as shown at the top of https://tromp.github.io/cl/diagrams.html

This is gorgeous!

Re: The Y Combinator

#26

Post by scapp »

bidirectional wrote: post #19
Joker_vD wrote: post #16

Earlier quoted context omitted.

It's perfectly well typed in System F as "forall a. (a -> a) -> a".

Can you type that in System F? It doesn't seem logically valid, a -> a is trivially true, but apparently implies any a?

System F isn't consistent as a logic (pretty much precisely because it has general recursion). In languages with general recursion, you can do things like

(Haskell)

    anyType :: a
    anyType = anyType
or

(Rust)

    fn any_type() -> T {
        any_type()
    }

Re: The Y Combinator

#28

Post by Joker_vD »

kragen wrote: post #24
Joker_vD wrote: post #17

Earlier quoted context omitted.

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…

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 undecidabilit…

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)".
Post reply on HN