5 ms·

The Y combinator is not the same as λ calculus. The Y combinator is an expression in λ calculus.

lmm 3y ago
The Y combinator is in a sense the heart of the λ calculus; it's a key discovery for understanding that the λ calculus is universal, which is what makes it a useful concept rather than an arbitrary bundle of rules.
- andsoitis 3y ago
  > heart of the λ calculus The Y combinator is a specific fixed-point combinator in lambda calculus. It is used to express recursion in lambda calculus where direct recursion is not initially available due to the lack of named functions. The Y combinator demonstrates the power of lambda calculus.
  - deleted 3y ago
    [deleted]
- Hirrolot 3y ago
  > which is what makes it a useful concept rather than an arbitrary bundle of rules. I cannot recall a single practical FP language based on the Y combinator for recursion. The typical approach is to extend lambda calculus with a separate recursion primitive.
  - lmm 3y ago
    The lambda calculus was never meant to be a "practical FP language"; it predates programming languages and even mechanical stored-program computers as we understand them.
    - Hirrolot 3y ago
      What are the useful cases of the Y combinator then? (I don't say that the lambda calculus is useless, I was responding to a comment that claimed the lambda calculus is useless without the Y combinator.)
      - lmm 3y ago
        Emulating recursion, and more generally the whole Church-Turing thesis. The fact that you can represent mechanical computation through, well, computation - the fact that equating those concepts makes sense at all, which was such a huge innovation that today it seems too banal to even notice.
        Hirrolot 3y ago
        You keep answering with the same words though. My question was _where_ the Y combinator is useful, not _what_ it is designed for, which I am of course aware of.
        lmm 3y ago
        What do you mean "where"? In Princeton? In the Proceedings of the London Mathematical Society? In the head of anyone who presumes to think about computation?
      - kragen 3y ago
        the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all so when you're faced with a formal system that doesn't seem to support indefinite iteration, perhaps because you are trying to design it to guarantee termination, a useful exercise is to try to construct an analogue of the y-combinator in it if you can't, you may have gained enough insight into the problem to show that the system actually does guarantee termination, and maybe even show useful time bounds on it if you can, you have usually shown the system is turing-complete, which means you can appeal to rice's theorem whenever you are tempted to analyze the behavior of the system in any way, so you can satisfy yourself with partial decision procedures that work often enough to be useful and are conservative in the appropriate way, rather than wasting time trying to find a complete solution (also if you're designing the system you might consider either supporting iteration more directly or removing the back door) every once in a while it's also useful in practice to be able to program a weird machine, too
  - fanf2 3y ago
    The Miranda programming language was an early lazy functional programming language, an ancestor of Haskell. It compiles down to combinators, and uses combinator reduction as its evaluation strategy. This became obsolete by the end of the 1980s but it’s still neat to learn how it works. One of the primitive combinators is Y. Here is its implementation: https://github.com/pkreyenhop/miranda/blob/master/reduce.c#L400 https://github.com/pkreyenhop/miranda/blob/master/reduce.c#L...
- cvoss 3y ago
  The simply typed, and, especialy, the dependently typed lambda calculi are extremely versatile and powerful subsets of untyped lambda calculus which do not admit the Y combinator. Their usefulness does not at all require universality, and are, perhaps, more useful for being typed.
  - lmm 3y ago
    There are many useful things that are not "the lambda calculus". "The lambda calculus" is more widely known and important, largely because it is universal, hence Church-Turing thesis.
    - cvoss 3y ago
      Of course there are other useful things. But a comment argued that the presence of Y is what makes untyped lambda calculus useful. My rebuttal is that certain subsets which (intentionally) lack Y are more useful. Applications of typed calculi abound, but one rarely sees applications of the untyped calculus. Universality is not so important, it would seem. For example, infinite computations can still be modeled in typed calculi, but one has more control over them in that setting than running on "bare metal" untyped lambda calculus.
      - lmm 3y ago
        Ok, "useless" is a slight exaggeration; non-universal calculi can be useful. But the thing that makes the lambda calculus so important and famous - the thing that makes it "the lambda calculus - is universality, and that's the ur-application that makes all of the subsequent application of calculi to mechanical computation possible.

lmm 3y ago

The Y combinator is in a sense the heart of the λ calculus; it's a key discovery for understanding that the λ calculus is universal, which is what makes it a useful concept rather than an arbitrary bundle of rules.

andsoitis 3y ago
> heart of the λ calculus The Y combinator is a specific fixed-point combinator in lambda calculus. It is used to express recursion in lambda calculus where direct recursion is not initially available due to the lack of named functions. The Y combinator demonstrates the power of lambda calculus.
- deleted 3y ago
  [deleted]
Hirrolot 3y ago
> which is what makes it a useful concept rather than an arbitrary bundle of rules. I cannot recall a single practical FP language based on the Y combinator for recursion. The typical approach is to extend lambda calculus with a separate recursion primitive.
- lmm 3y ago
  The lambda calculus was never meant to be a "practical FP language"; it predates programming languages and even mechanical stored-program computers as we understand them.
  - Hirrolot 3y ago
    What are the useful cases of the Y combinator then? (I don't say that the lambda calculus is useless, I was responding to a comment that claimed the lambda calculus is useless without the Y combinator.)
    - lmm 3y ago
      Emulating recursion, and more generally the whole Church-Turing thesis. The fact that you can represent mechanical computation through, well, computation - the fact that equating those concepts makes sense at all, which was such a huge innovation that today it seems too banal to even notice.
      - Hirrolot 3y ago
        You keep answering with the same words though. My question was _where_ the Y combinator is useful, not _what_ it is designed for, which I am of course aware of.
        lmm 3y ago
        What do you mean "where"? In Princeton? In the Proceedings of the London Mathematical Society? In the head of anyone who presumes to think about computation?
    - kragen 3y ago
      the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all so when you're faced with a formal system that doesn't seem to support indefinite iteration, perhaps because you are trying to design it to guarantee termination, a useful exercise is to try to construct an analogue of the y-combinator in it if you can't, you may have gained enough insight into the problem to show that the system actually does guarantee termination, and maybe even show useful time bounds on it if you can, you have usually shown the system is turing-complete, which means you can appeal to rice's theorem whenever you are tempted to analyze the behavior of the system in any way, so you can satisfy yourself with partial decision procedures that work often enough to be useful and are conservative in the appropriate way, rather than wasting time trying to find a complete solution (also if you're designing the system you might consider either supporting iteration more directly or removing the back door) every once in a while it's also useful in practice to be able to program a weird machine, too
- fanf2 3y ago
  The Miranda programming language was an early lazy functional programming language, an ancestor of Haskell. It compiles down to combinators, and uses combinator reduction as its evaluation strategy. This became obsolete by the end of the 1980s but it’s still neat to learn how it works. One of the primitive combinators is Y. Here is its implementation: https://github.com/pkreyenhop/miranda/blob/master/reduce.c#L400 https://github.com/pkreyenhop/miranda/blob/master/reduce.c#L...
cvoss 3y ago
The simply typed, and, especialy, the dependently typed lambda calculi are extremely versatile and powerful subsets of untyped lambda calculus which do not admit the Y combinator. Their usefulness does not at all require universality, and are, perhaps, more useful for being typed.
- lmm 3y ago
  There are many useful things that are not "the lambda calculus". "The lambda calculus" is more widely known and important, largely because it is universal, hence Church-Turing thesis.
  - cvoss 3y ago
    Of course there are other useful things. But a comment argued that the presence of Y is what makes untyped lambda calculus useful. My rebuttal is that certain subsets which (intentionally) lack Y are more useful. Applications of typed calculi abound, but one rarely sees applications of the untyped calculus. Universality is not so important, it would seem. For example, infinite computations can still be modeled in typed calculi, but one has more control over them in that setting than running on "bare metal" untyped lambda calculus.
    - lmm 3y ago
      Ok, "useless" is a slight exaggeration; non-universal calculi can be useful. But the thing that makes the lambda calculus so important and famous - the thing that makes it "the lambda calculus - is universality, and that's the ur-application that makes all of the subsequent application of calculi to mechanical computation possible.