---
title: Fixed Points in Cartesian Closed Categories
module: Cartesian Closed Categories and Typed Lambda Calculus
moduleNumber: 8
lessonNumber: 3
order: 803
summary: >
  The untyped lambda calculus has a fixed-point combinator; the typed calculus
  cannot, and Lawvere's fixed-point theorem explains why: any point-surjection
  onto an exponential forces every endomap to have a fixed point, which is the
  abstract form of Cantor's diagonal argument. Recursion is recovered instead by
  restricting to omega-complete partially ordered objects, where every
  continuous endomap has a least fixed point built by iterating from bottom.
  This gives While loops a semantics.
topics: [Cartesian Closed Categories and Typed Lambda Calculus]
sources:
  - book: Barr & Wells
    ref: "§6.6 Fixed points in cartesian closed categories"
draft: false
---

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

> **Worked example (Successor has no fixed point).** On the type $\mathbf{N}$ of
> natural numbers, the successor is the arrow $s : \mathbf{N} \to \mathbf{N}$
> with $s(n) = n + 1$. A fixed point would be an element $n : 1 \to \mathbf{N}$
> with $s(n) = n$, that is $n + 1 = n$, which no natural number satisfies. A
> typed combinator $Y : [\mathbf{N} \to \mathbf{N}] \to \mathbf{N}$ would produce
> $Y(s)$ with $s(Y(s)) = Y(s)$, a fixed point of $s$; since none exists, no such
> $Y$ can be a term of the typed calculus.

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 $\omega$-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

$$
\mathrm{eval} \circ \langle g \circ a,\; \mathrm{id}_A \rangle \;=\; f
\qquad\text{i.e.}\qquad g(a) = \lambda f .
$$

> **Theorem (Lawvere).** In a cartesian closed category, if some arrow
> $g : A \to [A \to B]$ is point-surjective, then every endomap $t : B \to B$
> has a fixed point: an arrow $s : 1 \to B$ with $t \circ s = s$.[^lawvere]

> **Proof.** Form the diagonal composite
>
> $$
> q \;=\; t \circ \mathrm{eval} \circ (g \times \mathrm{id}_A) \circ \Delta
> \;:\; A \longrightarrow B,
> $$
>
> in element notation $q(a) = t\bigl(g(a)(a)\bigr)$: feed each $a$ to the function
> that $a$ itself names, then apply $t$. Since $g$ is point-surjective, some point
> $p : 1 \to A$ names $q$, so $g(p) = \lambda q$. Set $s = q \circ p$. Then
>
> $$
> s \;=\; q(p) \;=\; t\bigl(g(p)(p)\bigr) \;=\; t\bigl(q(p)\bigr) \;=\; t(s),
> $$
>
> so $s$ is a fixed point of $t$. $\blacksquare$

$$
% caption: 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.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\node (a)  at (0,0) {$A$};
\node (aa) at (2.4,0) {$A \times A$};
\node (ea) at (5.6,0) {$B^A \times A$};
\node (b1) at (8.6,0) {$B$};
\node (b2) at (10.6,0) {$B$};
\draw[->, thick] (a) -- (aa) node[midway, above, black] {diag};
\draw[->, thick] (aa) -- (ea) node[midway, above, black] {$g \times A$};
\draw[->, thick] (ea) -- (b1) node[midway, above, black] {$\mathrm{ev}$};
\draw[->, thick] (b1) -- (b2) node[midway, above, black] {$t$};
\draw[->, acc, thick] (a) to[bend right=22] node[midway, below, black] {$q$} (b2);
\end{tikzpicture}
$$

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 $\mathcal{C} = \mathbf{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 \notin g(a)\}$ is
the transpose of $\neg \circ \mathrm{eval} \circ (g \times \mathrm{id}) \circ
\Delta$, and it differs from every $g(a)$ at the point $a$.

