0
$\begingroup$

Russell's paradox: The set that contains all the sets that do not contain themselves. Does it contain itself? It contains itself if and only if it does not contain itself.

Russell's paradox for the lambda-calculus: The functions that may not be applied to themselves when combined with themselves, they negate themselves.

lambda calculus uses anonymous functions called lambda-expressions. So, the paradox re-stated in lambda-calculus terms becomes:

The lambda-expressions that may not be applied to themselves when combined with themselves, they negate themselves.

If such a lambda-expression is encoded into a string w, then input to a Turing machine, will the Turing machine (Paradox Recognizer machine) accept it? not accept it: reject it? or loop forever?

Thanks in advance for your comments.

Rafee Kamouna.

$\endgroup$
  • 4
    $\begingroup$ "The functions that may not be applied to themselves when combined with themselves, they negate themselves." I'm sorry but I can't understand what you mean by that. Could you try to rephrase? $\endgroup$ – David Richerby Aug 27 '16 at 17:48
3
$\begingroup$

Russel's paradox does not apply to the lambda calculus. Intuitively speaking, Russel's paradox comes up when there is a level system (e.g. sets that are members of “bigger” sets one level up), and there is a form of negation. The lambda calculus has neither: all lambda terms are at the same level and there is no negation.

I don't know what you think you mean by “The lambda-expressions that may not be applied to themselves”. Any lambda term can be applied to any lambda term.

An analog of Russel's paradox (or rather the similar Burali-Forti paradox) arises in the higher-order typed lambda calculus, where terms have types that themselves have types. If $\mathsf{Type} : \mathsf{Type}$, it's possible to construct a well-typed term that of type $\mathsf{Type}$ that does not terminate. See Example of a false proposition when assuming Type : Type. As can be done in set theory, type theory can solve the problem by adding a universe stratification: base types have the sort $\mathsf{Type}_0$ and higher-order types obey $\mathsf{Type}_n : \mathsf{Type}_{n+1}$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.