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/Al...
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.
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!).
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.
It might be valuable to expand the definitions of things a bit.
First, we talk about characteristic functions. As noted, they are merely functions which return either 1 or 0, True or False. They represent sets by examining their argument and returning True if and only if the set they represent contains that thing.
So, if x is a characteristic function and (x x) is True, then x "contains" itself. Then N is just negation, so if N (x x) is True then x does not "contain" itself. That much is simple.
Now we form a special new characteristic function, R, defined as
R x = N (x x)
When is (R x) True? Exactly when x is "contained" in R. When does that happen? When N (x x), e.g., when x does not "contain" itself.
So this is a well-defined characteristic function and therefore represents what we might think is a well-defined set.
But what happens when we check (R R), i.e. to see if R contains itself?
Well, R, by definition, contains all things which are not members of themselves. If R is in R then (R R) is True, but then N (R R) is False and (R R) = False. Contradiction!
We can inline R into (R R) in order to take a look at the functional form.
(\x -> N (x x)) (\x -> N (x x))
and the author notes that this is the same form as the Y-combinator with its first argument specialized to N.
So to translate that back into natural language, R R asks 'does the set of sets which don't contain themselves contain itself?', and the answer, 'Y N' reads, 'why not'?
How is this example special, compared to the general notion:
F = (\x -> Z (x x))
Y f = (\x -> f (x x)) (\x -> f (x x))
Y Z = F F
so, any set F that is defined in terms of how sets (functions) relate to themselves, fits into the Y combinator. Which is expected, since Y is the essence of recursion.
I don't know that there's anything special about Russell's paradox in particular, to be honest. It has obvious historical importance, obviously, but I doubt that's what you're looking for.
There's something a bit remarkable about how trivial it is, I suppose. Booleans are very simple types, if you'll give me those, and then Not is the only involution!
Ahh.. thank you. We touched on this in philosophy courses but my specific courses did not cover it in depth. Thank you for explaining the notation for me.
I'm not a native speaker, I'm sorry you had trouble going through it. I tried to keep it short but maybe did not articulate the first paragraph and the end of the second ideally.
minor edit for you since you're not English: it's Russell's Paradox. It's amazing how much going along with accepted spelling conventions helps people like a piece, especially a short one. Good luck!
I've read that languages for mathematical reasoning (such as Coq) are not Turing-complete to avoid issues like this. We can tolerate the possibility of infinite loops when we actually execute a program and see that it returns an answer, but apparently programs used as proofs aren't actually run, so type-checking needs to eliminate this sort of paradox.
It's true! The reasoning is fairly simple, though.
In such a language, types classify terms and types correspond to theorems. The type/theorem for a fixed point is
fix : forall a . (a -> a) -> a
which as a theorem reads: "for any proposition A, if we can prove 'if A, then A' then we can prove A". Hopefully it's now clear why having 'fix' in your prover language won't work!
Not quite. You're appleaing to the Curry-Howard correspondance, which is neat but is not used by many theorem provers. Furthermore,
> fun fix (f : 'a -> 'a) : 'a = fix f;
val fix = fn: ('a -> 'a) -> 'a
The trick is that all functions must be total, which is the crux of the matter (and why the Y-combinator exhibits the paradox, because it allows nontermination). This is why we have stuff like the polymorphic lambda calculus, in which termination is guaranteed and the Y-combinator is untypeable.
Correct. One way to think of it is that running the program produces a proof of the theorem. But since the program is guaranteed to terminate with a proof (since all functions are total in Coq), why run it at all? Type checking is sufficient.
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/Al...