Complete Compositional Syntax for Finite Transducers on Finite and Bi-Infinite Words

TL;DR

This paper introduces a unified, compositional diagrammatic syntax for finite transducers that enables formal reasoning about automata, transition systems, and subshifts, with proven completeness of the associated equational theory.

Contribution

It develops a novel diagrammatic syntax with sound rewriting rules for finite transducers, providing a unified framework for automata and related systems.

Findings

Sound rewriting rules enable formal reasoning.

Completeness of the equational theory is proven.

Framework unifies automata, transition systems, and subshifts.

Abstract

Minimizing finite automata, proving trace equivalence of labelled transition systems or representing sofic subshifts involve very similar arguments, which suggests the possibility of a unified formalism. We propose finite states non-deterministic transducer as a lingua franca for automata theory, transition systems, and sofic subshifts. We introduce a compositional diagrammatical syntax for transducers in form of string diagrams interpreted as relations. This syntax comes with sound rewriting rules allowing diagrammatical reasoning. Our main result is the completeness of our equational theory, ensuring that language-equivalence, trace-equivalence, or subshift equivalence can always be proved using our rewriting rules.