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

31–39 of 39 posts

Re: The Y Combinator

#31

Post by ProfHewitt »

Joker_vD wrote: post #27
ProfHewitt wrote: post #23

Earlier quoted context omitted.

Does the github Java code make use of recursion?

As you can clearly see, it does not. It also doesn't use any forced typecasts to circumvent type checking.

Is FuncToFunc defined recursively in the excerpt below???

      private static interface FuncToTFunc {
          Func apply(FuncToTFunc x);
      }
BTW, what is "x" in the above?

Also is Func defined mutually recursively with FuncToFunc in excerpt below?

      public static  Func Y(final Func> r) {
        return ((FuncToTFunc) f -> f.apply(f))
            .apply(
                f -> r.apply(
                    x -> f.apply(f).apply(x)));
      }

Re: The Y Combinator

#32

Post by amw-zero »

tromp wrote: post #6
eru wrote: post #4

Earlier quoted context omitted.

I always assumed that's where it got the same from?

The name Y combinator is many decades old, while this graphical notation is not even one decade old. But you do raise an interesting question: How did the fixed point combinator come to be known as the Y combinator?

Why was lambda chosen as the abstraction character in the lambda calculus? Mathematicians just pick random letters and symbols for things.

Re: The Y Combinator

#33

Post by cheese_it »

ProfHewitt wrote: post #13

Y Combinator does not work for strongly-typed programs because the definition is not strongly typed. Instead recursion must be added as an additional primitive to the lambda calculus. See https://papers.ssrn.com/abstract=3418003

Interestingly, mutable data is also sufficient to achieve general recursion in a typed language:

  let fact' = ref (fun x -> x) in
  let fact = fun n -> if n = 0 then 1 else n * !fact' (n-1) in
  fact' := fact; fact 3

Re: The Y Combinator

#34

Post by kragen »

Joker_vD wrote: post #28
kragen wrote: post #24

Earlier quoted context omitted.

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

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.

Re: The Y Combinator

#35

Post by yesenadam »

amw-zero wrote: post #32
tromp wrote: post #6

Earlier quoted context omitted.

The name Y combinator is many decades old, while this graphical notation is not even one decade old. But you do raise an interesting question: How did the fixed point combinator come to be known as the Y combinator?

Why was lambda chosen as the abstraction character in the lambda calculus? Mathematicians just pick random letters and symbols for things.

On the origin of the lambda symbol: https://en.wikipedia.org/wiki/Lambda_calculus#Origin_of_the_...

Re: The Y Combinator

#36

Post by gsg »

scapp wrote: post #26
bidirectional wrote: post #19

Earlier quoted context omitted.

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() }

System F doesn't have general recursion.

Extensions with a letrec-like construct are common, and are sometimes inaccurately called 'System F', but those languages do not have the properties of System F.

Re: The Y Combinator

#37

Post by scapp »

gsg wrote: post #36
scapp wrote: post #26

Earlier quoted context omitted.

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() }

System F doesn't have general recursion. Extensions with a letrec-like construct are common, and are sometimes inaccurately called 'System F', but those languages do not have the properties of System F.

You're right. I must have been thinking of one of those extensions you're talking about (F# maybe?). I should have remembered that System F is part of the lambda cube, so it's at least as consistent as CoC

Re: The Y Combinator

#38

Post by ProfHewitt »

Joker_vD wrote: post #27
ProfHewitt wrote: post #23

Earlier quoted context omitted.

Does the github Java code make use of recursion?

As you can clearly see, it does not. It also doesn't use any forced typecasts to circumvent type checking.

Joker_vD: Looks like you are incorrect because Func and

FuncToFunc are defined recursively.

Re: The Y Combinator

#39

Post by Joker_vD »

ProfHewitt wrote: post #38
Joker_vD wrote: post #27

Earlier quoted context omitted.

As you can clearly see, it does not. It also doesn't use any forced typecasts to circumvent type checking.

Joker_vD: Looks like you are incorrect because Func and FuncToFunc are defined recursively.

No, they are not. Do you know what "interface" is in Java, and what is "class"? And what is "method"?

Interface Func doesn't refer to FuncToFunc in its declaration, and interface FuncToFunc doesn't refer to Func. The method Y does refer to those two interfaces, but it's declared later than those are, and they don't (and can't, acvtually) refer to it.

Post reply on HN