4 ms·

I studied both (λ-calculus and Set Theory) academically and the description IS disjointed and difficult to read. I get what OP is trying to say because I alread

by dvt 11y ago

I studied both (λ-calculus and Set Theory) academically and the description IS disjointed and difficult to read. I get what OP is trying to say because I already understand these concepts. But even though the isomorphism between the Y combinator and Russell's paradox is elegant, the paradox is actually very deep (much deeper than the idea of a fixed point) -- that's why it took someone until the early 20th century to formalize it. For an awesome (and mind-blowing) explanation of the paradox, see Halmos' Naive Set Theory (botom of page 6): http://sistemas.fciencias.unam.mx/~lokylog/images/stories/Alexandria/Logica%20y%20Conjuntos/Paul%20R.Halmos%20-%20Naive%20Set%20Theory.pdf http://sistemas.fciencias.unam.mx/~lokylog/images/stories/Al...

deleted 11y ago
[deleted]
Chinjut 11y ago
It also took someone until the mid-20th century to formalize the Y combinator, though... Earliness of discovery is no grounds on which to consider the Y combinator less "deep" than Russell's paradox (if anything, the reverse!).
- dvt 11y ago
  The Y combinator followed from of the invention of λ-calculus whereas formal logic predated both Russell as well as Curry/Haskell by a large margin. Also, the idea of a "fixed point" (consider x^2-3x+4 where there's a fixed point at x=2) had already been recognized.
shasta 11y ago
Actually, the connection between non-terminating computations and Russell's paradox is fairly strong. The piece of explanation missing from the article that is that the naive conception of sets corresponds to total boolean valued functions. That is, a set is a rule that answers whether a value is in the set or not. To get set theory out of lambdas, you just have to restrict to the subset of lambdas that only apply sets to sets and that end up returning a proposition. So you'd have to reject a lambda like this: λx. x (x x), because when you rewrite that in set theory notation it looks like this: { x | x ∈ (x ∈ x) }. Bad since (x ∈ x) is a proposition used as a set. We'd also reject λx. x because it returns a set and not a proposition. Labeling expressions with one of two sorts (proposition or set) can be done statically, though, and this allows us to quickly check whether a lambda corresponds to a construction of naive set theory. Once you have this correspondence, the rest of the author's note goes through fairly well. Except that technically Y = λN. R R, not R R.

by dvt 11y ago

deleted 11y ago

[deleted]

Chinjut 11y ago

It also took someone until the mid-20th century to formalize the Y combinator, though... Earliness of discovery is no grounds on which to consider the Y combinator less "deep" than Russell's paradox (if anything, the reverse!).

dvt 11y ago
The Y combinator followed from of the invention of λ-calculus whereas formal logic predated both Russell as well as Curry/Haskell by a large margin. Also, the idea of a "fixed point" (consider x^2-3x+4 where there's a fixed point at x=2) had already been recognized.

shasta 11y ago

Actually, the connection between non-terminating computations and Russell's paradox is fairly strong. The piece of explanation missing from the article that is that the naive conception of sets corresponds to total boolean valued functions. That is, a set is a rule that answers whether a value is in the set or not. To get set theory out of lambdas, you just have to restrict to the subset of lambdas that only apply sets to sets and that end up returning a proposition. So you'd have to reject a lambda like this: λx. x (x x), because when you rewrite that in set theory notation it looks like this: { x | x ∈ (x ∈ x) }. Bad since (x ∈ x) is a proposition used as a set. We'd also reject λx. x because it returns a set and not a proposition. Labeling expressions with one of two sorts (proposition or set) can be done statically, though, and this allows us to quickly check whether a lambda corresponds to a construction of naive set theory. Once you have this correspondence, the rest of the author's note goes through fairly well. Except that technically Y = λN. R R, not R R.