nLab algebraically compact category

Idea

A category is called algebraically compact if for every endofunctor on it the respective initial algebra coincides with the final coalgebra.

Under categorical semantics of programming languages this condition ensures the existence of inductive-recursive types (e.g. Zamdzhiev 20). For that, recall:

In computer science, a data type is often defined by an isomorphism of types $X\cong T(X)$ for some construction $T$ (an endofunctor on the category of types), namely as a fixed point of an endofunctor. (For example, the natural numbers may be defined – see there – as being fixed $\mathbb{N} \cong \mathbb{N} + 1$ by the operation of disjoint union with a singleton.) These are inductive types.

However, in a language with general recursion (including partial recursive functions), the data types have properties in addition to as the usual inductive ones, which allow coinductive reasoning. For example, in a lazy language such as Haskell, there is an infinity element in $\mathbb{N}$, which is a fixed point for the successor operation.

In general, it is common to allow the construction $T$ to be mixed-variance. For example, $X\cong (X\to X)$ is a recursive data type whose inhabitants are expressions of the untyped lambda calculus. Thus recursive data types are a generalization of reflexive objects. On the semantic side, recursive data types are sometimes called “recursive domain equations”.

Definition

Definition

A category is algebraically complete if every endofunctor $F$ has an initial algebra $F(A) \to A$. A category is algebraically cocomplete if every endofunctor $F$ has a final coalgebra $Z\to F(Z)$.

By Lambek's lemma, an initial algebra is an isomorphism, and so is a final coalgebra, thus they can be regarded as coalgebras and algebras respectively. This gives rise to a canonical morphism from the initial algebra to the final coalgebra, $A\to Z$.

An algebraically complete and cocomplete category $C$ is algebraically compact if this canonical morphism from the initial algebra to the final coalgebra is an isomorphism.

Remark

In classical set theory, very few categories are algebraically compact. Thus it is common to restrict attention to certain endofunctors. One might then say that this class of endofunctors is algebraically compact. A leading example is where $C$ is $V$-enriched, in which case we might restrict attention to $V$-endofunctors. For example, the $\mathbf{cpo}$-enriched category of pointed cpo‘s and strict maps is $\mathbf{cpo}$-algebraically compact.

Recall that a cpo is an $\omega$-chain-complete partial order. The category $\mathbf{cpo}$ comprises cpo’s and continuous maps. A cpo is pointed if it has a bottom element, and a continuous map is strict if it preserves the bottom elements.

Proposition

The category $\mathbf{cpo}_{\bot!}$ of pointed cpo‘s and strict continuous maps is algebraically compact as a $\mathbf{cpo}$-enriched category.

Proof sketch.

In a poset-enriched category, an embedding-projection pair is a retract $e:X \to Y$, $p: Y\to X$ such that $p e=id$ and $e p\leq id$.

Let $F:\mathbf{cpo}_{\bot!}\to \mathbf{cpo}_{\bot!}$ be an endofunctor. Consider the chain of projections

$$1 \xleftarrow{p} F(1) \xleftarrow{F(p)} F(F(1)) \xleftarrow{F(F(p))} \dots$$

We consider the limit $D$ of this sequence of projections as a poset, which is already a pointed cpo.

Because $1$ is also an initial object, each of these projections in the chain forms an embedding-projection pair, and we have a sequence

$$1 \xrightarrow{e} F(1) \xrightarrow{F(e)} F(F(1)) \xrightarrow{F(F(e))}\dots$$

One can show that $D$ can also be regarded as a colimit of this sequence of embeddings.

Now we use the universal properties of limits and colimits to show that $D$ is an initial algebra and final coalgebra of $F$.

Mixed variance domain equations and minimal solutions

Let $T:C^{op}\times C\to C$ be a bifunctor. A solution for $T$ is an object $X$ together with an isomorphism

$$a:X \cong T(X,X)$$

In general there may be many solutions. One approach to comparing them is via retractions. If an object $Y$ is a retract of $X$, and $Y$ forms a solution $b:Y\cong T(Y,Y)$, then we can ask that the retraction respects the solution, i.e.

$$\array{& Y & \overset{i}\rightarrow & X & \\ b & \downarrow &&\downarrow & a&\\ &T(Y,Y) & \underset{T(r,i)}\rightarrow& T(X,X) & \\ } \quad and \quad \array{& X & \overset{r}\rightarrow & Y & \\ a & \downarrow &&\downarrow & b&\\ &T(X,X) & \underset{T(i,r)}\rightarrow& T(Y,Y) & \\ }$$

Proposition (Freyd)

If $C$ and $D$ are algebraically compact, so is $C\times D$. If $C$ is algebraically compact, so is the dual category $C^{op}$.

As a result of this proposition, we solve a mixed-variance domain equation $X \cong T(X,X)$ for $T:C^{op}\times C\to C$ on an algebraically compact category by considering the initial algebra / final coalgebra of the endofunctor $\bar{T}:C^{op}\times C\to C^{op}\times C$ given by $\bar{T}(X,Y)=(T(Y,X),T(X,Y))$.

Proposition (Freyd, Fiore)

For a bifunctor $T:C^{op}\times C\to C$ on an algebraically compact category, the solution from the initial algebra / final coalgebra is minimal in the sense that it is uniquely a retract of every solution.

References

The notion is due to:

• Peter Freyd, Algebraically complete categories, Category Theory in Como, 1990 (dpi:10.1007/BFb0084215)

Barr proposed to look at certain functors as algebraically compact, and gave basic facts about building algebraically compact functors and numerous examples. Fiore and Plotkin looked enriched functors and proved “adequacy” results about data types in programming languages.

• Michael Barr, Algebraically compact functors, Journal of Pure and Applied Algebra Volume 82, Issue 3, 26 October 1992, Pages 211-231 (doi:10.1016/0022-4049(92)90169-G)

• Marcelo Fiore. Axiomatic domain theory in categories of partial maps. CUP 1996.

• Marcelo Fiore and Gordon Plotkin. An axiomatization of computationally adequate domain theoretic models of FPC. In Proc. LICS, 1994. pdf.

Pitts gives a survey and discussion, together with further reasoning principles.

• Andrew Pitts, Relational properties of domains, Information and Computation, 1996. pdf.

See also:

• Vladimir Zamdzhiev, Reflecting Algebraically Compact Functors, EPTCS 323, 2020, pp. 15-23 (arXiv:1906.09649)