Fixed-Point Combinators and How Recursion Enters a Nameless Calculus

A recursive definition names itself. The factorial function is defined in terms of factorial, the list traversal in terms of the traversal of the tail. In a language with named definitions that is unproblematic: the name is bound in an environment that already contains the definition being introduced. In the lambda calculus there are no named definitions, and a term cannot contain itself — a term is a finite tree, and a subtree cannot be the whole tree.

So recursion has to be recovered rather than assumed, and the recovery is one of the more surprising constructions in the theory. No new primitive is added. The self-reference is manufactured out of duplication: a term that applies its argument to itself, passed to a copy of itself, produces the effect of a definition that refers to its own body. The fixed-point combinators are the terms that perform this trick, and their behaviour under different evaluation strategies is the reason several variants exist.

The fixed-point property, stated without recursion

A fixed point of a function f is a value x with f x = x. In the lambda calculus, the equation is beta-convertibility: x is a fixed point of f when f x →→ x and x →→ f x, or more usefully when f x reduces to x in some number of steps. A fixed-point combinator is a closed term Y such that for every term f, Y f is a fixed point of f.

The point of the definition is that it converts recursion into ordinary application. If a function F expects its recursive self as an argument, then Y F supplies it:

factorial = Y (λself. λn. isZero n 1 (mult n (self (pred n))))

The inner lambda is not recursive. It receives self as a parameter, and self is whatever Y supplies. The equation Y F →→ F (Y F) is exactly the unfolding that a recursive definition needs: it says that Y F behaves like F applied to itself, so the self argument is again the whole function. Each unfolding happens on demand, which is why the recursion terminates only when the base case is reached.

The existence of such a Y is the fixed-point theorem for the lambda calculus, and it holds for the untyped calculus precisely because terms can be applied to themselves. In a typed calculus without recursive types the theorem fails: the simply typed lambda calculus has no fixed-point combinator, because every term is strongly normalising and a fixed-point combinator would produce divergence. Adding a recursion primitive or recursive types is exactly adding back the power that the type system removed.

Constructing self-application

The construction has two layers. The inner layer is a term that takes a function and produces a term which applies that function to itself:

U = λf. f f

U g reduces to g g. If g is a lambda that expects a self-argument, then g g is that lambda applied to itself, which is the self-reference wanted. The trouble is that g must be able to receive itself as an argument, and a term cannot literally contain itself; it can only be duplicated by the act of applying U.

The outer layer packages this so that the duplication is delayed until the function is applied to an argument. The Curry combinator:

Y = λf. (λx. f (x x)) (λx. f (x x))

Reducing Y F:

Y F
→ (λx. F (x x)) (λx. F (x x))
→ F ((λx. F (x x)) (λx. F (x x)))
= F (Y F)

Two beta steps, and the result is F applied to a term that is again Y F. The self-reference is not stored; it is reconstructed at every unfolding by the same two steps. This is the important structural fact: Y F has no finite normal form when F uses its argument, because the unfolding never stops unless the body of F discards the self-argument.

The Turing combinator achieves the same property with a different arrangement of the same idea:

Θ = (λx. λy. y (x x y)) (λx. λy. y (x x y))

Here the same self-application is reached through an extra binder rather than by direct duplication, and Θ F →→ F (Θ F) takes two steps as well.

Why call-by-value needs a different combinator

Y relies on the argument (λx. F (x x)) being substituted unevaluated. Under call-by-value, the argument is reduced before the application, and reducing (λx. F (x x)) (λx. F (x x)) means reducing the argument of that application, which is the same term, which requires reducing it again. The reduction diverges before F is ever applied. So the naive Y does not work in a strict language: it loops while trying to construct the fixed point, not while using it.

The standard repair is the Z combinator, also called the strict or call-by-value fixed-point combinator. It wraps the recursive call in an extra lambda so that the self-application is not evaluated until the resulting function is applied to an argument:

Z = λf. (λx. f (λv. x x v)) (λx. f (λv. x x v))

Now Z F reduces to F (λv. (λx. F (λv. x x v)) (λx. F (λv. x x v)) v), and the inner self-application sits under a lambda, so call-by-value stops. When the function is applied to an argument, the deferred application fires and produces the next unfolding. The cost is one extra beta step per recursive call and one extra closure allocation, because the thunk λv. x x v is a real value that has to be built.