$$
% caption: 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.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\node at (1.2,3.1) {$a_1$};
\node at (2.4,3.1) {$a_2$};
\node at (3.6,3.1) {$a_3$};
\node at (4.8,3.1) {$a_4$};
\node at (-0.6,2.4) {$g(a_1)$};
\node at (-0.6,1.6) {$g(a_2)$};
\node at (-0.6,0.8) {$g(a_3)$};
\node at (-0.6,0.0) {$g(a_4)$};
\node[draw, acc, thick, inner sep=2pt] at (1.2,2.4) {$0$};
\node at (2.4,2.4) {$1$};
\node at (3.6,2.4) {$0$};
\node at (4.8,2.4) {$1$};
\node at (1.2,1.6) {$1$};
\node[draw, acc, thick, inner sep=2pt] at (2.4,1.6) {$1$};
\node at (3.6,1.6) {$0$};
\node at (4.8,1.6) {$0$};
\node at (1.2,0.8) {$0$};
\node at (2.4,0.8) {$0$};
\node[draw, acc, thick, inner sep=2pt] at (3.6,0.8) {$1$};
\node at (4.8,0.8) {$1$};
\node at (1.2,0.0) {$1$};
\node at (2.4,0.0) {$0$};
\node at (3.6,0.0) {$1$};
\node[draw, acc, thick, inner sep=2pt] at (4.8,0.0) {$0$};
\node at (-0.6,-1.1) {new row};
\node at (1.2,-1.1) {$1$};
\node at (2.4,-1.1) {$0$};
\node at (3.6,-1.1) {$0$};
\node at (4.8,-1.1) {$1$};
\draw[->, acc, thick] (5.5,-1.1) -- (6.9,-1.1);
\node[align=center, font=\footnotesize] at (8.3,-1.1) {equals no row:\\new row at $a_i$\\negates row $i$ at $a_i$};
\end{tikzpicture}
$$

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é.[^bw-fix] 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
$\omega$-CPOs of domain theory into an arbitrary cartesian closed category, by
ordering hom-sets rather than elements.

> **Definition (Partially ordered object).** An object $D$ of a cartesian closed
> category is **partially ordered** if every hom-set $\mathrm{Hom}(A, D)$
> carries a partial order such that $g \le h$ in $\mathrm{Hom}(A, D)$ implies
> $g \circ f \le h \circ f$ in $\mathrm{Hom}(B, D)$ for every $f : B \to A$.

> **Definition (Omega-CPO object).** A partially ordered object $D$ is an
> **$\omega$-complete partially ordered object** ($\omega$-CPO object) if every
> increasing countable chain $g_0 \le g_1 \le g_2 \le \cdots$ in each hom-set
> $\mathrm{Hom}(A, D)$ has a least upper bound. It is **strict** if there is an
> arrow $\bot : 1 \to D$ that is least: $\bot \circ \langle\rangle \le f$ for
> every $f : A \to D$.

> **Definition (Continuous arrow).** For $\omega$-CPO objects $D, D'$, an arrow
> $f : D \to D'$ is **$\omega$-continuous** if for every chain $g_0 \le g_1 \le
> \cdots$ of arrows $A \to D$ with supremum $g$, the arrow $f \circ g$ is the
> supremum of the chain $f \circ g_0 \le f \circ g_1 \le \cdots$.

Continuity implies monotonicity: $f \le g$ exactly when the chain $f, g, g,
\dots$ has supremum $g$, and a continuous arrow preserves that supremum. In
$\mathbf{Set}$ these definitions recover the ordinary $\omega$-CPOs, and the
category of $\omega$-CPOs with continuous maps is itself
[cartesian closed](/category-theory/cartesian-closed-lambda/cartesian-closed-categories).

### The least fixed point

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

> **Theorem (Least fixed point).** Let $D$ be a strict $\omega$-CPO object and
> $f : D \to D$ an $\omega$-continuous arrow. Then there is an element
> $\mathrm{fix}(f) : 1 \to D$ with $f \circ \mathrm{fix}(f) = \mathrm{fix}(f)$,
> and $\mathrm{fix}(f)$ is the least element of $D$ with this property.

