Recursion in Lambda Calculus

Theorem About Recursion

Recursion is the process of defining a function in terms of itself. However, in lambda calculus, functions cannot reference themselves directly, as there are no variable bindings for function names. This is where the Y-combinator and fixed-point theory come into play.

The recursion theorem states:

\forall M \exists F : F \equiv_{β} M [x := F]

It means that for every function $M$ , there exists a function $F$ such that $F$ is equal (under β-reduction) to $M$ with $x$ replaced by $F$ itself.

Breaking it Down

$M [x := F]$ means "replace $x$ with $F$ in $M$ ".
- In simpler terms, if $M$ is some function with an unknown part $x$ , we replace $x$ with $F$ .
$F$ satisfies the equation $F = M (F)$ .
- This means that applying $M$ to $F$ just gives back $F$ .
- $F$ is a fixed point of $M$ , which makes it self-referential.
In Lambda Calculus, we can write this stuff like this:

F \equiv (λ x . M) F

Example to Make It Clear

Suppose we define a function $M$ like this:

M (x) = 2 x + 1

According to the theorem, we need to find $F$ such that:

F = M (F) = 2 F + 1

This means that $F$ is a solution to the equation:

F = 2 F + 1

If we solve for $F$ , we get:

F - 2 F = 1

- F = 1

F = - 1

Thus, $F = - 1$ is a fixed point because if we plug it into $M$ , we get:

M (- 1) = 2 (- 1) + 1 = - 1

which is the same as $F$ .

What This Means in Lambda Calculus

In lambda calculus, we don’t have numbers like $- 1$ , but we can still define functions that refer to themselves.
The theorem says we can find an $F$ that satisfies $F = M (F)$ , meaning $F$ is self-referential.
This is how recursion is possible—it allows a function to call itself without explicitly having a name.

By using the Y-combinator, we can construct $F$ automatically:

F = Y M = M (Y M)

This allows recursion without naming the function explicitly.

Example: Recursive Addition with the Y-Combinator

Now that we understand how the Y-combinator enables recursion in lambda calculus, let’s go through a step-by-step example of addition using the Y-combinator.

Step 1: Defining Addition Recursively

We define addition as a recursive function in an imperative style:

def add(x, y):
    if isZero(y):
        return x
    else:
        return add(increment(x), decrement(y))

This function works by:

Returning $x$ if $y = 0$ (base case).
Otherwise, increasing $x$ and decreasing $y$ until $y$ reaches $0$ .

Step 2: Transforming to a Lambda Expression

Since lambda calculus does not allow direct recursion, we rewrite add by introducing a placeholder function f:

def add(f, x, y):
    if isZero(y):
        return x
    else:
        return f(increment(x), decrement(y))  # Indirect recursive call (magic!)

In lambda calculus, this becomes:

add \equiv λ f . λ x . λ y . (if isZero y then x else f (increment x) (decrement y))

Since f is meant to call add recursively, we apply the Y-combinator to define recursion:

Y add \equiv add (Y add)

Now, add can call itself indirectly through Y add!

Remark:

We already know that $Y M = M (Y M)$ , so here our $M$ is add.

Step 3: Evaluating 1 + 1 Step by Step

We now evaluate:

(Y add) 1 1

First expansion

(Y add) 1 1 \equiv add (Y add) 1 1 \equiv (λ x . λ y . (if isZero y then x else (Y add) (increment x) (decrement y))) 1 1

Substituting values:

if isZero 1 then 1 else (Y add) (increment 1) (decrement 1)

Since isZero(1) = False, we continue:

(Y add) (2) (0)

Second expansion

Expanding again:

(Y add) 2 0 \equiv add (Y add) 2 0 \equiv (λ x . λ y . (if isZero y then x else (Y add) (increment x) (decrement y))) 2 0

Substituting values:

if isZero 0 then 2 else (Y add) (increment 2) (decrement 0)

Since isZero(0) = True, we return 2.

✅ Final result: $1 + 1 = 2$ 🎉

Why Does This Work?

We define addition recursively by reducing $y$ while incrementing $x$ .
The Y-combinator enables recursion by ensuring add can call itself.
The evaluation follows a structured reduction process, stopping when y = 0.

🚀 This method allows us to express recursion in pure lambda calculus, without explicitly naming functions!