Fixed-Point Theorem (Lambda Calculus)

lambda-calculus

Definition

Fixed-Point Theorem (Lambda Calculus)

Every lambda abstraction has a fixed-point.

Proof

Fixed-Point Theorem (Lambda Calculus)

The Y combinator

$$\mathbf{Y}\equiv \lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$

is a fixed-point generator. It holds that:

$$\mathbf{Y}N{\to }_{\beta }N\mathbf{Y}N$$

for every lambda abstraction $N$.