Fixed-point theorem and Y-combinator

Fixed-Point Theorem

The Fixed-Point Theorem states that for any function $F$ in lambda calculus, there exists a value $X$ such that applying $F$ to $X$ returns $X$ itself:

\forall F \in Λ, \exists X \in Λ : X \equiv_{β} F X

This means that $X$ is a fixed point of $F$ , meaning applying $F$ to $X$ does not change its value.

What is a Fixed Point? 🤔

A fixed point of a function $F$ is a value $X$ that does not change when you apply $F$ to it.

In simple terms:

F (X) = X

This means $X$ stays the same, even after applying the function $F$ .

Real-World Example 🌍

Think of pressing an elevator button:

If you're on the 3rd floor and press "3", the elevator doesn't move.
The 3rd floor is a fixed point because pressing "3" doesn't change your position.

Another Example: Multiplication

Imagine a function that doubles a number:

F (n) = 2 n

If we apply $F$ to $0$ :
$F (0) = 2 \times 0 = 0$
$0$ is a fixed point because doubling it still gives $0$ .

🚀 A fixed point is a value that "stays put" under a function! It will help us to stop the recursion later...

Constructing a Fixed Point

To construct a fixed point, we define a special term $W$ :

W \equiv λ x . F (x x)

Now, let’s set:

X \equiv W W

Expanding:

X \equiv λ x . F (x x) W

Now applying $W$ :

λ x . F (x x) W \to_{β} F (W W) \equiv F X

Thus, we have:

X \equiv_{β} F X

✅ We found a fixed point for $F$ !

The Y-Combinator

The Y-Combinator is a special lambda function that finds fixed points for any function $F$ . It is crucial in lambda calculus because it enables recursion in a system that lacks named functions.

Definition of the Y-Combinator

Y \equiv λ f . (λ x . f (x x)) (λ x . f (x x))

When applied to $F$ , we get:

Y F \equiv (λ f . (λ x . f (x x)) (λ x . f (x x))) F

Expanding:

(λ f . (λ x . f (x x)) (λ x . f (x x))) F \to_{β} (λ x . F (x x)) (λ x . F (x x))

Now, look at this magic:

\begin{aligned} Y F \equiv (λ x . F (x x)) (λ x . F (x x)) & \equiv (λ x . F (x x)) M \\ \to_{β} F (M M) \\ \equiv F ((λ x . F (x x)) (λ x . F (x x))) \\ \equiv F (Y F) \end{aligned}

Thus, $Y F$ satisfies:

Y F \equiv_{β} F (Y F)

✅ $Y F$ is a fixed point of $F$ , meaning $Y$ finds fixed points for any function $F$ !

Why is the Y-Combinator Important?

🔁 Enables recursion in lambda calculus, where self-reference is not inherently possible.
🏗 Builds loops and functions that call themselves indefinitely.
🔍 Used in functional programming (e.g., Haskell, Scala) for defining recursive functions without explicit self-references.