Learning path

Full curriculum

Full curriculum

Unit content

Fixed-point combinators and recursion in lambda calculus

The untyped lambda calculus has no built-in named recursion, yet recursive behavior can be expressed by obtaining a fixed point of a function that describes one recursive layer.

A fixed-point combinator $Y$ satisfies

$$YF = F(YF).$$

Suppose $F$ describes one layer of factorial computation:

$$F = \lambda f.\lambda n.;\text{if }n=0\text{ then }1\text{ else }n\cdot f(n-1).$$

The parameter $f$ stands for the recursive call. Applying the combinator gives

$$YF=F(YF),$$

so the recursive calls made through $f$ refer again to $YF$. The result behaves like a self-referential factorial definition even though the calculus itself contains no special rec construct.

The exact combinator depends on evaluation strategy. The classic $Y$ combinator works directly under normal-order reduction, while strict call-by-value evaluation needs a variant that delays the self-application responsible for recursion.

Fixed-point combinators reveal that named recursion can be derived from higher-order functions and self-application. They also make precise the connection between a recursive program and the fixed-point equation that characterizes its behavior.