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

TL;DR

The paper addresses unifying automata, transition systems, and symbolic dynamics through finite-state relational transducers expressed with a diagrammatic, compositional syntax. It develops a sound and (partially) complete equational theory for transducers acting on finite words, and extends the framework to bi-infinite words via ${\bb Z}$-transducers and sofic subshifts, establishing a correspondence between sofic relations and ${\bb Z}$-transducers. Key contributions include a diagrammatic representation language with a simulation principle that yields completeness in the finite case, a bi-infinite extension with adapted simulation principles, and a canonical presentation theory for sofic subshifts (pruned rooted right-resolving presentations). The approach enables compositional proofs of language-, trace-, and subshift-equivalence and opens avenues for probabilistic or quantum generalizations by changing the base category. Overall, the work provides a unified, diagrammatic toolkit for reasoning about automata, transition systems, and symbolic dynamics with potential broad impact on theory and applications.

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.

Figures (29)

• Figure 1: Equations for the Cup and Cap.
• Figure 2: Equations for a Feedback Category.
• Figure 3: Equations for Faithfully Embedding FinRel.
• Figure 4: Simulation Principle for Finite Words.
• Figure 5: Sliding.

Theorems & Definitions (70)

• Definition 3.1: Transducer
• Proposition 3.1
• Proposition 3.2: Proved in \ref{['app:transducer-fin']}
• Proposition 3.3: Quasi-Normal Form
• proof
• Theorem 3.4: Universality
• proof
• Theorem 3.5: Completeness
• Definition 3.2: Determinization
• Proposition 3.6