The same eta-expansion trick appears in typed settings. In a language whose recursion is encoded through a fixed-point operator rather than a primitive, the operator’s type is ∀α. (α → α) → α, and its call-by-value implementation takes the Z shape rather than the Y shape, for exactly the reason above.

Combinator	Equation	Steps to unfold	Works under call-by-name	Works under call-by-value
Y	Y F →→ F (Y F)	2	yes	no
Θ	Θ F →→ F (Θ F)	2	yes	no
Z	Z F →→ F (λv. Z F v)	2	yes	yes

The Z row is not a strict improvement; what F receives is an eta-expanded variant rather than Z F itself, so each use of the self-argument costs an extra application. Under call-by-name, Z F and Y F are beta-eta equivalent, so nothing is lost semantically; under call-by-value the difference is the difference between a program that terminates and one that does not.

The recursion that does not terminate

Y F unfolds forever if F always uses its self-argument. The canonical example is Y (λself. self), which reduces to itself in two steps and never reaches a value. That is not a defect of the combinator; it is the intended semantics of a recursive definition with no base case, and it corresponds to an infinite loop in any language.

The interesting cases are the ones where the unfolding terminates. Y (λself. λn. ...) terminates for any n that reaches the base case, because each unfolding happens only when the function is applied, and the branch that does not recurse discards self. This is guarded recursion in the untyped setting: there is no type system enforcing it, so whether a program terminates is a property of the particular F, not of the construction. The fixed-point combinator makes every F have a fixed point, including the ones whose fixed point is bottom.

That universality has a cost that shows up in reasoning. Because Y F has no normal form for a large class of F, equational reasoning about programs that use it requires a theory of approximation rather than plain beta conversion. The standard device is the Böhm tree, an infinite tree that records the successive unfoldings, and the ordering on those trees is what makes “this program diverges” a statement with a truth value. Finite reasoning about Y is possible only for the fragments where the unfoldings terminate, and that restriction is why total languages reject the combinator outright.

Encoding recursion without a combinator

There is an alternative that avoids Y entirely, and it is worth knowing because it is what a compiler for a recursive function actually generates. Instead of a fixed-point combinator, the definition is tied through an environment: the closure for the function body contains a reference to a cell that is filled with the closure itself after it is allocated. The recursion is a cycle in the heap, not a self-application in the syntax.

The two approaches differ in cost and in what they can express. The heap cycle is O(1) to set up and O(1) per recursive call, with the indirection resolved at each call. The combinator costs two or three beta steps per unfolding and allocates a new closure at every unfolding, because the self-argument is reconstructed rather than reused. For a recursive function called n times, the combinator does O(n) extra allocation; the environment cycle does none. That is the reason no practical implementation of a strict language uses Y or Z at runtime, even though both are the textbook account of what recursion means.

The trade is in reasoning, not in execution. A heap cycle is invisible to the equational theory; there is no term that denotes it, so a proof about the program cannot proceed by reduction. The combinator is a term, so Y F →→ F (Y F) is a beta step and the usual machinery applies. Implementations choose the cycle and reason about it with a separate semantics; textbooks choose the combinator and pay the reduction cost. Both describe the same function.

Where the construction meets the rest of the theory

The fixed-point theorem is the point at which the untyped calculus becomes a programming language rather than a notation for functions. It is also the point at which several of the surrounding results become sharp. Confluence still holds: Y F may have no normal form, but if a term has one, the Church-Rosser theorem still guarantees it is unique, and the fixed-point construction does not disturb that. Normal-order reduction still finds the normal form when one exists, which is why a lazy implementation of Y terminates on the same programs as the theory predicts, while a strict one needs Z to even start.

The construction also interacts with the encodings. A recursive function over Church numerals is a term whose unfoldings are guarded by the numeral’s iterator, so the recursion depth is bounded by the value being processed, and the whole computation is a finite reduction sequence. A recursive function that does not consume a numeral has no such bound, and its normal form may not exist. That distinction — recursion structurally decreasing on an encoded value versus recursion with no measure — is the untyped analogue of termination checking, and it is the reason the Church encodings and the fixed-point combinators are usually presented together. The machinery that actually runs these terms, deferring the unfolding until it is needed, is described with the Krivine machine and its environment-based cousins.