A String Diagrammatic Axiomatisation of Finite-State Automata

TL;DR

This paper introduces a novel diagrammatic framework for finite-state automata, providing a complete algebraic axiomatization of language equivalence that simplifies the Kleene star operation.

Contribution

It presents a fully diagrammatic, equational approach to automata theory, with a finitary axiomatisation that reinterprets state transitions as string diagrams.

Findings

Complete axiomatization of language equivalence

Kleene star decomposed into primitive algebraic blocks

Finitary axiomatisation not possible in traditional syntax

Abstract

We develop a fully diagrammatic approach to the theory of finite-state automata, based on reinterpreting their usual state-transition graphical representation as a two-dimensional syntax of string diagrams. Moreover, we provide an equational theory that completely axiomatises language equivalence in this new setting. This theory has two notable features. First, the Kleene star is a derived concept, as it can be decomposed into more primitive algebraic blocks. Second, the proposed axiomatisation is finitary -- a result which is provably impossible to obtain for the one-dimensional syntax of regular expressions.