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.