Fixed Points in Cartesian Closed Categories

The untyped lambda calculus owes much of its interest to the fixed-point combinator $Y$ , a term satisfying $x^{‵} (Y^{‵} x) = Y^{‵} x$ : for every term $x$ , the term $Y^{‵} x$ is a fixed point of $x$ . No such combinator can exist in the typed calculus. If there is a type of natural numbers, the successor function is a term of type $[N \to N]$ , and successor has no fixed point.¹

Yet recursion needs fixed points. A recursive program

f = p \Rightarrow q; H (f)

(read: if $p$ then $q$ else $H (f)$ , in Backus's notation) defines $f$ as a fixed point of the operator $f \mapsto (p \Rightarrow q; H (f))$ . Without some fixed-point principle, a typed language cannot interpret its own While loops. Two results bound the situation. Lawvere's theorem shows that too many fixed points collapse the category; a construction on the $ω$ -complete partially ordered objects supplies enough.

Lawvere's fixed-point theorem

The obstruction to a typed $Y$ is a theorem about cartesian closed categories, not a defect of syntax. Call an arrow $g : A \to [A \to B]$ point-surjective if every arrow $f : A \to B$ is named by some point of $A$ : there exists $a : 1 \to A$ with

eval \circ ⟨ g \circ a, id_{A} ⟩ = f i.e. g (a) = λ f .

Lawvere's diagonal composite: duplicate the argument, let

g

name a function, evaluate it on the copy, and apply

t

; point-surjectivity of

g

then forces

t

to have a fixed point.

The theorem reads in both directions:

Forward. If a model of the typed lambda calculus contains a type $A$ with a point-surjection $A \to [A \to A]$ — a type that can enumerate its own endofunctions, as the untyped calculus does — then every endomap of $A$ has a fixed point. This is how models of the untyped calculus must look.
Contrapositive. If some endomap of $B$ has no fixed point, then no arrow $A \to [A \to B]$ is point-surjective, for any $A$ . One fixed-point-free map rules out every enumeration.

The diagonal arguments

The contrapositive is the abstract form of the classical diagonal arguments. Take $C = Set$ and $B = {0, 1}$ . Negation $\neg : B \to B$ has no fixed point, so no function $g : A \to [A \to {0, 1}]$ is surjective. Since functions $A \to {0, 1}$ are exactly subsets of $A$ , this is Cantor's theorem: no set surjects onto its own power set. The proof extracted from Lawvere's composite is precisely Cantor's: the set ${a : a \in / g (a)}$ is the transpose of $\neg \circ eval \circ (g \times id) \circ Δ$ , and it differs from every $g (a)$ at the point $a$ .

Cantor's diagonal as the contrapositive of Lawvere: list the functions

g (a_{i})

as rows, flip the diagonal, and the flipped row differs from every listed row, so

g

misses it.

The same skeleton yields Russell's paradox (take $A$ the universe of sets), Gödel-style self-reference (take $g$ an enumeration of definable predicates), and Tarski's undefinability theorem. In each case a diagonal composite plus one fixed-point-free endomap contradicts surjectivity.

For semantics this is a no-go theorem. A model of a programming language would ideally provide three things: cartesian closure, a fixed point for every endomap of every type (general recursion), and non-degenerate data types (some type with two distinct points, such as booleans). Lawvere's theorem shows these are inconsistent: if booleans exist, negation has no fixed point. Requiring fixed points for all endomaps of all objects collapses the category to triviality, and Barr & Wells note the sharpened forms of this inconsistency due to Huwig and Poigné.¹ Fixed points must therefore be demanded only for some endomaps of some objects: enough to interpret loops, few enough to avoid collapse.

Ordered objects in a cartesian closed category

The objects that carry fixed points are those with enough order structure to support a limiting process. The definitions internalize the $ω$ -CPOs of domain theory into an arbitrary cartesian closed category, by ordering hom-sets rather than elements.

Continuity implies monotonicity: $f \leq g$ exactly when the chain $f, g, g, \dots$ has supremum $g$ , and a continuous arrow preserves that supremum. In $Set$ these definitions recover the ordinary $ω$ -CPOs, and the category of $ω$ -CPOs with continuous maps is itself cartesian closed.

The least fixed point

On strict $ω$ -CPO objects, continuous endomaps do have fixed points, and the construction is iteration from the bottom.

The least fixed point is the supremum of the chain of iterates from bottom; here

d_{0} = ⊥

, each arrow applies

f

, and the limit

s

satisfies

f (s) = s

The chain $d_{n + 1} = f (d_{n})$ climbs by successive approximation and the fixed point is its limit. The loop on $s$ records the defining equation $f (s) = s$ . This is the same construction as the initial algebra built by iterating an endofunctor, one level down: there the chain lives in a category of objects, here in a poset of approximants.

Semantics of recursive programs

The fixed points needed for programming are not on the base data types. On $N$ with its usual order, squaring is not even monotone, and successor has no fixed point at all; nothing in the theory applies to them, and nothing should. The objects that need fixed points are the arrow types: the operator $f \mapsto (p \Rightarrow q; H (f))$ is an endomap of a function object, and it is there that the order structure lives.⁴

The order is by definedness. Given any object $D$ of data (no order assumed), adjoin a fresh bottom element:

A flat order is trivially $ω$ -complete: an increasing chain is either constantly $⊥$ or eventually a single constant. An arrow $A \to D_{⊥}$ is a partial arrow $A \to D$ : it sends the arguments outside its domain of definition to $⊥$ . Under mild assumptions on the category (true in $Set$ ), the exponential $[A \to D_{⊥}]$ is again an $ω$ -CPO object, because a chain of arrows $B \to [A \to D_{⊥}]$ transposes to a chain $B \times A \to D_{⊥}$ , which has a supremum by assumption. The induced order on $[A \to D_{⊥}]$ is extension of domain:

f \leq g ⟺ g is defined wherever f is, and agrees with f there.

Every continuous endomap of $[A \to D_{⊥}]$ therefore has a least fixed point, and this is all a recursive definition requires. For the Backus form $f = p \Rightarrow q; H (f)$ , the operator $Φ (f) = (p \Rightarrow q; H (f))$ is an endomap of $[A \to D_{⊥}]$ ; when $H$ is continuous, so is $Φ$ , and $fix (Φ)$ interprets the program. The iterates from $⊥$ are the finite unrollings of the loop. With $H (f) = g \circ f \circ h$ :

Algorithm:

\textsc{Unroll}(p, q, g, h, x)

— the iterates of

\Phi

from

\bot

as nested conditionals

1
if $p(x)$ then
2
output $q(x)$
3
else if $p(h(x))$ then
4
output $g(q(h(x)))$
5
else if $p(h(h(x)))$ then
6
output $g(g(q(h(h(x)))))$
7
$\vdots$
8
else if $p(h^n(x))$ then
9
output $g^n(q(h^n(x)))$
10
$\vdots$

The $n$ -th iterate $Φ^{n} (⊥)$ is the partial function defined on precisely those inputs that exit the loop within $n$ tests; each iterate extends the domain of the last and never revises a value already produced, which is monotonicity in the extension order; and the supremum — the program's meaning — is defined on exactly the inputs for which the loop terminates. If the guard never succeeds on $x$ , every iterate is $⊥$ at $x$ and so is the fixed point: nontermination is denoted by $⊥$ , not by an error. The fixed point is syntactic existence, not a termination guarantee — the least fixed point of the identity operator is the everywhere-undefined function, the denotation of the canonical infinite loop.

Worked example (The factorial as a least fixed point). Interpret the recursive definition

fact (n) = if n = 0 then 1 else n \cdot fact (n - 1)

as the least fixed point of the operator $Φ$ on $[N \to N_{⊥}]$ with $Φ (f) (n) = 1$ if $n = 0$ and $Φ (f) (n) = n \cdot f (n - 1)$ otherwise. Iterate from $⊥$ , the everywhere-undefined partial function:

$Φ^{0} (⊥) = ⊥$ is undefined at every $n$ .
$Φ^{1} (⊥)$ is defined only at $0$ , where it returns $1$ ; at $n \geq 1$ it calls $⊥ (n - 1) = ⊥$ and stays undefined.
$Φ^{2} (⊥)$ is defined on ${0, 1}$ with values $0! = 1$ and $1! = 1$ .
$Φ^{k} (⊥)$ is defined on ${0, 1, \dots, k - 1}$ , returning $n!$ there.

Each iterate extends the previous one by one input and revises no value already produced, so the chain increases in the extension order. Its supremum

fix (Φ) (n) = n! for every n

is total: the factorial. The $k$ -th iterate is the program unrolled $k$ times, defined on exactly the inputs whose recursion bottoms out within $k$ calls.

Continuity of $H$ must be checked, once, for the constructors of the language: constants, projection onto a component of a tuple of functions, and composition with fixed functions ( $H (f) = Γ \circ ⟨ E_{1} (f), \dots, E_{n} (f)⟩$ for simpler continuous forms $E_{i}$ ) all yield continuous operators, so every loop built from them has a semantics.⁴

Setting	Fixed points available	Cost
untyped lambda calculus	every term, via $Y$	no types; $Y (id)$ is the nonterminating loop
typed lambda calculus / bare CCC	none guaranteed; all endomaps only if degenerate	no general recursion
CCC with strict $ω$ -CPO objects	every continuous endomap of an ordered object	recursion only at ordered (arrow) types; $⊥$ enters the semantics

Concept dependencies

A cartesian closed category and the typed lambda calculus present the same theory, with recursion supplied by order-theoretic fixed points and bounded by Lawvere's diagonal theorem.

The course's concept dependencies: each result stands on the ones below it, and the three readings of a CCC — functions, logic, programs — meet in this module.

Read bottom to top, a category is objects and arrows under composition; universal properties characterize constructions up to unique isomorphism; functors and natural transformations compare categories and functors; the Yoneda lemma says an object is determined by its arrows in; limits and colimits build objects from diagrams; adjunctions pair the building with the forgetting, and right adjoints preserve limits. From adjunctions two roads lead into computing: monads and their Kleisli categories model effects, while the product-exponential adjunction of a cartesian closed category models functions themselves — and, by this module's equivalence, is the typed lambda calculus. Lawvere's theorem bounds this world by a diagonal argument, and domain-theoretic order structure supplies the recursion a programming language needs.

Barr & Wells, Category Theory for Computing Science, §6.6.1 — the untyped fixed-point combinator $Y$ , the impossibility of typing it (successor has no fixed point), the Backus form $p \Rightarrow q; H (f)$ , and the inconsistency of all-objects fixed points with other desirable assumptions (citing Huwig and Poigné). ↩ ↩²
F. W. Lawvere, Diagonal arguments and cartesian closed categories (1969), reprinted as TAC Reprints no. 15 — http://www.tac.mta.ca/tac/reprints/articles/15/tr15abs.html. The theorem, its proof by the diagonal composite, and the derivation of Cantor, Russell, and Gödel-style arguments as contrapositives. ↩
Barr & Wells, §6.6.2–6.6.3 — partially ordered objects, $ω$ -CPO objects, strictness, $ω$ -continuous arrows, and the least-fixed-point proposition with the iteration-from-bottom proof. ↩
Barr & Wells, §6.6.4 — application to programs: fixed points at arrow types rather than data types, the flat CPO $D_{⊥}$ , the extension-of-domain order on $[A \to D_{⊥}]$ , the infinite unrolling of $p \Rightarrow q; H (f)$ , and the continuity of Backus's functional forms. ↩ ↩²