James Worthington

Abstract: In this dissertation, we study automata, languages, and functions between automata which preserve the language accepted. We examine them from the perspectives of representation theory, category theory, and proof theory. A central theme is that these perspectives interact in many useful, interesting ways.

Let M be a monoid in a monoidal category. We view automata as objects of a category of representations of M, equipped with a start state and an observation function. If M is a monoid in Set, this view yields a generalization of the standard notion of a deterministic automaton. In this generalization, the inputs to an automaton are elements of an arbitrary monoid. Omitting the requirement that automata have start states yields categories with final objects. These final objects can be used to minimize deterministic automata.

Let K be a commutative semiring. To express nondeterminism in our framework, we must first take an algebraic detour and show that the category of K-semimodules and K-linear maps is a monoidal category. We then define K-algebras as monoids in this category. We call the corresponding automata K-linear automata. These automata are related to, but distinct from, weighted automata. A K-linear automaton with input K-algebra A defines an element of Lin(A,K). In certain cases, elements of Lin(A,K) correspond to K-linear extensions of formal power series.

In the K-linear case, there is an addition defined on both the states and the inputs. Addition of states can be used to represent nondeterminism. Addition of inputs is needed to define comultiplication. Comultiplication defines a K-algebra structure on Lin(A,K). That is, comultiplication of inputs corresponds to multiplication of “languages.” If multiplication and comultiplication satisfy certain “compatibility conditions,” the input elements form a structure known as a K-bialgebra. Part of this dissertation is the development of the numerous parallels between the theory of bialgebras and the theory of automata and formal languages. These parallels demonstrate that comultiplication is a “hidden parameter” in many standard constructions involving automata and formal languages.

In certain cases, a category of K-linear automata is related to a category of (generalized) deterministic automata by an adjunction. We show that the standard subset construction used to determinize automata can be generalized as a forgetful functor; determinization is essentially forgetting the K-semimodule structure on the states of a K-linear automaton.

Using this adjunction, we can construct a sequence of K-linear automata and morphisms thereof which witnesses the fact that two K-linear automata define the same element of Lin(A,K). With appropriate restrictions, this witness can be efficiently verified. Furthermore, we can use this witnessing sequence as the basis for a proof system for the equational theory of Kleene algebra. We also show that such proofs can be generated by a PSPACE transducer.

Finally, we discuss alternating automata in relation to our framework, and provide a determinizing functor.