Algebras for an Endofunctor and Recursion

A monad algebra is a structure map $a:TA\to A$ constrained by two laws tied to the monad's unit and multiplication. Delete the laws (and the unit and multiplication with them), and what remains is an algebra for an endofunctor: any object with any map $F(A)\to A$. The definition looks weak, but its initial objects are the least fixed points of $F$, and the least fixed points of suitable functors are the natural numbers, lists, and trees of programming. Recursion over a datatype is one universal property applied repeatedly.¹

Fixed points of a functor

For a monotone function on a poset, a fixed point is an element with $f(x)=x$, and among the fixed points there may be a least one. Barr & Wells open Chapter 14 by asking what the analogue is for a functor $R:\mathcal{A}\to \mathcal{A}$, and the obvious candidate fails.²

Consider $R:\mathbf{Set}\to \mathbf{Set}$ with $R(S)=1+S$ (disjoint union with a one-point set), the functor whose fixed point ought to be the natural numbers. Demanding a set with $R(S)=S$ on the nose is hopeless: the equality would depend on the arbitrary choice of how disjoint unions are implemented. Weakening to isomorphism $S\cong 1+S$ fixes that but breaks leastness: every infinite set satisfies $S\cong 1+S$, and infinite sets have proper infinite subsets also satisfying it, so nothing is least in any containment sense. The resolution is to change the structure carrying the question.

Least reads a category as a generalized poset: in a poset-as-category, an initial object is a bottom element. A lemma justifies the definition by guaranteeing that initial algebras are fixed points.

Initial algebras also inherit the two other virtues of initial objects: they have no proper subobjects (the categorical residue of least), and they are unique up to unique isomorphism.⁵

The natural numbers as an initial algebra

Return to $R(S)=1+S$. The natural numbers carry the $R$-algebra structure

where $0$ picks out zero on the left summand and $s$ is the successor on the right. This algebra is initial: given any algebra $f:1+S\to S$, decompose $f$ into a chosen element $x_0=f(\ast )\in S$ and a map $t=f{|}_S:S\to S$; the unique homomorphism $h:\mathbb{N}\to S$ is defined by induction as

Commuting with the structure maps means this pair of equations, so $h$ is a homomorphism and is the only one.⁶ Definition by recursion — start at $x_0$, keep applying $t$ — is the universal property of an initial algebra, stated in $\mathbf{Set}$.

Folds

In functional programming the unique map out of an initial algebra is called a fold (or catamorphism). The data of an arbitrary algebra $f:F(S)\to S$ (one clause per summand of $F$) is the body of a structural recursion, and initiality says the recursion has exactly one solution. For the naturals, fold x0 t is the function iterating $t$ from $x_0$; for lists and trees (below), it is the usual fold over the datatype. Uniqueness is as useful as existence: two functions agreeing on the algebra clauses are equal, which is the fusion-style reasoning used to prove program transformations correct.

The step expose via $a^{-1}$ is licensed precisely by Lambek's lemma: the structure map of the initial algebra is invertible, so every element decomposes uniquely into a constructor applied to children.

Constructing initial algebras: the colimit chain

Existence of initial algebras needs a hypothesis on the functor. In $\mathbf{Set}$, the right condition is that the functor is finitary: every element of $R(S)$ comes from $R(S_0)$ for some finite subset $S_0\subseteq S$ — the functor's behavior is determined by what it does on finite sets.⁷ The functor $1+S$ is finitary; the powerset functor is not, since an infinite subset of $S$ is not contained in any finite subset.

The chain starts from nothing and applies the functor repeatedly; the colimit is the union if the maps are inclusions. Finitarity lets $R$ commute with this colimit, so that $R(Z)$ is the colimit of the shifted chain, which is canonically $Z$ again. For $R(S)=1+S$ the chain is

(with $n$ the $n$-fold sum $1+\cdots +1$ and the maps the sum injections), and the colimit is $\mathbb{N}$ with successor: the initial algebra built floor by floor, the $n$-th stage containing the numbers writable with at most $n$ constructor applications.

Inductive datatypes

The same construction interprets datatype declarations. A polynomial endofunctor is one built from constant functors and the identity by finite products and sums⁹; each summand is a constructor, each factor a field.

Barr & Wells work in the setting of a locos (a coherent, locally recursive category), where every polynomial endofunctor admits free algebras: the underlying functor from $(F:\mathcal{C})$ back to $\mathcal{C}$ has a left adjoint.¹⁰ The free algebra on the terminal object $1$ is the initial algebra, and for the tree functor $T(X)=D+X\times D\times X$ its structure map

reads as the two constructors: a leaf datum, or a datum with two subtrees. This is initial-algebra semantics: the meaning of a recursive datatype is the initial algebra of its signature functor.

Recursive categories and list objects

Recursion can also be internalized: made available inside a category rather than stated about it. For an object $A$ of a category with finite products, the endofunctor $A\times (-)$ has as algebras the $A$-actions$x:A\times X\to X$, forming a category $\mathbf{act}(A)$.