> **Proof.** Since $\bot$ is least, $\bot \le f(\bot)$. Applying the monotone $f$
> repeatedly gives $f^n(\bot) \le f^{n+1}(\bot)$ by induction, hence an increasing
> chain
>
> $$
> \bot \;\le\; f(\bot) \;\le\; f^2(\bot) \;\le\; \cdots \;\le\; f^n(\bot) \;\le\; \cdots
> $$
>
> Define $\mathrm{fix}(f)$ as its least upper bound, which exists because $D$ is
> $\omega$-complete. Continuity of $f$ moves $f$ across the supremum:
>
> $$
> f\bigl(\mathrm{fix}(f)\bigr)
> = f\Bigl(\sup_n f^n(\bot)\Bigr)
> = \sup_n f^{n+1}(\bot)
> = \mathrm{fix}(f),
> $$
>
> the last step because dropping the first term of a chain does not change its
> supremum. Leastness: if $d : 1 \to D$ is any fixed point, then $\bot \le d$, and
> inductively $f^n(\bot) \le f^n(d) = d$, so the supremum is $\le d$.[^bw-lfp]
> $\blacksquare$
$$
% caption: The least fixed point is the supremum of the chain of iterates from bottom; here $d_0 = \bot$, each arrow applies $f$, and the limit $s$ satisfies $f(s) = s$.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\small]
\definecolor{acc}{HTML}{4A6FA5}
\draw[thick, black] (0,0) -- (10.4,0);
\node[circle, fill=black!55, inner sep=1.6pt, label=below:{$d_0$}] (d0) at (0.4,0) {};
\node[circle, fill=black!55, inner sep=1.6pt, label=below:{$d_1$}] (d1) at (2.4,0) {};
\node[circle, fill=black!55, inner sep=1.6pt, label=below:{$d_2$}] (d2) at (4.4,0) {};
\node[circle, fill=black!55, inner sep=1.6pt, label=below:{$d_3$}] (d3) at (6.0,0) {};
\node[circle, fill=black!55, inner sep=1.6pt, label=below:{$d_4$}] (d4) at (7.2,0) {};
\node[circle, fill=acc, inner sep=2.2pt, label=below:{$s$}] (s) at (9.4,0) {};
\draw[->, acc, thick] (d0) to[bend left=38] node[midway, above, black] {$f$} (d1);
\draw[->, acc, thick] (d1) to[bend left=38] node[midway, above, black] {$f$} (d2);
\draw[->, acc, thick] (d2) to[bend left=38] node[midway, above, black] {$f$} (d3);
\draw[->, acc, thick] (d3) to[bend left=38] node[midway, above, black] {$f$} (d4);
\node at (8.2,0.42) {$\cdots$};
\draw[->, acc, thick] (s) to[out=115, in=65, looseness=8] node[midway, above, black] {$f$} (s);
\end{tikzpicture}
$$

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](/category-theory/monads-algebras/algebras-for-endofunctors),
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
$\mathbf{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.[^bw-sem]

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

> **Definition (Flat CPO).** For an object $D$, the object $D_\bot = D +
> \{\bot\}$ ordered by $\bot \le d$ for every $d \in D$, with no other strict
> comparabilities, is the **flat CPO** on $D$.

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

$$
f \le g
\quad\Longleftrightarrow\quad
g \text{ is defined wherever } f \text{ is, and agrees with } f \text{ there.}
$$

Every continuous endomap of $[A \to D_\bot]$ 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 $\Phi(f) = (p \Rightarrow q;\,
H(f))$ is an endomap of $[A \to D_\bot]$; when $H$ is continuous, so is $\Phi$,
and $\mathrm{fix}(\Phi)$ interprets the program. The iterates from $\bot$ are
the finite unrollings of the loop. With $H(f) = g \circ f \circ h$:

```algorithm
caption: $\textsc{Unroll}(p, q, g, h, x)$ — the iterates of $\Phi$ from $\bot$ as nested conditionals
if $p(x)$ then
  output $q(x)$
else if $p(h(x))$ then
  output $g(q(h(x)))$
else if $p(h(h(x)))$ then
  output $g(g(q(h(h(x)))))$
$\vdots$
else if $p(h^n(x))$ then
  output $g^n(q(h^n(x)))$
$\vdots$
```

The $n$-th iterate $\Phi^n(\bot)$ 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 $\bot$ at $x$ and so is the fixed
point: nontermination is denoted by $\bot$, 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
> $$
> \mathrm{fact}(n) = \text{if } n = 0 \text{ then } 1 \text{ else } n \cdot \mathrm{fact}(n - 1)
> $$
> as the least fixed point of the operator $\Phi$ on $[\mathbf{N} \to
> \mathbf{N}_\bot]$ with $\Phi(f)(n) = 1$ if $n = 0$ and $\Phi(f)(n) = n \cdot
> f(n - 1)$ otherwise. Iterate from $\bot$, the everywhere-undefined partial
> function:
> - $\Phi^0(\bot) = \bot$ is undefined at every $n$.
> - $\Phi^1(\bot)$ is defined only at $0$, where it returns $1$; at $n \ge 1$ it
>   calls $\bot(n - 1) = \bot$ and stays undefined.
> - $\Phi^2(\bot)$ is defined on $\{0, 1\}$ with values $0! = 1$ and $1! = 1$.
> - $\Phi^{k}(\bot)$ 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
> $$
> \mathrm{fix}(\Phi)(n) = n! \quad\text{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) = \Gamma \circ \langle E_1(f), \dots, E_n(f)
\rangle$ for simpler continuous forms $E_i$) all yield continuous operators, so
every loop built from them has a semantics.[^bw-sem]

