3 ms·
Actually, the connection between non-terminating computations and Russell's paradox is fairly strong. The piece of explanation missing from the article that is
by 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.