Write $\mathrm{rec}(A,B)=U_A(F_A(B))$, the free $A$-action on $B$. Its universal property: given any $t_0:B\to X$ and $t:A\times X\to X$, there is a unique $f:\mathrm{rec}(A,B)\to X$ compatible with both: a seed and a step determine a unique recursive map. In $\mathbf{Set}$, $\mathrm{rec}(A,B)\cong A^{\ast }\times B$: a list of $A$'s waiting to be consumed, together with a seed $b$. Two specializations matter:

• $\mathrm{rec}(A,1)=A^{\ast }$ is the list object on $A$, available in any recursive category, with well-defined head and tail operations.
• $\mathrm{rec}(1,1)$ is a natural numbers object: lists over a one-point alphabet are tallies.

The definition strengthens in stages: a locally recursive category has $\mathrm{rec}(A,B)\cong A^{\ast }\times B$ uniformly and all slices recursive, and a locos is additionally coherent. The stronger axioms yield a computability theorem: in a locos generated by decidable objects, every object is decidable, so the constructions of a locos never manufacture undecidable equality from decidable ingredients.¹²

State machines as algebras

An algebra for $A\times (-)$ is also exactly a deterministic transition system: $\delta :A\times C\to C$ takes an input letter and a state to a next state. Barr & Wells package this as categorical dynamics: an endofunctor $R$ whose algebra category has free objects is an input process, an $R$-algebra is an $R$-dynamic, and a machine is a dynamic with an initial state arrow $\tau :I\to C$ and an output arrow $\beta :C\to Y$.¹³ The free-monoid action ${\delta }^{\ast }:A^{\ast }\times C\to C$ extends $\delta$ to strings, recovering the classical automaton; reachability becomes $\tau$ factors through no proper subalgebra. Choosing a different functor (say $R(C)=C\times C$) gives machine notions with no classical counterpart.

Terminal coalgebras

Dualizing once more: a coalgebra for $F$ is a map $c:X\to F(X)$, and the terminal coalgebra is the greatest fixed point of $F$ (Lambek's lemma dualizes, so its structure map is again an isomorphism). Where the initial algebra of $1+A\times X$ is finite lists, the terminal coalgebra of $A\times X$ is infinite streams over $A$: a stream is observed by its head and tail, $⟨\mathrm{hd},\mathrm{tl}⟩:X\to A\times X$, and the unique map into the terminal coalgebra assigns to every state of any transition system the stream of outputs it generates. Folds consume finite structure; unfolds produce possibly-infinite structure. The pairing — datatypes as initial algebras, codatatypes as terminal coalgebras — organizes recursion and corecursion into one picture.

Scott domains by the same technique

Fixed points of functors also produce a model of the untyped lambda calculus, an object $D$ in a cartesian closed category with

so that every element of $D$ is simultaneously a function $D\to D$ and can be applied to itself. In $\mathbf{Set}$ this is impossible for cardinality reasons (except for $D=1$). Worse, the assignment $D\mapsto [D\to D]$ is not even a functor: an arrow $D\to E$ induces maps $[D\to D]\to [D\to E]$ and $[E\to D]\to [D\to D]$, but nothing between $[D\to D]$ and $[E\to E]$ — the exponential is contravariant in one variable and covariant in the other.¹⁴

The Smyth–Plotkin technique repairs functoriality by enriching. A Smyth–Plotkin category is a cartesian closed category whose hom-sets are posets, with composition and the exponential monotone, and with limits and colimits along countable chains that are order-isomorphisms on homs.¹⁵ From such a $\mathcal{C}$ build the category $\mathbf{LA}(\mathcal{C})$: same objects, but an arrow $A\to B$ is an adjoint pair $(f:A\to B,g:B\to A)$ with ${\mathrm{id}}_A\le g\circ f$ and $f\circ g\le {\mathrm{id}}_B$ — each arrow carries its own approximate inverse, and either component determines the other. A pair with $g\circ f=\mathrm{id}$ is a retract.

On $\mathbf{LA}(\mathcal{C})$ the exponential becomes an honest covariant functor: $F(B)=[B\to A]$ sends the pair $(f,g)$ to the pair $([g,A],[f,A])$, using $g$ in the contravariant slot and $f$ in the covariant one. The main theorem then supplies the fixed point.

The construction of the model runs the initial-algebra chain in this enriched setting. Start with an object $A\ne 1$ with $A\cong A\times A$ and a retract pair $A\to [A\to A]$; iterate $F$:

Let $B$ be the colimit. Because $[-,A]$ converts the colimit chain into a limit chain and back, $F$ preserves the colimit, so $F(B)\cong B$ — that is, $B\cong [B\to A]$, and a short calculation upgrades this to

The concrete instance takes $\mathcal{C}$ to be the category of $\omega$-complete partial orders and countable-sup-preserving maps, which is cartesian closed. For $A$, take a countable power of any nontrivial CPO $A_0$ with a bottom element (a countable power satisfies $A\cong A\times A$ by splitting a sequence into its even- and odd-indexed halves); the retract pair sends an element to the constant function at it, and a function to its value at $\perp$. The result is a Scott domain $D$ with $D\cong D\times D\cong [D\to D]$: a genuine model of self-application, constructed as a fixed point of a functor by the same chain that built the natural numbers.¹⁷

The same fixed-point chain, enriched over posets, builds the Scott domains on which the cartesian closed categories interpret the untyped lambda calculus.