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?

  • 1
    $\begingroup$ 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. :-) $\endgroup$ – David Richerby Oct 12 '15 at 9:55
  • $\begingroup$ @DavidRicherby Could you please define your use of "natural category," as I have not yet encountered that term. $\endgroup$ – user40709 Oct 13 '15 at 4:01
  • $\begingroup$ I just mean "form a category in a natural way." $\endgroup$ – David Richerby Oct 13 '15 at 7:03

As David Richerby stated, you can make a category out of just about anything, so of course automata in their various forms are included. Googling "category of automata" will return results and Joseph Goguen used a category of automata as an example in his Categorical Manifesto. (He also did research on such categories.) That such categories exist makes no suggestion that there is any special relationship between automata and categories.

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.

So, it turns out there are pretty profound connections between state machines and category theory. Of course, there are also profound connections between category theory and topology or order theory or metric spaces. This is part of what makes category theory so enticing.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy