Completeness for categories of generalized automata
Guido Boccali, Andrea Laretto, Fosco Loregian, Stefano Luneia
TL;DR
The paper develops a general, category-theoretic framework for $F$-automata (Mealy and Moore) in a generic category $\mathcal K$, showing these categories can be realized as strict 2-pullbacks in $\mathsf{Cat}$. It proves that if $F$ has a right adjoint $R$ and $\mathcal K$ is complete/cocomplete, then the automata categories inherit all limits and colimits from $\mathcal K$, with terminal objects constructed as $O_\infty$ via $\prod_{n\ge 0} R^n O$ (Moore) and $\prod_{n\ge 1} R^n O$ (Mealy) using Adámek’s theorem. A mechanized Agda formalization corroborates the synthetic approach, and the framework connects automata with behaviour via adjunctions, providing a scalable method to reason about generalized automata in abstract categorical settings. The results unify Mealy/Moore and $F$-automata under a 2-pullback perspective, offering tools for both theoretical analysis and practical formalization.
Abstract
We present a slick proof of completeness and cocompleteness for categories of $F$-automata, where the span of maps $E\leftarrow E\otimes I \to O$ that usually defines a deterministic automaton of input $I$ and output $O$ in a monoidal category $(\mathcal K,\otimes)$ is replaced by a span $E\leftarrow F E \to O$ for a generic endofunctor $F : \mathcal K\to \mathcal K$ of a generic category $\mathcal K$: these automata exist in their `Mealy' and `Moore' version and form categories $F\text{-}\mathsf{Mly}$ and $F\text{-}\mathsf{Mre}$; such categories can be presented as strict 2-pullbacks in $\mathsf{Cat}$ and whenever $F$ is a left adjoint, both $F\text{-}\mathsf{Mly}$ and $F\text{-}\mathsf{Mre}$ admit all limits and colimits that $\mathcal K$ admits. We mechanize some of of our main results using the proof assistant Agda and the library `agda-categories`.