Fixed-Point Semantics of Recursion
Recursion writes a circular definition. When we say
f(n) \;=\; \text{if } n = 0 \text{ then } 1 \text{ else } n \times f(n-1),
we have used f on the right of its own definition. Read naively this is not a
definition at all — it is an equation, and equations can have zero, one, or many solutions.
What licenses us to speak of "the function f that this defines"? The
answer, and one of the most elegant ideas in all of computer science, is that the meaning of a recursive
definition is a least fixed point — and, thanks to the
domain theory
of the previous page, that fixed point always exists and can be reached by climbing a chain.
From a recursive name to a functional
The trick is to peel the recursion off the name. Rewrite the equation as a demand that
f be a fixed point of a non-recursive functional
F — a function on functions:
F(g) \;=\; \lambda n.\ \text{if } n = 0 \text{ then } 1 \text{ else } n \times g(n-1), \qquad f = F(f).
Now F itself has no recursion in it: hand it any function
g and it hands back a new function that "does one more level" of the
computation before delegating to g. A solution of the original equation is
exactly a fixed point of F, a
f with F(f) = f. Two questions remain: does a fixed
point exist, and if several do, which one is the meaning of the program?
The domain is the flat function space
D = [\mathbb{N} \to \mathbb{N}_\bot] of partial functions, ordered by
the graph-inclusion order: g \sqsubseteq h iff wherever
g is defined, h agrees with it (and
h may be defined in more places). The bottom
\bot is the totally undefined function — the program that always
diverges — and it approximates every partial function. This is a pointed CPO, and
F is continuous on it.
The ascending Kleene chain
Here is the payoff. Start from the least element \bot — the function that
knows nothing — and apply F over and over. Because
\bot \sqsubseteq F(\bot) (bottom is below everything) and
F is monotone, applying F to both sides keeps the
order, so we generate an ascending chain:
\bot \;\sqsubseteq\; F(\bot) \;\sqsubseteq\; F^2(\bot) \;\sqsubseteq\; F^3(\bot) \;\sqsubseteq\; \cdots
Each rung is more defined than the last. For the factorial functional,
F^n(\bot) is exactly "factorial, but only for inputs
< n; undefined beyond". The chain climbs, filling in one more argument at
every step, and its least upper bound is the full factorial function. Reveal the climb:
Because D is a CPO, this chain has a lub
\bigsqcup_n F^n(\bot); call it
\mathrm{fix}(F). And because F is
continuous, that lub is a genuine fixed point:
F\!\left(\bigsqcup_{n} F^n(\bot)\right) \;=\; \bigsqcup_{n} F\!\left(F^n(\bot)\right) \;=\; \bigsqcup_{n} F^{n+1}(\bot) \;=\; \bigsqcup_{n} F^n(\bot).
The first equality is continuity; the last drops the harmless bottom rung. So the limit of the chain is
a fixed point — and it is the least one, because every rung
F^n(\bot) lies below any fixed point (a quick induction), so their lub does
too.
The theorem, stated properly
Let (D, \sqsubseteq, \bot) be a pointed CPO and
F : D \to D continuous. Then F has a
least fixed point, given by the lub of the ascending Kleene chain:
\mathrm{fix}(F) \;=\; \bigsqcup_{n \ge 0} F^n(\bot).
It is a fixed point (F(\mathrm{fix}(F)) = \mathrm{fix}(F)) and the least one:
for any d with F(d) \sqsubseteq d (a
pre-fixed point) we have \mathrm{fix}(F) \sqsubseteq d.
On a complete lattice L, every monotone map
F : L \to L has a least fixed point, and it equals the meet of all pre-fixed
points:
\mathrm{lfp}(F) \;=\; \bigsqcap \{\, x \in L \mid F(x) \sqsubseteq x \,\}.
The whole set of fixed points is itself a complete lattice.
The two theorems are cousins with different hypotheses. Knaster–Tarski needs a complete lattice
but only monotonicity, and reaches the fixed point "from above" as a meet. Kleene needs only a
CPO but demands continuity, and reaches it "from below" as the lub of a chain you can
actually compute. For denotational semantics Kleene's version is the tool of choice: its chain
is the sequence of finite approximations a machine literally produces, so the theorem is not just an
existence proof — it is an algorithm.
Iterating a functional to its fixed point
Let us watch the Kleene chain in code. We represent an approximation
F^n(\bot) as a partial function on
\mathbb{N} that returns undefined where it is not yet defined
(that is our \bot at a point). The functional
F for factorial is written once, non-recursively, and we apply it repeatedly
starting from the everywhere-undefined function.
// A partial function ℕ → ℕ⊥ : returns a number, or undefined ( = ⊥ at that point).
type PFun = (n: number) => number | undefined;
// ⊥ : the totally undefined function — the bottom of the CPO.
const bottom: PFun = (_n) => undefined;
// The factorial FUNCTIONAL F : (PFun) → PFun. No recursion inside — it calls its argument g.
function F(g: PFun): PFun {
return (n: number) => {
if (n === 0) return 1;
const prev = g(n - 1); // delegate one level down to the approximation g
return prev === undefined ? undefined : n * prev;
};
}
// Build the Kleene chain ⊥ ⊑ F(⊥) ⊑ F²(⊥) ⊑ … and print how much each rung defines.
let approx: PFun = bottom;
for (let step = 0; step <= 5; step++) {
const defined: number[] = [];
for (let n = 0; n <= 6; n++) if (approx(n) !== undefined) defined.push(n);
const shown = defined.map((n) => `${n}!=${approx(n)}`).join(", ");
console.log(`F^${step}(⊥) defined on {${defined.join(",")}}` + (shown ? ` -> ${shown}` : " (nothing yet)"));
approx = F(approx); // climb one rung
}
// The limit ⊔ Fⁿ(⊥) is the real factorial — check it agrees on a value now fully defined.
console.log("limit at 5! = " + F(F(F(F(F(F(bottom))))))(5));
Each rung F^n(\bot) is defined on exactly
\{0, 1, \dots, n-1\} — the chain fills in one more argument every step and
never revises a value it already fixed (that is monotonicity in action). No single rung is the
whole factorial, but their limit is. That limit is \mathrm{fix}(F), the
meaning of the recursive definition.
It says the honest thing: \bot. Consider the useless definition
f(n) = f(n) + 1, whose functional is
F(g) = \lambda n.\, g(n) + 1. Starting from
\bot, every rung is still totally undefined
(F(\bot) = \lambda n.\, \bot + 1 = \bot in the flat domain, since arithmetic
on \bot stays \bot), so the whole chain is
constantly \bot and its lub is \bot — the
everywhere-undefined function. The least fixed point automatically identifies "this program
computes nothing" with divergence. Had we chosen a greatest fixed point instead we might have
conjured a fictitious total function out of a loop that never returns — which is exactly why "least"
is the right choice: it never claims to know more than the computation actually produces.
Two classic slips. First, Kleene's construction needs continuity, not mere monotonicity:
the step F(\bigsqcup F^n(\bot)) = \bigsqcup F(F^n(\bot)) is precisely the
preservation-of-chain-lubs law, and a merely monotone F can fail it, so
\bigsqcup F^n(\bot) need not be a fixed point at all. (Knaster–Tarski rescues
existence with monotonicity alone — but only on a complete lattice, and it no longer hands you
the computable chain.) Second, a recursive equation can have many fixed points; the meaning is
always the least one. Grabbing an arbitrary solution can invent behaviour on inputs
where the real program diverges. When you hear "the function defined by this recursion", read "the least
fixed point of its functional".