| Setting | Fixed points available | Cost |
| --- | --- | --- |
| untyped lambda calculus | every term, via $Y$ | no types; $Y(\mathrm{id})$ is the nonterminating loop |
| typed lambda calculus / bare CCC | none guaranteed; all endomaps only if degenerate | no general recursion |
| CCC with strict $\omega$-CPO objects | every continuous endomap of an ordered object | recursion only at ordered (arrow) types; $\bot$ 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.

$$
% caption: 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.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\footnotesize,
  c/.style={draw, minimum width=25mm, minimum height=8mm, align=center}]
\definecolor{acc}{HTML}{4A6FA5}
\node[c] (cat) at (0,0) {categories};
\node[c] (fun) at (-3.4,1.5) {functors};
\node[c] (up)  at (3.4,1.5) {universal properties};
\node[c] (nat) at (-3.4,3.0) {naturality};
\node[c] (lim) at (3.4,3.0) {limits and colimits};
\node[c] (yon) at (-3.4,4.5) {Yoneda lemma};
\node[c] (adj) at (0,4.5) {adjunctions};
\node[c] (rapl) at (3.9,6.0) {adjoints preserve limits};
\node[c] (mon) at (-3.4,6.0) {monads};
\node[c] (ccc) at (0,6.0) {cartesian closed};
\node[c, draw=acc, text=acc, thick] (lam) at (0,7.5) {typed lambda calculus};
\node[c] (rec) at (3.6,7.5) {recursion};
\draw[->, thick] (cat) -- (fun);
\draw[->, thick] (cat) -- (up);
\draw[->, thick] (fun) -- (nat);
\draw[->, thick] (up) -- (lim);
\draw[->, thick] (nat) -- (yon);
\draw[->, thick] (nat) -- (adj);
\draw[->, thick] (yon) -- (adj);
\draw[->, thick] (lim) -- (rapl);
\draw[->, thick] (adj) -- (rapl);
\draw[->, thick] (adj) -- (mon);
\draw[->, thick] (adj) -- (ccc);
\draw[->, thick] (lim) -- (ccc);
\draw[->, acc, thick] (ccc) -- (lam);
\draw[->, acc, thick] (ccc) -- (rec);
\end{tikzpicture}
$$

Read bottom to top, a
[category](/category-theory/foundations/what-is-a-category) is objects and
arrows under composition;
[universal properties](/category-theory/universal-properties/universal-properties)
characterize constructions up to unique isomorphism;
[functors](/category-theory/foundations/functors) and
[natural transformations](/category-theory/foundations/natural-transformations)
compare categories and functors; the
[Yoneda lemma](/category-theory/representables-yoneda/yoneda-lemma) says an
object is determined by its arrows in;
[limits](/category-theory/limits-colimits/limits) and
[colimits](/category-theory/limits-colimits/colimits) build objects from
diagrams; [adjunctions](/category-theory/adjunctions/adjunctions) pair the
building with the forgetting, and
[right adjoints preserve limits](/category-theory/adjoints-limits/adjoints-preserve-limits).
From adjunctions two roads lead into computing:
[monads](/category-theory/monads-algebras/monads) and their
[Kleisli categories](/category-theory/monads-algebras/kleisli-and-programming)
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.

[^bw-fix]: **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é).
[^lawvere]: 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](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.
[^bw-lfp]: **Barr & Wells**, §6.6.2–6.6.3 — partially ordered objects, $\omega$-CPO objects, strictness, $\omega$-continuous arrows, and the least-fixed-point proposition with the iteration-from-bottom proof.
[^bw-sem]: **Barr & Wells**, §6.6.4 — application to programs: fixed points at arrow types rather than data types, the flat CPO $D_\bot$, the extension-of-domain order on $[A \to D_\bot]$, the infinite unrolling of $p \Rightarrow q; H(f)$, and the continuity of Backus's functional forms.