Natural Numbers and Arithmetic

The Concept of Numbers in Lambda Calculus

Numbers are fundamental in computation, but in lambda calculus, we don't have built-in numbers like 1, 2, or 3. Instead, we must construct them using functions.

This idea comes from Alonzo Church, the inventor of Church numerals — a way to represent natural numbers using functions alone.

At its core, a number n is simply a function that applies another function n times.

For example:

• 0 applies a function 0 times.
• 1 applies a function once.
• 2 applies a function twice, and so on.

Church numerals

In lambda calculus, natural numbers are represented using Church numerals — a way to encode numbers as functions. The idea is simple:
A number $n$ is a function that applies another function $n$ times.

The general definition is:

So, basically, $c_n$ is a function that represents the number $n$.

Where:

• $c_0$ (zero) does nothing:$$c_0\equiv \lambda x.x$$
• $c_1$ (one) applies f once:$$c_1\equiv \lambda f.\lambda x.f(x)$$
• $c_2$ (two) applies f twice:$$c_2\equiv \lambda f.\lambda x.f(f(x))\equiv \lambda f.\lambda x.f^2(x)$$
• And so on…

Addition

Adding two Church numerals means applying one number's function on top of another number’s function:

Looks complex, right? Let's break it down. Keep eyes on colors!

Example

Let's compute $2+2$:

We substitute $c_2$:

First, we apply $c_2$ instead of $x$:

Expand $c_2$ instead of $y$:

Now, substitute $c_2\equiv \lambda f.\lambda x.f(f(x))$:

Applying $p$ and $q$ in the inner function $\lambda f.\lambda x.f(f(x))$:

Now, substitute $c_2\equiv \lambda f.\lambda x.f(f(x))$:

Let $p(p(q))\equiv M$:

Now, push $p$ and $M$ into the inner function:

Expand $M\equiv p(p(q))$:

Which is exactly $c_4$!

✅ We have computed $2+2=4$ correctly using lambda calculus!

Successor and Predecessor Functions

So, another way to define numbers could be implemented inductively using pairs.

Basically, $c_n$ is a pair of successor operation $\mathbb{F}$ and the previous number $c_{n-1}$.

In other words:

Successor Function (Increment)

The successor function adds one to a given number:

Where:

• $F$ is the successor operation:$$\mathbb{F}\equiv \lambda x.\lambda y.y$$
• $[M,N]$ represents a pair:
  $[M,N]\equiv \lambda z.zMN$

Thus, $succ$ applies $\mathbb{F}$ once more, effectively adding one.

Let's evaluate $succ{c}_2$:

So, $succ{c}_2=c_3$!

It's like incrementing the number by one. 🚀

int x = 2;
x++;
std::cout << x; // 3

Predecessor Function (Decrement)

The predecessor function subtracts one from a given number:

Where:

• $\mathbb{F}$ is the function used to track previous values.
• The function applies $\mathbb{F}$ while counting up, keeping track of the last valid number.

Let's evaluate $dec{c}_3$:

So, $dec{c}_3=c_2$!

It's like decreasing the number by one. 🚀

int x = 3;
x--;
std::cout << x; // 2

Zero Check Function

To check if a number is zero, we use the function:

This function takes a Church numeral and applies it to $\mathbb{T}$ (true).

Let's evaluate $isZero{c}_2$:

Since $c_2$ applies functions twice, it doesn't return $\mathbb{T}$ but instead produces $\mathbb{F}$ (false).

✅ Correct! $isZero(c_2)=false$.

Special Case: Zero Check on $c_0$

Since $c_0$ does nothing, it returns $\mathbb{T}$, meaning $isZero(c_0)=true$!

✅ Success! We can now check if a number is zero in lambda calculus. 🚀

Special Case: Decrement Zero

Let's try to decrement $c_0$:

Thus, $dec(c_0)=\mathbb{F}$. So, unfortunately (or fortunately), we can't decrement zero in lambda calculus! It returns $\mathbb{F}$ instead. No sense, right? 🤷‍♂️