What is the cardinality of the set of untyped $\lambda$-calculus functions? I know it’s an infinity, but is it countable or uncountable?

What is the cardinality of the set of untyped $\lambda$-calculus functions? I know it’s an infinity, but is it countable or uncountable?

Let $\Lambda$ be the set of untyped $\lambda$-calculus functions. We know the grammar of $\lambda$-calculus functions:

1. If $x$ is a variable, then $x \in \Lambda$.
2. If $M, N \in \Lambda$, then $(MN) \in \Lambda$.
3. If $x$ is a variable and $M \in \Lambda$, then $(\lambda x.M) \in \Lambda$.

Given this, what is $|\Lambda|$?

Would it help to define a grammar for variables? Do variable names consist of only one character or can they consist of multiple characters?

Solution 1:

It's $\max(\aleph_0, \text{# variables})$.

Usually we say that there are countably many variables (which we formally write as $x_1, x_2, x_3, \ldots$), and in that case there are countably many lambda terms.

To see why, let's overcount and look at all possible strings of $\lambda$s, $.$s, $($s, $)$s, and variables. There are countably many strings of length $1$, countably many strings of length $2$, and so on. Since every lambda term shows up in one of these, we get all the terms in this way. But a countable union of countable sets is countable, so we find there are at most countably many formulas. As you say, obviously there are infinitely many formulas, and the claim follows.

As a quick exercise, what happens if we have $|\mathbb{R}|$-many variables? Can you show that there are $| \mathbb{R}|$ formulas in that case?

I hope this helps ^_^