# DFAs as Categories

I've been recently investigating metacategories (arrows and objects) alongside Automata theory and noticed that a category is a sort of parent container for DFAs, which are just a specific type of function over sets.

If the relationship between automata and categories is significant, does that mean an automata could encode type information in addition to its accepting duties?

• Note that you can form a category out of almost anything, so the mere existence of a natural category of DFAs isn't necessarily significant. But I'll leave answering your question to people who actually know something about categories. :-) – David Richerby Oct 12 '15 at 9:55
• @DavidRicherby Could you please define your use of "natural category," as I have not yet encountered that term. – user40709 Oct 13 '15 at 4:01
• I just mean "form a category in a natural way." – David Richerby Oct 13 '15 at 7:03

However... (one type of) a deterministic automaton is just a monoid action. You have your state space $S$ and a monoid of inputs $M$ (often the free monoid on some finite set, i.e. strings) and your transition function $t : M \times S \to S$. We want our $t$ to be equivariant, i.e. it respects the monoid structure on $M$. Formally, $t(1, s) = s$ and $t(mn, s) = t(n, t(m, s))$.
There's a particularly nice and fairly important categorical reformulation of this. We can view a monoid as a one object category, call it $C_M$. The object isn't too important so let's just call it $\star$. The only hom set is $Hom(\star, \star) = M$ and composition is just the multiplication of the monoid. A monoid action is then just a functor $F : C_M^{op} \to Set$. $F(\star) = S$ and $F(m)(s) = t(m, s)$. The functor laws guarantee equivariance.
Once we have this perspective, there are many directions we can go with it. We can change $Set$ to $Poset$ and talk about state machines with monotonically increasing states. (Or, you know, if we want finite state machines, use $FinSet$.) We can generalize $C_M$ from a one object category to an arbitrary (small) category and have different state spaces as we transition which I think may be similar to what you were thinking about "types". We can recognize that we immediately have an entire category of state machines over $M$, namely the functor category $[C_M^{op}, Set]$. We can further recognize that this is a presheaf category, a type of category of foundational importance in category theory. Presheaf categories also have a lot of structure for free; in particular, they're toposes so you can interpret a dependently type lambda calculus into them. This example is also an example of a Lawvere theory.