# Notes

### 2015-06-02

Here is a short note for those who have trouble remembering Russell's Paradox or the definition of the Y combinator in lambda-calculus. I will expose here one observation that allows you to remember just one of the two and recover the other. The actual link between these two notions prevents the lambda-calculus from serving the purpose Church had for it: giving a formal basis to mathematics. Fortunately the lambda-calculus found another application not any less important than grounding mathematics: it describes universal computations.

Russell's Paradox considers the set R = { X | X ∉ X } of sets that do not belong to themselves. Now if such set exists, R ∈ R if and only if R ∉ R, and we have a contradiction. Let us encode this reasoning in lambda-calculus, we start by observing that sets can be represented by their characteristic function: a function returning 1 for all members of the set and 0 for the others. Assume that we represent the negation using a function N. Then, we can define the set R in lambda-calculus by the following characteristic function:

R = λ x. N (x x)

Let's observe what happens when we ask if R is in itself:
We form `Y = R R`

(that is exactly the Y combinator) and by one
application of beta-reduction, we get `N (R R) ≡ N Y`

.

We just found a fixpoint of N. In set theory we had a fixpoint of
negation, but negation does not have fixpoint, hence the paradox. In the
lambda-calculus case, we get out of this with a trick: if N has no fixpoint,
the computation we get by applying these characteristic functions never
terminates, it *diverges* and we face an ever-running program that
never gives us the answer if R is in itself or not.