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

Titouan Carette, Marc de Visme, Vivien Ducros, Victor Lutfalla, Etienne Moutot

► To cite this version:

Titouan Carette, Marc de Visme, Vivien Ducros, Victor Lutfalla, Etienne Moutot. Complete Compositional Syntax for Finite Transducers on Finite and Bi-Infinite Words. 2025. hal-05390813

HAL Id: hal-05390813

https://hal.science/hal-05390813v1

Preprint submitted on 1 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Complete Compositional Syntax for Finite Transducers on
Finite and Bi-Infinite Words

Titouan Carette¹, Marc de Visme², Vivien Ducros³, Victor Lutfalla*⁴, and Etienne Moutot†⁵

¹titouan.carette@polytechnique.edu, LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, 91120 Palaiseau, France

²marc.de-visme@inria.fr, Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles, 91190 Gif-sur-Yvette, France

³vivien.ducros@ens-paris-saclay.fr, ENS Paris-Saclay, Université Paris-Saclay, 91190 Gif-sur-Yvette, France

⁴victor.lutfalla@math.cnrs.fr, Aix-Marseille Univ, CNRS, I2M, Marseille, France

⁵etienne.moutot@math.cnrs.fr, CNRS, I2M, Aix-Marseille Université, Marseille, France

February 10, 2025

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.

# 1 Introduction

The interest of category theory for computer science is to provide an abstract language suitable to describe computational structures in their most general form, allowing to clarify connections between similar constructions appearing in different fields, sometimes seemingly unrelated. One of those abstract ideas, ubiquitous in computer science, is a machine interacting with its environment by updating an internal set of states. Most computational models fit this description, the paradigmatic example being Turing machines. Such machines interact with their environment via inputs and outputs, thus their behavior can be described as the set of all possible input/output pairs, which are interpreted as a relation between a (possibly infinite) sequence of input events and another sequence of output events. When constraining the set of internal states of a machine to be finite, one enforces interesting

<footnote>*Partially supported by ANR ALARICE (ANR-24-CE48-7504)</footnote>

<footnote>†Partially supported by ANR IZES (ANR-22-CE40-0011)</footnote>
mathematical properties on the set of admissible behaviors, as they must be definable by finite means, in a certain way.

Let us take three examples of models exhibiting this kind of behavior. The most famous is the finite automaton [Sip97; HMU07], which only takes finite sequences of input events and evaluates if those sequences are valid or not. The behavior then coincides with the language recognized by the automaton, and the possible behaviors are exactly the regular languages. Perhaps more aligned with the interacting machine point of view, a Labelled Transition System (LTS) performs a transition (depending on an input event and its current state) that can produce an output event. In the LTS literature, we usually talk about the trace of the system to design its behavior. The last model we will mention is perhaps less known by the computer science community and comes from dynamical systems. A discrete-time dynamical system is a set $X$ equipped with an update function $f: X \to X$ implementing the dynamic. Symbolic dynamics is the study of coarse-grained dynamical systems when $X$ is partitioned into subsets indexed by finitely many symbols [LM21]. One can learn a lot on the original dynamical system by studying the sequences of symbols induced by the evolution $f$. Those sequences correspond to our general notion of behavior, and the ones "definable by finite means" correspond to a set of sequences known as sofic subshifts. The fact that similar mathematical methods, mostly involving regular languages, can be employed to handle those three cases is folklore. However, to our knowledge, no framework exists to formally unify those three models.

We propose finite relational transducers as general objects subsuming automata, LTS, and symbolic dynamical systems. The originality of our approach is to embrace a fully relational point of view, considering relations and not functions as more fundamental. In other words, we will consider non-determinism to be more natural, and see determinism as an interesting special case. This stance will lead us to present generalizations of well-known models that might feel unfamiliar, typically in the case of non-deterministic symbolic dynamical systems. Still, we believe that the relational setting is the right place to understand clearly how the various models we present are linked. Furthermore, the relational point of view is also the most well-suited for the use of string diagrams.

Indeed, our approach fits in a recent thread of research aiming to represent and reason on computational processes using diagrams with inputs and outputs. Those diagrams can be thought of as boolean circuits-like structures, built from elementary generators (or gates) on which we can perform local rewritings by replacing a sub-circuit with another one having the same type and an equivalent behavior. Such methods have been successfully applied to provide compositional syntax for control flow graphs [BSZ14; BSZ21] or quantum computing [Wet20] for example. As with the choice of moving from functions to relations, the diagrammatic paradigm requires the introduction of unfamiliar notions (for a reader used to automata, transition systems, or symbolic dynamic) from category theory [Sel11]. Still, even if dressed in the unusual language of category theory and diagrams, the fundamental notions involved are the same.

We hope that the benefits of this choice outweigh the price paid for it. Indeed, our formalism being formulated in the language of string diagrams (or equivalently, in the language of symmetric monoidal categories [Mac98]), we expect to be able to obtain straightforward generalizations by changing our base category (the mathematical world in which we interpret our diagrams) from relation to stochastic kernels or quantum channels. This provides solid theoretical bases to define meaningful notions of automata, transition systems, and symbolic dynamical systems in the probabilistic and quantum case, on which we could develop similar simulation-based proof techniques.

One can see the current paper as the first step toward this goal. The use of diagrammatic formalism to unify notions of finite tilings and quantum tensors has been developed in
[CM24].

We hope our unified formalism can ease the transfer of ideas between the transition system and symbolic dynamics communities and stimulate the emergence of new questions and insights set off by our diagrammatical approach.

In this paper, we introduce relational transducers with finite states and show how they generalize finite automata, LTS, and symbolic dynamical systems. We define their behaviors on both finite and bi-infinite words. In both cases, we fully characterize the admissible behaviors with the notion of regular and sofic relations, respectively. We also introduce two string diagrammatic equational theories which are able to represent transducers on finite and bi-infinite words in a compositional way. We show that those equational theories are expressive enough to represent any transducers and present two sound simulation principles that are strong enough to equate in a diagrammatic form any two transducers having the same behavior, both in the finite and bi-infinite case. On a more technical side, we present a new diagrammatical formulation of the notion of backward and forward simulation and introduce a new notion of normal form for the presentation of a sofic subshift.

We start by introducing the diagrammatic aspects of our approach in Section 2. In Section 3, with the notion of transducers used throughout the paper, we introduce our diagrammatical equational theory and completeness result for transducers acting on finite words. Section 4 gathers results on sofic relations culminating in the extension of our diagrammatical theory and a completeness proof for the case of bi-infinite words. Most of the proofs are postponed to the appendix.

## 2 Relations and their Diagrams

Before introducing transducers, we quickly present the formalism we use to handle relations between finite sets. We later use the same formalism for relations between infinite sets, more specifically sets of finite words and sets of bi-infinite words. In the context of relations, those infinite sets will always be clearly denoted with a `*` or a `_Z`, as such, the letters A, B, C, ... will refer to finite sets.

Given some finite sets $A_1, \dots, A_n, B_1, \dots, B_m$, a relation $\mathcal{R}$ from $\Pi_{i=1}^n A_i$ to $\Pi_{j=1}^m B_j$ is simply a subset $\mathcal{R} \subseteq \Pi_{i=1}^n A_i \times \Pi_{j=1}^m B_j$. We write $a \mathcal{R} b$, and say that $\mathcal{R}$ relates $a$ to $b$, whenever $(a, b) \in \mathcal{R}$. We represent such relation as the diagram on the left, the identity relation on $\Pi_{i=1}^n A_i$ as the one on the middle, and the transposed of $\mathcal{R}$ (defined by $b\mathcal{R}ta$ iff $a\mathcal{R}b$) as the one on the right.

<figure><img src="image_2.png" /></figure>

We write $\mathbf{1} = \{()\}$ for the singleton set which is the zero-ary Cartesian product, and we will often omit diagrammatically the wires labeled by $\mathbf{1}$. Three notable relations are the swap $\gamma_{A,B} = \{((a, b), (b, a)) \mid a \in A, b \in B\}$, the cap $\eta_A = \{((), (a, a)) \mid a \in A\} : \mathbf{1} \to A \times A$ and the cup $\epsilon_A = \{((a, a),()) \mid a \in A\} : A \times A \to \mathbf{1}$, which we represent with bent wires as below. We also represent below the “full” relation $\bullet_{A,B} = A \times B : A \to B$.

<figure><img src="image_3.png" /></figure>

We give in Figure 1 a couple of remarkable identities about them. We note that there is a lot of arbitrary choices in those representations, as for example a relation from $A \times B$ to $\mathbf{1}$ could be represented in any of the following ways.

$$A \times B - \boxed{\mathcal{R}} = A \times B - \boxed{\mathcal{R}} - \mathbf{1} = \frac{A}{B} - \boxed{\mathcal{R}} = \frac{A}{B} - \boxed{\mathcal{R}} - \mathbf{1}$$
<figure><img src="image_4.png" /><figcaption>Figure 1: Equations for the Cup and Cap.</figcaption></figure>

Nevertheless, those graphical representations remain practical, especially when representing various kind of compositions. The usual ones are the sequential compositions of $\mathcal{R}: A \to B$ with $\mathcal{S}: B \to C$, and the parallel composition of $\mathcal{R}: A \to B$ and $\mathcal{S}: C \to D$, which are defined as follows:

$$ \mathcal{S} \circ \mathcal{R} = \{(a, c) \mid \exists b \in B, a \in \mathcal{R}, b, c \in \mathcal{S}\} \qquad \mathcal{R} \times \mathcal{S} = \{((a, c), (b, d)) \mid a \in \mathcal{R}, c, d \in \mathcal{S}\} \\ A \rightarrow \mathcal{S} \circ \mathcal{R} \rightarrow C = A \rightarrow \mathcal{R} \rightarrow B \rightarrow \mathcal{S} \rightarrow C \rightarrow A \rightarrow \mathcal{R} \rightarrow B \rightarrow \mathcal{S} \rightarrow C = A \rightarrow \mathcal{R} \rightarrow B \rightarrow \mathcal{S} \rightarrow D = C \rightarrow \mathcal{S} \rightarrow D $$

The general case is the partial composition. For example, given two relations $\mathcal{R}: A \to B \times C$ and $\mathcal{S}: C \times D \to E$, their composite relation $\{((a, d), (b, e)) \mid \exists c, a \in \mathcal{R}, (b, c), (c, d) \in \mathcal{S}, e\}: A \times D \to B \times E$ is written diagrammatically as shown on the right. Conversely, whenever we have a diagram that decomposes $\mathcal{R}: \Pi_{i=1}^n A_i \to \Pi_{j=1}^m B_j$, into the partial composition of $\mathcal{R}_1, \dots, \mathcal{R}_r$, and if we write $C_1, \dots, C_p$ for all the sets labeling the “internal wires” of the diagram, then we can build a logical formula equivalent to $(a_1, \dots, a_n) \in \mathcal{R}(b_1, \dots, b_m)$ of the following form:

$$ \exists c_1 \in C_1, \dots, \exists c_p \in C_p, (\mathcal{R}_{1-}) \wedge \dots \wedge (\mathcal{R}_{p-}) $$

where the blanks _ have to be filled with adequate tuples of $a_i, b_j$ and $c_k$. For example, the following diagram would correspond to the following logical formula:

$$ a \left( A \xrightarrow{\substack{\mathcal{R}_1 \\ \mathcal{R}_2}} B \right) b \iff \exists c_1 \in C_1, \exists c_2 \in C_2, ((a, c_1) \in \mathcal{R}_1 (c_2, b)) \wedge (c_1 \in \mathcal{R}_2 c_2) $$

We remark that if any of the $\mathcal{R}_\ell$ is the full relation $\bullet_{A,B}$, then it can safely be omitted from the logical formula as $(a \bullet_{A,B} b)$ is always true. Combining the partial composition with the swap, cup and cap defined above, one can reorganize the inputs and outputs of a relation, turning for example a relation $\mathcal{R}: A \times B \times C \to D$ into a relation from $B \times A$ to $D \times C$ as on the right.

<figure><img src="image_5.png" /></figure>

All those diagrams can actually be formalized using string diagrams from category theory [Mac98]. Indeed, finite sets and relations form a strict symmetric monoidal category, called **FinRel**. We recall the definition of such a category in Appendix A, though for the sake of this paper, the only required understanding is “the diagrams works as intended, there is never a need to explicitly add bracketing, and all ’reasonable’ ways of rewriting a diagram yield the same relation”. If we account for the cup and cap, relations even form a compact closed category<fnref n="1" />, which exactly means that it satisfies the equations listed in

<footnote n="1">¹Where the dual is the transposition on relations, and the identity on objects.</footnote>
Figure 1. We redirect to [Sel11] for a survey of variations around monoidal categories and the corresponding diagrammatic notations.

# 3 Transducers on Finite Words

## 3.1 Transducers and Regular Relations

For any finite set $A$, called an alphabet, we denote $A^*$ the set of finite words over $A$, that is $A^* = \mathcal{U}_{k \ge 0} A^k$. We write a word $w = w_1 \dots w_k \in A^*$, $|w|$ for its size $k$ and $\epsilon$ for the empty word. The concatenation of two words $u$ and $v$, respectively of size $n$ and $m$, is denoted $uv$ and has size $n+m$. A subset of $A^*$ is called a language over the alphabet $A$. A **uniform relation** between two alphabets $A$ and $B$, denoted $\mathcal{R}: A^* \to B^*$, is a language over the product alphabet $A \times B$, equivalently, it's a relation between $A^*$ and $B^*$ only relating words of the same size, i.e. $u \mathcal{R} v$ implies $|u| = |v|$.

The product of two uniform relations $A^* \to B^*$ and $C^* \to D^*$ is formally a relation $A^* \times C^* \to B^* \times D^*$ but to maintain the uniformity constraints, we choose to restrict it to a uniform relation $(A \times C)^* \to (B \times D)^*$. While of course $(A \times B)^* \neq A^* \times B^*$ as sets, we will identify the two as long as all relations involved are uniform. In other words, uniform relations are ignoring the elements of $A^* \times B^*$ that are not in $(A \times B)^*$. We keep the notation $\mathcal{R} \times S$ for this uniform product, even if it is no longer a Cartesian product. Uniform relations are preserved by composition and (uniform) product, and include identities, as well as cups and caps. Similarly to **FinRel**, they form a compact closed strict symmetric monoidal$^2$ category called **UniRel**, meaning we can use the exact same graphical representation for them.

**Definition 3.1 (Transducer).** A (non-deterministic finite) transducer is a tuple $(\mathcal{T}, A, B, Q, I, F)$ where $A$ is a finite set representing the *input alphabet*, $B$ is a finite set representing the *output alphabet*, $Q$ is a finite set representing the *states*, $\mathcal{T}: A \times Q \to B \times Q$ the *transition relation*, $I \subseteq Q$ the *initial states* and $F \subseteq Q$ the *final states*.

Similarly to non-deterministic finite automata, we write $q \xrightarrow{a} q'$ whenever $((a, q), (b, q'))$ is a transition of $\mathcal{T}$. A **run** of length $k$ within a transducer is a sequence

$$q_0 \xrightarrow{a_1} q_1 \xrightarrow{a_2} \dots \xrightarrow{a_k} q_k$$

such that $q_0 \in I$ and $q_k \in F$. When such a run exists, we say that the transducer can transform the word $a_1 \dots a_k$ into $b_1 \dots b_k$. The *behavior* of the transducer, written $\mathcal{L}(\mathcal{T}, A, B, Q, I, F)$, is the uniform relation from $A^*$ to $B^*$ which relates $w$ to $v$ whenever the transducer can transform $w$ into $v$.

A transducer with only inputs, said otherwise $B = 1$, is exactly a non-deterministic finite automaton. Alternatively, every transducer from $A$ to $B$ can be seen as a non-deterministic finite automaton over $A \times B$. We recall that a **regular language**, is a language recognized by a finite automaton. A **regular relation** is a uniform relation $A^* \to B^*$ which is a regular language when seen as a subset of $(A \times B)^*$, which is the case if and only if it is the behavior of a transducer.

**Proposition 3.1.** Regular relations are preserved by composition and product. We call **RegRel** the subcategory of **UniRel** of regular relations.

<footnote>$^2$Note that the monoidal unit of **UniRel** is $1^*$, that is the words over the singleton alphabet, which is isomorphic to $\mathbb{N}$.</footnote>
The proof is based on standard construction of products and composition of transducers.

Any relation $\mathcal{R} : A \to B$ can be lifted to a regular$^3$ relation $\mathcal{R}^* : A^* \to B^*$ defined letter by letter: $\mathcal{R}^* = \{(u, v) \mid |u| = |v|, \forall 1 \le i \le |u|, (u_i, v_i) \in \mathcal{R}\}$. Categorically, this lift is a faithful strong symmetric monoidal functor from **FinRel** to **RegRel**, which means:

**Functoriality** $(\mathcal{S} \circ \mathcal{R})^* = \mathcal{S}^* \circ \mathcal{R}^*$ and $(\mathrm{id}_A)^* = \mathrm{id}_{A^*}$.

**Strong Monoidality** $(\mathcal{R} \times \mathcal{S})^*$ can be identified with $\mathcal{R}^* \times \mathcal{S}^*$ within **RegRel**.

**Symmetric** $(\gamma_{A,B})^* = \gamma_{A^*,B^*}$.

**Faithfullness** If $\mathcal{R}^* = \mathcal{S}^*$, then necessarily $\mathcal{R} = \mathcal{S}$.

This notion of transducers and regular relations appeared early in the history of theoretical computer science, one can find similar definitions, though in a different form in [EM65].

## 3.2 Diagrammatic Representation of Transducers

Looking at $\mathcal{R} : \Pi_{i=1}^n A_i \to \Pi_{j=1}^m B_j$, we can see its lifted relation $\mathcal{R}^*$ as going from $\Pi_{i=1}^n A_i^*$ to $\Pi_{j=1}^m B_j^*$, since $(\Pi_{i=1}^n A_i)^*$ is identified with $\Pi_{i=1}^n A_i^*$ (we are only working with uniform relations here). Diagrammatically, this allows us to apply $\mathrm{-}^*$ to individual wires:

$$ \begin{array}{c} A_1^* \xrightarrow{\vdots} \boxed{\mathcal{R}^*} \xrightarrow{\vdots} B_1^* \\ A_n^* \xrightarrow{\vdots} B_m^* \end{array} = (\Pi_{i=1}^n A_i)^* - \boxed{\mathcal{R}^*} - (\Pi_{j=1}^m B_j)^* $$

When looking at uniform relations over words, one such regular$^4$ relation will be particularly useful, the **finite shift** $\triangleright_A^{|F}$: $A^* \to A^*$ for a finite set $A$ and two subsets $I, F \subseteq A$, defined as $\{(w, v) \mid \exists i \in I, \exists f \in F, iw = vf\}$. Said otherwise, $w$ and $v$ are related by the shift if either both are empty and $I \cap F \neq \emptyset$, or if neither are empty and the first letter of $v$ is in $I$, the last letter of $w$ is in $F$, and the remaining letters satisfy $w_k = v_{k+1}$. Diagrammatically, we represent the shift and its transposed: $\triangleright_A^{|F} = A^* \xrightarrow{\exists I \mid F} A^*$, $(\triangleright_A^{|F})^t = A^* \xrightarrow{\exists I \mid F} A^*$.

The shift allows to obtain the behavior of a transducer in a compositional way.

**Proposition 3.2** (Proved in Appendix B.2). For every transducer $(\mathcal{T}, A, B, Q, I, F)$, its behavior can be obtained by lifting $\mathcal{T}$ and using the shift as follows:

$$ A^* \xrightarrow{Q^*} \boxed{\mathcal{T}^*} \xrightarrow{I \mid F} B^* = A^* - \boxed{\mathcal{L}(\mathcal{T}, A, B, Q, I, F)} - B^* $$

## 3.3 Diagrammatic Language for Transducers

This is however not the only way to represent transducers using relations. Another approach is to start from the category **FinRel** and freely add a feedback, state that a transducer $(\mathcal{T}, Q, B, Q, I, F)$ should be able to be represented by the diagram on the right, and then find additional equations ensuring that this feedback operator behaves exactly as transducers do.

<figure><img src="image_6.png" /></figure>

Formally, we define a graphical language **Trans**, so a syntactical construct, where the diagrams are seen as mathematical objects distinct from the relations they represent – which

<footnote>$^3$The corresponding transducer has only one state which is accepting and initial and its transition relation is directly $\mathcal{R}$ seen as having type $A \times 1 \to B \times 1$.</footnote>

<footnote>$^4$It is the behavior of the transducer $(\gamma_{A,A}, A, A, A, I, F)$.</footnote>
<figure><img src="image_7.png" /><figcaption>Figure 2: Equations for a Feedback Category.</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>Figure 3: Equations for Faithfully Embedding FinRel.</figcaption></figure>

is a category where the objects are finite sets, and where the morphisms are generated by composing sequentially and in parallel the generators below together with the usual equations of a strict symmetric monoidal category (see Figure 10 in the appendix for a reminder), the equations of a feedback category<fnref n="5" /> (see Figure 2), and some equations ensuring we faithfully embed **FinRel** (see Figure 3).

<figure><img src="image_9.png" /></figure>

Let us point a couple of facts about this language:

• A bundle of wires labeled $A_1, \dots, A_n$ is the same as a single wire labeled $\Pi_{i=1}^n A_i$.

• The wires and syntactical constructs are in **thick blue**, to distinguish them from actual relations. $\mathcal{R}$ refers to an actual relation while $\mathbf{R}$ refers to an element of our language.

• Double-line boxes denote the generator, while single-line boxes denote any diagram potentially constituted of many generators, including feedbacks.

• The arrows on the feedback are a reminders that those are not the same as the cup and cap of Section 2.

• Within Figure 2, the gray lines correspond to bracketing, and similarly to the equations of a strict symmetric monoidal category, the overall consequences of those equations is that bracketing can be safely ignored. Additionally, compared to the literature, those equations had to be adapted to the presence of labels on the feedback.

<footnote n="5">⁵Some authors, like in [KSW02], have an additional equation which allows to slide isomorphisms through the feedback. While we do not have this equation, it is actually a special case of Figure 5, which is part of the completed equational theory.</footnote>
<figure><img src="image_10.png" /><figcaption>Figure 5: Sliding.</figcaption></figure>

**Theorem 3.5 (Completeness).** For **R** and **T** two diagrams of **Trans** from **A** to **B**. Whenever $[[\mathbf{R}]] = [[\mathbf{T}]]$, we can rewrite **R** into **T** by using only the rules of **Trans** and Figure 4.

The core idea of the proof is diagrammatically mimic the determinization and minimization from automata theory. We recall that a finite automaton is simply a transducer with 1 for output alphabet, so we start by studying completeness in the case where $B = 1$.

**Definition 3.2 (Determinization).** Let $(\mathcal{T}, A, Q, I, F)$ be a finite automaton. We write $\xrightarrow{\mathcal{T}}$ for the transitions within that automaton. Its determinization is the automata

$$ (\mathcal{P}(\mathcal{T}), A, \mathcal{P}^{\text{acc}}(Q), \{I\}, \mathcal{P}_{\cap F \neq \emptyset}^{\text{acc}}(Q)) $$

More precisely, we start by recalling that $\mathcal{P}(Q)$ is the set of all subsets of $Q$. We use $x, y$ for elements of $Q$, and $X, Y$ for elements of $\mathcal{P}(Q)$. Then, we define the function$^7$ $\mathcal{P}(\mathcal{T}) : A \times \mathcal{P}(Q) \to \mathcal{P}(Q)$ as $\mathcal{P}(\mathcal{T})(a, X) = \{y \in Q \mid \exists x \in X, x \xrightarrow{a} y\}$. We then consider the set $\mathcal{P}^{\text{acc}}(Q)$ of subsets of $Q$ accessible by iteration of that function, starting from $I$. We can now restrict $\mathcal{P}(\mathcal{T})$ to a function $A \mapsto \mathcal{P}^{\text{acc}}(Q) \to \mathcal{P}^{\text{acc}}(Q)$. Lastly, $\mathcal{P}_{\cap F \neq \emptyset}^{\text{acc}}(Q)$ is the set of accessible subsets of $Q$ that have a non-empty intersection with $F$.

**Proposition 3.6.** For all finite automata $(\mathcal{T}, A, Q, I, F)$, we have

$$ \mathcal{P}^{\text{acc}}(Q) \xrightarrow{A} \mathcal{P}^{\text{acc}}(Q) \xrightarrow{\exists} \mathcal{T} \xrightarrow{Q} \mathcal{P}^{\text{acc}}(Q) = \mathcal{P}^{\text{acc}}(Q) \xrightarrow{A} \mathcal{P}(\mathcal{T}) \xrightarrow{\mathcal{P}^{\text{acc}}(Q)} \mathcal{P}^{\text{acc}}(Q) \xrightarrow{\exists} Q $$

where $\exists: \mathcal{P}^{\text{acc}}(Q) \to Q$ is the usual “contains” relation, that is $X \ni x$ whenever $x \in X$.

*Proof.* Using the logical reasoning as in Section 2, we can rewrite the equation as the following. We are looking at $\forall a \in A, \forall X \in \mathcal{P}^{\text{acc}}(Q), \forall y \in Q$,

$$ (\exists x \in Q, (x \in X) \land (x \xrightarrow{a} y)) \iff (\exists Y \in \mathcal{P}^{\text{acc}}(Q), (X \xrightarrow{a} Y) \land (y \in Y)) $$

We start by reformulating the right side of the equivalence, as $\mathcal{P}(\mathcal{T})$ is a function, we can remove the $\exists$ and write $y \in \mathcal{P}(\mathcal{T})(a, X)$. Then, using the definition of $\mathcal{P}(\mathcal{T})$, we obtain that it is equivalent to $\exists x \in X, x \xrightarrow{a} y$, which is exactly the left side of the equivalence. $\square$

Rephrased in our graphical language and apply in the simulation principle, this gives:

**Corollary 3.7.** For any finite automaton $(\mathcal{T}, A, Q, I, F)$, using Figure 4, we have

$$ \mathcal{P}^{\text{acc}}(Q) \xrightarrow{A} \mathcal{P}(\mathcal{T}) \xrightarrow{\mathcal{P}^{\text{acc}}(Q)} \mathcal{P}^{\text{acc}}(Q) \xrightarrow{\exists} \mathcal{P}^{\text{acc}}(Q) \xrightarrow{\{I\} \cap \mathcal{P}_{\cap F \neq \emptyset}^{\text{acc}}(Q)} \mathcal{P}^{\text{acc}}(Q) $$

<footnote>$^7$We consider functions to be a special case of relations.</footnote>
Another key element of our completeness result is the minimization of automata.

**Definition 3.3 (Minimization).** Let $(\mathcal{D}, A, Q, \{i\}, F)$ be a **deterministic finite automaton** where every state is accessible from the initial state. We write $\xrightarrow{\mathcal{D}}$ for the transitions within that automaton. We write $\xrightarrow{w}$ with $w$ a word of size $n$ for its iterated transition $\xrightarrow{w_1} \dots \xrightarrow{w_n} \mathcal{D}$. Its minimization is the deterministic automata $(L_{\mathcal{D}}, A, L_{A^*}, L_{\epsilon}, L_{A^*}^{\exists \epsilon})$.

More precisely, we write $L_w = \{v \in A^* | \exists f \in F, i \xrightarrow{w} f\}$, and remark that whenever $L_w = L_u$, then for all $a \in A$ we also have $L_{wa} = L_{ua}$. We then define $L_{A^*} = \{L_w | w \in A^*\}$ note that a single element of this set might correspond to multiple distinct $w$, and in fact $L_{A^*}$ is actually smaller or equal to $Q$ in cardinality. We defined its restriction $L_{A^*}^{\exists \epsilon} = \{L_w | w \in A^*, \epsilon \in L_w\}$. Lastly, we define the transition function as $L_{\mathcal{D}}(a, L_w) = L_{wa}$.

This minimization is well known in the literature [HMU07], and yields the unique smallest deterministic automaton equivalent to the starting one.

**Proposition 3.8.** For any deterministic finite automaton $(\mathcal{D}, A, Q, \{i\}, F)$ where every state is accessible from the initial state, we have

$$ P \xrightarrow{A} \mathcal{D} \xrightarrow{P} \mathcal{L} \xrightarrow{L_{A^*}} L_{A^*} = P \xrightarrow{A} \mathcal{L} \xrightarrow{L_{A^*}} \mathcal{L}_{\mathcal{D}} \xrightarrow{L_{A^*}} L_{A^*} $$

where $\mathcal{L}: Q \to L_{A^*}$ relates $p \in Q$ to $\ell \in L_{A^*}$ whenever $\ell = \{v | \exists f \in F, p \xrightarrow{v} f\}$. We note that since every state is accessible, there exists $w \in A^*$ such that the later is equal to $L_w$.

The core idea is similar to Proposition 3.6: we express both sides of the equality as equations relating transitions of the transducers, and prove their equivalence using standard argument of automata minimization. Again the simulation principle can be applied to conclude that the behavior of an automata and its minimization are the same.

**Corollary 3.9.** For any deterministic finite automaton $(\mathcal{D}, A, Q, \{i\}, F)$ where every state is accessible from the initial state, using Figure 4, we have

$$ P \xrightarrow{A} \mathcal{D} \xrightarrow{\{i\} | F} P = L_{A^*} \xrightarrow{L_{\mathcal{D}}} L_{A^*} $$

We can now provide a proof of the completeness result.

*Proof of Theorem 3.5.* We start with two diagrams **R**, **S** of **Trans** from **A** to **B** and assume $[[\mathbf{R}]] = [[\mathbf{S}]]$. We start by focusing on **R**. We combine it with the cup $\epsilon_B$ to bend its output into an input, and we then use Proposition 3.3 to put the result in quasi-normal form. Then, we use Corollary 3.7 followed by Corollary 3.9 to obtain:

$$ B \xrightarrow{A} \mathbf{R} \xrightarrow{B} \mathcal{E}_B = B \times A \xrightarrow{Q} \mathcal{T} \xrightarrow{I | F} Q = L_{(B \times A)^*} \xrightarrow{L_{\mathcal{P}(\mathcal{T})}} L_{(B \times A)^*} $$

For convenience, we name $(\mathcal{R}_M, B \times A, Q_M, I_M, F_M)$ the resulting minimal automaton. We do the same for **S** and write $(\mathcal{S}_N, B \times A, Q_N, I_N, F_N)$ for the resulting minimal automaton. Since $[[\mathbf{R}]] = [[\mathbf{S}]]$ and by soundness of the equations, we obtain that:

$$ \left[ \begin{array}{ccc} B \times A & \mathcal{R}_M & Q_M \\ Q_M & I_M | F_M & Q_M \end{array} \right] = \left[ \begin{array}{ccc} B \times A & \mathcal{S}_N & Q_N \\ Q_N & I_N | F_N & Q_N \end{array} \right] $$
Using the definition of $\llbracket - \rrbracket$ and Proposition 3.2, it follows that $(\mathcal{R}_M, B \times A, Q_M, I_M, F_M)$ and $(S_N, B \times A, Q_N, I_N, F_N)$ recognize the same language, hence by uniqueness of the minimal automaton (see [HMU07]) we obtain that the two automata are equal up to an isomorphism $\iota: Q_M \to Q_N$, hence using the simulation principle with this $\iota$, we obtain

<figure><img src="image_11.png" /></figure>

By combining with the cap $\eta_B$ to bend the input $B$ into an output, and using the fact that $(\mathbf{id}_B \times \epsilon_B) \circ (\eta_B \times \mathbf{id}_B) = \mathbf{id}_B$, we obtain $\mathbf{R} = \mathbf{S}$. $\square$

The simulation principle requires to find a well chosen relation between the state spaces of two automata for the language equality to follow. This is reminiscent of the well studied simulation techniques in automata theory, and it is not a coincidence. In fact, the simulation principles also holds in the case where we only want language inclusion, simply by replacing every “=” of Figure 4 by $\subseteq$ (for a backward-simulation) or by $\supseteq$ (for a forward-simulation). Thus, the simulation principle can be reinterpreted as asking to find a simulation which is at the same time forward and backward, the fact that finding a backward-forward simulations implies language equivalence has already appeared in the literature [LV95].

# 4 Transducers on Bi-Infinite Words

We will now consider the case of transducers acting on bi-infinite words, i.e. words that are infinite both ways. We call those transducers $\mathbb{Z}$-transducers, and note that within them the notion of initial or final state becomes irrelevant, although one could argue that in fact all the states of those transducers are both initial and final.

## 4.1 $\mathbb{Z}$-Transducers

Similarly to the _* lift, for $A$ finite, we consider elements of $A^{\mathbb{Z}}$ as infinite words $\dots w_{-1}w_0w_1\dots$, and we define the lifted relation $\mathcal{R}^{\mathbb{Z}}: A^{\mathbb{Z}} \to B^{\mathbb{Z}}$ of $\mathcal{R}: A \to B$ as $\{(w, v) \mid \forall i \in \mathbb{Z}, (w_i, v_i) \in \mathcal{R}\}$. Similarly to **UniRel** with _*, we write **Z-Rel** for the compact closed strict symmetric monoidal category of relations over sets of the form $A^{\mathbb{Z}}$, and reuse the diagrammatic representations of **FinRel** in this setting. Similarly to _*, we can apply _Z to individual wires as below, and this lifting operation is a faithful strong symmetric monoidal functor from **FinRel** to **Z-Rel**.

$$A_1^{\mathbb{Z}} \vdots \boxed{\mathcal{R}^{\mathbb{Z}}} \vdots B_1^{\mathbb{Z}} = (\Pi_{i=1}^n A_i)^{\mathbb{Z}} - \boxed{\mathcal{R}^{\mathbb{Z}}} - (\Pi_{j=1}^m B_j)^{\mathbb{Z}}$$

We can also define $\mathbb{Z}$-transducers – a.k.a transducers on bi-infinite words. They are simply tuples $(\mathcal{T}, A, B, Q)$ similar to transducers but without a specified sets of initial or final states. When $B = 1$, such transducers corresponds to transition systems with finite set of states. When $A = 1$, they can also be interpreted as generalized symbolic dynamic systems. Indeed the set of elements of $Q$ in relation with a symbol $b \in B$ form an overlapping partition of $Q$, and the transition function can be interpreted as the action of a non-deterministic dynamic.

We reuse the same notations as for usual transducers, and note that a **run** within an $\mathbb{Z}$-transducer is now a bi-infinite sequence $\dots \xrightarrow{a_1} q_{-1} \xrightarrow{a_0} q_0 \xrightarrow{a_1} q_1 \xrightarrow{a_2} q_2 \dots$. When such a run exists, we say that the transducer can transform the bi-infinite word $\dots a_{-1}a_0a_1\dots$
into ... $b_{-1}b_0...b_1...$. The behavior of the transducer is the relation from $A^Z$ to $B^Z$ which relates $w$ to $v$ whenever the transducer can transform $w$ into $v$. We write $\mathcal{L}^Z(\mathcal{T}, A, B, Q)$ for its behavior. We define the **infinite shift** $\triangleright_A: A^Z \to A^Z$ as the relation $\{(w, v) | \forall k \in \mathbb{Z}, w_k = v_{k+1}\}$. Said otherwise, $\triangleright_A((a_n)_{n \in \mathbb{Z}}) = (a_{n-1})_{n \in \mathbb{Z}}$. We often omit the alphabet $A$ and only write $\triangleright$ when the alphabet is clear from context and we represent it and its transposed: $\triangleright_A = A^Z \rightarrow \triangleright A^Z$, $(\triangleright_A)^t = A^Z \leftarrow \triangleright A^Z$. As in the finite case, we can obtain the behavior of a transducer from the shift.

**Proposition 4.1.** For every $\mathbb{Z}$-transducer $(\mathcal{T}, A, B, Q)$, its behavior can be obtained using the lift of $(\mathcal{T}, A, B, Q)$ and the shift as follows:

$$A^Z \xrightarrow{\mathcal{T}^Z} B^Z = A^Z \xrightarrow{\mathcal{L}^Z(\mathcal{T}, A, B, Q)} B^Z$$

In Lemma 4.5 we will link the behavior of a $\mathbb{Z}$-transducer $(\mathcal{T}, A, B, Q)$ to the behavior of the transducer $(\mathcal{T}, A, B, Q, Q, Q)$, that is, where all the states are initial and final.

## 4.2 Sofic Relations

We define the analog of regular languages and relations in the bi-infinite case. We start with **sofic subshifts** which have been extensively studied in symbolic dynamics.

### 4.2.1 Sofic Subshifts, Factor-Closure and Limits

For a finite, we can define a distance on $A^Z$ as $d(x, y) = 2^{-\inf\{i \in \mathbb{N}, x_i \neq y_i \lor x_{-i} \neq y_{-i}\}}$. The topology induced by this distance is called the prodiscrete topology (or Cantor topology), for which $A^Z$ is compact and closed. Subsets of $A^Z$ that are shift-invariant (meaning $\triangleright_A(X) = X$) and closed for the prodiscrete topology are called **subshifts**.

**Definition 4.1 (Factor).** Given two potentially bi-infinite words $x, y \in A^* \cup A^Z$, we say that $x$ is a factor of $y$ and write $x \sqsubseteq y$ whenever there exists $u, v$ such that $y = uxv$. Additionally, we say that $x$ is an internal factor of depth $n$, and write $x \sqsubseteq_n y$, whenever both $u$ and $v$ are of length at least $n$ (including infinity). For $x \in A^Z$, we then define $\text{Fact}(x) := \{u \in A^* | u \sqsubseteq x\}$. Similarly, for $X$ a subshift or a language, we define $\text{Fact}(X) := \{u \in A^* | \exists x \in X, u \sqsubseteq x\}$. A language $L$ is said **factor-closed** if $\text{Fact}(L) = L$.

A subshift $X \subseteq A^Z$ is said to be **sofic**$^8$ if $\text{Fact}(X)$ is regular. More than that, a sofic subshift can actually be generated by its factors with a well-chosen notion of limit.

For the remaining of this section, whenever we consider words of $A^*$, we consider them to be indexed as if they were words of $A^Z$. By default, $u \in A^*$ is indexed from 0 to $|u| - 1$ but we write $\triangleright^k(u)$ for its $k$-shifted version indexed from $-k$ to $-k + |u| - 1$. Whenever $i$ is not a valid index for $u$, we write $u_i = \perp$. This allows us to extend$^9$ the distance $d(u, x)$ to a finite word $u$ and an infinite word $x$.

**Definition 4.2 (Limit Language).** Given a language $L \subseteq A^*$, we define its limit language $\vec{L}$ as the set of bi-infinite words that can be reached as a limit of words in $L$, that is:

$$\vec{L} := \{x \in A^Z, \exists (u_n)_{n \in \mathbb{N}} \in L^\mathbb{N}, (k_n)_{n \in \mathbb{N}} \in \mathbb{N}^\mathbb{N} \text{ s.t. } \lim_{n \to \infty} \triangleright^{k_n}(u_n) = x\}$$

**Lemma 4.2.** Given a language $L \subseteq A^*$, its limit language $\vec{L}$ is a subshift.

<footnote>$^8$There are several equivalent definitions of sofic subshifts, we briefly discuss this in Appendix C.1</footnote>

<footnote>$^9$The formula is unchanged, that is $d(x, y) = 2^{-\inf\{i \in \mathbb{N}, x_i \neq y_i \lor x_{-i} \neq y_{-i}\}}$; see Appendix C.1.</footnote>
It is clear that different languages can have the same limit, typically a language and its factor closure have the same limit, however there is a canonical language for a given sofic subshift. The idea is to remove all the words that are not relevant for the limit behavior.

**Definition 4.3 (Pruned Language).** Given a language $L \subseteq A^*$, we define its pruned sublanguage $\text{Prun}(L)$ as the set of words in $L$ that have arbitrarily long (simultaneous) left and right extensions that is : $\text{Prun}(L) := \{u \in L, \forall n \in \mathbb{N}, \exists v \in L, u \subseteq_n v\}$. A language $L$ is said to be **pruned** when $L = \text{Prun}(L)$, or equivalently whenever for every $w \in L$ there exists two non-empty words $u, v$ such that $uwv \in L$.

**Proposition 4.3.** Fact(-) : $\mathcal{P}(A^Z) \to \mathcal{P}(A^*)$ can be restricted to a bijection between sofic subshifts and pruned factor-closed regular languages, and has $\stackrel{\rightarrow}{-} : \mathcal{P}(A^*) \to \mathcal{P}(A^Z)$ for inverse when restricted similarly.

This result allows to reduce questions on sofic subshifts to questions on pruned factor-closed regular languages.

### 4.2.2 Presentation of a Sofic Subshift

We have established a bijection between sofic subshifts and factor closed-regular languages, now building on this we introduce a normal form for automata that allows us to reproduce our completeness result to the infinite case.

**Definition 4.4 (Presentation of a Sofic Subshift).** A **presentation** $(\mathcal{T}, A, Q)$ of a sofic subshift $X$ is an automaton $(\mathcal{T}, A, Q, \overline{Q}, \overline{Q})$, meaning all the states are initial and final, recognizing a language $L$ and such that $\overline{L} = X$. A presentation is said

**Pruned** if its language is pruned, meaning that for every word $w$ in the language, there exists $u$ and $v$ both non-empty such that $uwv$ is in the language.

**Right-Resolving** whenever its transition relation is a partial function.

**Rooted** whenever there exists a root state $r$ such that

* every accepted word admits an accepted run starting by $r$,

* and every state is accessible from $r$, meaning there is a run from $r$ to that state.

**Theorem 4.4 (Uniqueness).** Every non-empty$^{10}$ sofic subshift admits a unique minimal rooted right-resolving pruned presentation, up to isomorphism.

Notice that this result is not in contradiction with the well known fact that the minimal presentation of a sofic subshift is not unique in general [LM21]. Indeed, it is often possible to find non-rooted presentations that are smaller than our “minimal” one, but it is from this rootedness that we obtain uniqueness.

### 4.2.3 Sofic Relations and $\mathbb{Z}$-Transducers

A relation $\mathcal{R} : A^Z \to B^Z$ is said sofic if it is a sofic subshift when seen as a subset of $(A \times B)^Z$, which we know is equivalent to having a representation $(\mathcal{T}, A \times B, \overline{Q})$. Using the usual equivalence between automaton on $A \times B$ and transducers from $A$ to $B$, and a relation $\mathcal{R} : A^Z \to B^Z$ is sofic if and only if there exists a $\mathbb{Z}$-transducer $(\mathcal{T}, A, B, \overline{Q})$ such that $\overline{\mathcal{L}(T, A, B, Q, \overline{Q}, \overline{Q})} = \mathcal{R}$. Using the following lemma, $\mathcal{R}$ is sofic if and only if it is the behavior of a $\mathbb{Z}$-transducer.

<footnote>$^{10}$If the sofic subshift is empty, its only pruned presentation is the empty automaton, but this automaton is not rooted.</footnote>
**Lemma 4.5.** Given a Z-transducers (*T*, *A*, *B*, *Q*), we consider the transducer (*T*, *A*, *B*, *Q*, *Q*)
where all the states are initial and final. We have $\mathcal{L}^Z(\mathcal{T}, A, B, Q) = \overline{\mathcal{L}}(\mathcal{T}, A, B, Q, Q, \overline{Q})$.

The composition or product of two sofic relations is sofic, one can simply build the
associated Z-transducer using the exact same construction as in Proposition 3.1, so we write
**SofRel** for the subcategory of Z-**Rel** of sofic relations.

4.3 Diagrams for Subshifts and Completeness

The graphical language **Z-Trans** is a variant of **Trans**.
Its definition and equational theory (without simulation
principle) are exactly the same, up to changing **thick blue** into **thick red** and applying the substitution on the
right

<figure><img src="image_12.png" /></figure>

We refer to Appendix D.2 for an explicit definition. Adapting the simulation principle is
more complex, so we will treat it explicitly in the core of this paper. We write $\llbracket - \rrbracket$ for its
semantics, going from **Z-Trans** to **Z-Rel**, which is simply “removing the color and adding
a _Z everywhere”. The explicit definition of this semantics is given in Figure 22. As in
the finite case, even without a simulation principle, we have a quasi-normal form and our
language is universal for sofic relations, see Appendices D.4 and D.5 for the exact statement.

Adapting the simulation principle to this infinite case is non-trivial, as we cannot simply
remove the preconditions that acted on *I* and *F* and expect the equation to be sound. We
propose in Figure 6 some relatively complex preconditions.

<figure><img src="image_13.png" /><figcaption>Figure 6: Simulation Principle for Bi-Infinite Words, and an Equation Deducible from it.</figcaption></figure>

Informally, the second precondition means that any state of the Z-transducer (*T*, *A*, *B*, *D*)
that is the start of a path of size *card*(*D*) (hence a loop must exists, hence it is the start
of an infinite path) must be in the domain of *S*. Conversely, the third precondition means
that any state of the Z-transducer (*R*, *A*, *B*, *C*) that is the end of a path of size *card*(*C*)
(hence a loop must exists, hence it is the end of an infinite path) must be in the codomain
of *S*. We note that most of the time this equation is used in the case where *S* is a total and
surjective relation (that is *S*<sup>-1</sup>(*C*) = *D* and *S*(*D*) = *C*), which automatically satisfies the
second and third preconditions. Like in the finite case, we can derive from the simulation
principle one of the well-known equations of trace monoidal categories. The only missing
equation to obtain a trace monoidal category is that adding a feedback loop to γ<sub>A,A</sub> yields
the identity **id**<sub>A</sub> (which would require to remove the “shift” from our feedback). We can
now state the completeness theorem.

**Theorem 4.6 (Completeness).** For **R** and **T** two diagrams of **Z-Trans** from **A** to **B**. If
$\llbracket \mathbf{R} \rrbracket = \llbracket \mathbf{T} \rrbracket$, we can rewrite **R** into **T** by using only the rules of **Z-Trans** and Figure 6.

While the proof still relies on the uniqueness of minimal deterministic automatons, two
differences are notable: (1) Our “automaton” is now a presentation of a sofic subshift,
meaning that we rely on Theorem 4.4 instead of the usual theorem about uniqueness of the
minimal automaton. (2) Before the determinization step, we need to prune all the states of
the presentation that are not part of any bi-infinite path.

5 Conclusion

The diagrammatical axiomatization presented in this paper presents many similarities with recent works also relying on feedback loops to represent internal state space. There was a thread of work aiming to handle diagrammatically streams of data, first [SK19] in the classical case and then [DFR22] and [CDP21] in the probabilistic and quantum cases. Our simulation principle bears similarity with equations appearing in [GKS22]. In [PZ+21], the authors provide a complete diagrammatical theory for finite automata with similar goals, however the structure or the categories involved is very different as they do not use the cartesian product as monoidal structure. However, we do not know of any attempt to handle subshifts with such formalism. Unifying transducers and sofic subshifts with similar graphical languages opens many research directions towards diagrammatical proofs in symbolic dynamics. We present a few of them.

**Subshifts on $N$** A straightforward next step would be to consider the situation in-
between finite and bi-infinite words. Indeed, this would allow to draw interesting bridges
between symbolic dynamics on the half-line, Buchi automata and LTS with initial states.
This direction would also allow easier comparison with the monoidal stream line of research.

**One-dimensional SFTs** One of the most natural objects of symbolic dynamics are subshift of finite type (SFTs), defined by a finite number of local constraints. Surprisingly, their diagrammatical definition is less straightforward than sofic ones. The logical next step would be to define SFTs diagrammatically and use this language to show classical results linking sofic subshifts, SFTs and cellular automata.

**Symbolic dynamics on groups** Symbolic dynamics also studies infinite colorings of $Z^2$ and more generally Cayley graphs of finitely generated groups. Diagrammatical proofs seem promising to tackle this since they seem to abstract the topology of the graph, "hidden" in the shift relation. This would suggest that some diagrammatical one-dimensional proof techniques may be adapted to higher dimensions and groups quite straightforwardly.

**General induction principle** Many objects in symbolic dynamics have a coinductive definition (substitutive subshifts, limit sets of cellular automata, ...). Generalizing our simulation principle to more abstract categories could provide new proofs techniques usable for all these co-inductive objects in an abstract way.

Finally, abstracting our diagrams to other settings/categories than relations may also
allow us to study other problems such as counting subshifts, studying ergodic probability
measures, and defining a notion of quantum subshifts.

References

[BSZ14] Filippo Bonchi, Paweł Sobociński, and Fabio Zanasi. “A categorical semantics of signal flow graphs”. In: *International Conference on Concurrency Theory*. Springer. 2014, pp. 435–450.

[BSZ21] Filippo Bonchi, Paweł Sobociński, and Fabio Zanasi. “A survey of compositional signal flow theory”. In: *Advancing Research in Information and Communication Technology: IFIP’s Exciting First 60+ Years, Views from the Technical Committees and Working Groups* (2021), pp. 29–56.
[CDP21] Titouan Carette, Marc De Visme, and Simon Perdrix. "Graphical language with delayed trace: Picturing quantum computing with finite memory". In: *2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*. IEEE. 2021, pp. 1–13.

[CM24] Titouan Carette and Etienne Moutot. *Aperiodicity in Quantum Wang Tilings*. 2024. arXiv: 2302.04503 [quant-ph]. URL: https://arxiv.org/abs/2302.04503.

[DFR22] Elena Di Lavore, Giovanni de Felice, and Mario Román. "Monoidal streams for dataflow programming". In: *Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science*. 2022, pp. 1–14.

[EM65] Calvin C. Elgot and Jorge E. Mezei. "On Relations Defined by Generalized Finite Automata". In: *IBM J. Res. Dev.* 9.1 (1965), pp. 47–68. DOI: 10.1147/RD.91.0047. URL: https://doi.org/10.1147/rd.91.0047.

[GKS22] Dan R Ghica, George Kaye, and David Sprunger. "A Fully Compositional Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic Semantics". In: *arXiv preprint arXiv:2201.10456* (2022).

[HMU07] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. *Introduction to automata theory, languages, and computation, 3rd Edition*. Pearson international edition. Addison-Wesley, 2007. ISBN: 978-0-321-47617-3.

[KL80] G.M. Kelly and M.L. Laplaza. "Coherence for compact closed categories". In: *Journal of Pure and Applied Algebra* 19 (1980), pp. 193–213. ISSN: 0022-4049. DOI: https://doi.org/10.1016/0022-4049(80)90101-2. URL: https://www.sciencedirect.com/science/article/pii/0022404980901012.

[KSW02] Katis, P., Sabadini, Nicoletta, and Walters, Robert F.C. "Feedback, trace and fixed-point semantics". In: *RAIRO-Theor. Inf. Appl.* 36.2 (2002), pp. 181–194. DOI: 10.1051/ita:200209. URL: https://doi.org/10.1051/ita:200209.

[LM21] D. Lind and B. Marcus. *An introduction to symbolic dynamics and coding*. 2nd ed. Cambridge University Press, 2021. ISBN: 9781108899727. DOI: 10.1017/9781108899727. URL: https://doi.org/10.1017/9781108899727.

[LV95] Nancy Lynch and Frits Vaandrager. "Forward and backward simulations". In: *Information and Computation* 121.2 (1995), pp. 214–233.

[Mac98] Saunders Mac Lane. *Categories for the working mathematician*. English. 2nd ed. Vol. 5. Grad. Texts Math. New York, NY: Springer, 1998. ISBN: 0-387-98403-8.

[PZ+21] Robin Piedeleu, Fabio Zanasi, et al. "A String Diagrammatic Axiomatisation of Finite-State Automata". In: *FoSSaCS*. 2021, pp. 469–489.

[Sel11] Peter Selinger. "A survey of graphical languages for monoidal categories". In: *New structures for physics* (2011), pp. 289–355.

[Sip97] Michael Sipser. *Introduction to the theory of computation*. PWS Publishing Company, 1997. ISBN: 978-0-534-94728-6.

[SK19] David Sprunger and Shin-ya Katsumata. "Differentiable causal computations via delayed trace". In: *2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*. IEEE. 2019, pp. 1–12.

[Wet20] John van de Wetering. "ZX-calculus for the working quantum computer scientist". In: *arXiv preprint arXiv:2012.13966* (2020).
<figure><img src="image_14.png" /><figcaption>Figure 7: Equations for a Strict Symmetric Monoidal Category.</figcaption></figure>

<figure><img src="image_15.png" /><figcaption>Figure 8: Equations for the Cup and Cap</figcaption></figure>

A The Category of Relations

All the diagrams of Section 2 can actually be formalized using string diagrams from category
theory [Mac98]. Indeed, finite sets and relations is well known to be a strict symmetric
monoidal category, called **FinRel**, that is:

• A set of objects (finite sets).

* A binary operation on objects (the Cartesian product ×) which is associative and has a neutral element (1).

* A set of morphisms between those objects (relations), a way to compose them (the usual composition ◦) that is associative and has a neutral element (the identity **id**).

* A binary operations on morphisms (the Cartesian product of relations ×) which is associative, has a neutral element (**id**₁), and is a bifunctor (see the last equation of Figure 7).

* For every two objects *A* and *B*, a morphism that swaps them ($\gamma_{A,B}$) which forms a natural isomorphism (third and fourth equations of Figure 7).

We list all the resulting equations in Figure 7, both in text and diagrams. In those diagrams,
gray boxes correspond to "bracketing", and the overall consequence of those equations is
that we can keep the bracketing implicit.
If we account for the cup and cap, relations form a compact closed category (where additionally all the objects are self-duals) [KL80], which correspond to the additional equations listed in Figure 8.

# B Proofs for Finite Words

## B.1 Composing Transducers

In this section, we prove Proposition 3.1 by showing that we can compose and make a product of transducers.

Given two transducers $(\mathcal{T}, A, B, Q, I, F)$ and $(S, C, D, P, J, G)$, we can build their product as $(\mathcal{R}, A \times C, B \times D, Q \times P, I \times J, F \times G)$ where $((a, c), (q, p)) \mathcal{R} ((b, d), (q', p'))$ whenever $(a, q) \mathcal{R} (b, q')$ and $(c, p) \mathcal{R} (d, p')$. Its behavior is exactly the product of the two behaviors. Assuming $B = C$, we can build their composition as $(\mathcal{U}, A, D, Q \times P, I \times J, F \times G)$ where $(a, (q, p)) \mathcal{U} (d, (q', p'))$ whenever there exists $b \in B$ such that $(a, q) \mathcal{R} (b, q')$ and $(b, p) \mathcal{R} (d, p')$. Its behavior is exactly the composition of the two behaviors.

## B.2 From Transducers to Graphical Representation

In this section, we prove Proposition 3.2, that is for every transducer $(\mathcal{T}, A, B, Q, I, F)$, its behavior can be obtained by lifting $\mathcal{T}$ and using the shift as follows:

$$A^* \xrightarrow{\substack{\mathcal{T}^* \\ \boxed{\phantom{\mathcal{T}^*}} \\ \multicolumn{2}{c}{\boxed{I|F}}}} B^* = A^* \xrightarrow{\boxed{\mathcal{L}(\mathcal{T}, A, B, Q, I, F)}} B^*$$

We write $\mathcal{R}$ for the left-hand-side. We take $w \in A^*$ and $v \in B^*$ of size $n$, and note that by definition of the composition of relations, $w \mathcal{R} v$ if and only there exists two words $u, t \in Q^*$ such that $(w, u) \mathcal{T}^* (v, t)$ and $u (\triangleright_I^{|F})^t t$.

Let us focus on the former, it is equivalent to, for every $1 \le k \le n$, $(w_k, u_k) \mathcal{T} (v_k, t_k)$, that is $u_k \xrightarrow{w_k} t_k$.

Let us focus on the latter, it is equivalent to the first letter of $u$ being in $I$, the last letter of $t$ being in $F$, and for all $1 \le k \le n$, $u_{k+1} = t_k$. Said otherwise, there exists a sequence $q_0, q_1, \dots, q_n \in Q$ such that $u = q_0 \dots q_{n-1}$, $t = q_1 \dots q_n$, $q_0 \in I$ and $q_n \in F$.

Coming back to the initial equivalence, we have $w \mathcal{R} v$ if and only if there exists a sequence $q_0, q_1, \dots, q_n \in Q$ such that $q_0 \in I$, $q_n \in F$, and for all $1 \le k \le n$, $q_{k-1} \xrightarrow{w_k} q_k$. Since this is exactly the definition of a run, we have that $w \mathcal{R} v$ if and only if $w \mathcal{L}(\mathcal{T}, A, B, Q, I, F) v$.

## B.3 Soundness of the Standard Equations

<figure><img src="image_16.png" /><figcaption>Figure 9: Generators of **Trans**.</figcaption></figure>

We start by recalling the generators of our language and all its equations in Figures 9 to 12. Then we formally define the semantics $\llbracket - \rrbracket : \mathbf{Trans} \to \mathbf{Rel}$ inductively on the syntax, as shown in Figure 13.

We now prove the soundness of the equational theory. The soundness of the equations stating that **Trans** is a strict symmetric monoidal category follows immediately from the
<figure><img src="image_17.png" /><figcaption>Figure 10: Equations for a Strict Symmetric Monoidal Category.</figcaption></figure>

<figure><img src="image_18.png" /><figcaption>Figure 11: Equations for a Feedback Category.</figcaption></figure>

fact that **Rel** is a strict symmetric monoidal category, so we only need to look at the equations of Figure 2. The top-left and bottom-left equations also follow from the fact that **Rel** is a strict symmetric monoidal category. The top-right is sound because $\triangleright_1^{|1|} = \text{id}_1$, and the bottom-right is sound because $\triangleright_C^{|I|} \times \triangleright_D^{|J|} = \triangleright_{C \times D}^{|I \times J|}$. $\square$

## B.4 Soundness of the Simulation Principle

We prove the soundness of the equation of Figure 4 with respect to $[[−]]$, that is, we want to prove the equation of Figure 14.

Since all the relations involved are uniform, we can make a case-by-case analysis on the size of the input words on $A^*$. This means we are now trying to prove the following for all $n \ge 0$:

<figure><img src="image_19.png" /></figure>

Then, using the hypothesis of Figure 14, we can rewrite $I$ into $S \circ J$, then move the $S$ through the $n$ copies of $R$ to transform them into $n$ copies of $T$, and lastly rewrite $S \circ F$ into $G$.

In the above proof, one could replace all the instances of $=$ by $\subseteq$, or all of them by $\supseteq$, this would yield a proof of soundness for the backward-simulation principle of Figure 15 or of the forward-simulation principle of Figure 16. $\square$
<figure><img src="image_20.png" /><figcaption>Figure 12: Equations for Faithfully Embedding **FinRel**.</figcaption></figure>

<figure><img src="image_21.png" /><figcaption>Figure 13: Inductive Definition of the Semantics $\llbracket - \rrbracket : \mathbf{Trans} \to \mathbf{UniRel}$.</figcaption></figure>

## B.5 Minimization of finite transducers

We provide the full proof of Proposition 3.8.

Using the logical reasoning as in Section 2, we can rewrite the equation as the following. We are looking at $\forall a \in A, \forall p \in Q, \forall \ell \in L_{A^*}$,

$$ 
\left( \exists q \in Q, \left( \begin{array}{l} (p \xrightarrow{a/D} q) \wedge (\ell = \{w \mid \exists f \in F, q \xrightarrow{w/D} f\}) \\ \phantom{(p \xrightarrow{a/D} q) \wedge (\ell = \{w \mid \exists f \in F, q \xrightarrow{w/D} f\}) \\ \Leftrightarrow} \\ \phantom{(p \xrightarrow{a/D} q) \wedge (\ell = \{w \mid \exists f \in F, q \xrightarrow{w/D} f\})} \left( \exists m \in L_{A^*}, \left( m = \{v \mid \exists f \in F, p \xrightarrow{v/D} f\} \wedge \left( m \xrightarrow{a/L_D} \ell \right) \right) \end{array} \right) \right) 
$$

Before studying either side of that equivalence, we note that since $p$ is accessible from the initial state, there exists a word $u \in A^*$ such that $i \xrightarrow{u/D} p$, hence $L_u = \{v \mid \exists f \in F, p \xrightarrow{v/D} f\}$.

We start by reformulating the second part of the equivalence. Since the formula for $m$ is given, we can remove the $\exists m$ and obtain $L_u \xrightarrow{a/L_D} \ell$. We can now use the definition of $L_D$ and simplify the later in $\ell = L_{ua}$.

We now look at the first part of the equivalence, since $\mathcal{D}$ is deterministic, $q$ is uniquely determined so we can remove the $\exists q$ and we obtain $\ell = \{w \mid \exists f \in F, \mathcal{D}(a,p) \xrightarrow{w/D} f\}$. Since $i \xrightarrow{u/D} p$, this is equivalent to $\ell = \{w \mid \exists f \in F, i \xrightarrow{u/D} f\}$, that is $\ell = L_{ua}$.

<figure><img src="image_22.png" /><figcaption>Figure 14: Semantics of the Simulation Principle for Finite Words.</figcaption></figure>
<figure><img src="image_23.png" /><figcaption>Figure 15: Backward-Simulation Principle for Finite Words.</figcaption></figure>

<figure><img src="image_24.png" /><figcaption>Figure 16: Forward-Simulation Principle for Finite Words.</figcaption></figure>

## B.6 Deducing the Sliding Equation

We prove that the equation from Figure 17 can be deduced from the others. For that, we start by using Proposition 3.3 on $\mathbf{R}$:

<figure><img src="image_25.png" /></figure>

We can then merge the two feedbacks into one, rewriting both sides of the equation we are trying to prove into:

<figure><img src="image_26.png" /></figure>

We then conclude using the simulation principle, using the following prerequisites:

<figure><img src="image_27.png" /></figure>

<figure><img src="image_28.png" /><figcaption>Figure 17: Deducible Equation.</figcaption></figure>
# C Proofs for the Sofic Subshifts

## C.1 Sofic subshifts and pruned factor-closed language

Here we present the proofs that where omitted in Section 4.2 and a few additional minor or intermediate results on the correspondence between sofic subshifts and pruned factor-closed languages.

First recall that, in Section 4.2, we define sofic subshifts as the subshifts whose factor language is regular. This may differ from the definition with which the reader is familiar with, as a more usual definition is that a subshift is sofic when it can be defined as the image of a SFT (subshift of finite type) by a cellular automaton.

Note that we deal here only with symbolic dynamics in dimension 1, that is the full shift is $A^Z$ for some finite alphabet $A$. Hence another definition of a sofic shift is a subshift $X$ which can be defined by a regular language $\mathcal{F}$ of forbidden words. Denote $A^* \cdot \mathcal{F} \cdot A^*$ the set of finite word containing a word in $\mathcal{F}$ as a factor subword. Now remark that the factor language of $X$ is precisely the complement of $A^* \cdot \mathcal{F} \cdot A^*$, since $\mathcal{F}$ is regular then $\mathrm{Fact}(X)$ is also regular. Conversely if $X$ is a subshift with regular factor language $\mathcal{L}$, then it can be defined as avoiding the complement of $\mathcal{L}$ which is also a regular language.

For the same considerations (though with a different terminology) one may refer to [LM21].

We can refine the factor relation $x \sqsubseteq y$ into $x \subset y$ by asking for the indexes to match. More precisely, for $u$ a finite word and $x$ a bi-infinite word, we write $\triangleright^k(u) \subset x$ whenever $u = x_{-k} \dots x_{-k+|u|-1}$. We remark that $\mathrm{d}(x, \triangleright^k(u)) = \sup\{\mathrm{d}(x, y) | y \in A^Z \text{ s.t. } \triangleright^k(u) \subset y\}$. *Remark C.1 (Comparing finite and infinite words)*. For simplicity we extend the distance $d$ to compare finite words and infinite words. However this does not define a metric on the mixed space $A^* \cup A^Z$.

The most rigorous approach to talk of a convergence of a sequence of finite words to an infinite word is that of cylinders.

The **cylinder** of word $u$ at position $k$, denoted by $[u]_k$, is the set of all bi-infinite words that coincide with $u$ at position $k$ that is

$$[u]_k := \{x \in A^Z | \forall 0 \le i < |u|, x_{i-k} = u_i\}$$

In our notation this corresponds to $[u]_k = \{x \in A^Z | \triangleright^k(u) \subset x\}$.

We call **domain** of a cylinder $[u]_k$ the integer interval $[-k, |u| - k - 1]$, and we denote it here by $\mathcal{D}([u]_k)$.

Given a family $(C_n)_{n \in \mathbb{N}}$ of cylinders, if $\mathcal{D}(C_n) \underset{n \to \infty}{\longrightarrow} \mathbb{Z}$, then there exists a sub-family $(C_{f(n)})_{n \in \mathbb{N}}$, for each $n$ a larger cylinder $C_{f(n)} \subset C'_n$ and an infinite word $x$ such that $\{x\} = \bigcap_{n \in \mathbb{N}} C'_n$.

In particular if $\mathcal{D}(C_n) \underset{n \to \infty}{\longrightarrow} \mathbb{Z}$ and for all $n$, $C_{n+1} \subseteq C_n$ then $\bigcap_{n \in \mathbb{N}} C_n = \{x\}$ for some bi-infinite word $x$.

The easiest case is when each cylinder is some $C_n = [u_n]_{k_n}$ such that $u_n \subseteq 1$ $u_{n+1}$ with $u_{n+1} = v \cdot u_n \cdot v'$, $|v| = k_{n+1} - k_n > 0$ and $|v'| > 0$. In this case we indeed have $\bigcap_{n \in \mathbb{N}} C_n = \{x\}$ which, outside this remark, we write $\triangleright^{k_n}(u_n) \underset{n \to \infty}{\longrightarrow} x$.

*Remark C.2 (Intersection of cylinders compared to limit of words)*. The notion of limit of words is a bit more permissive than that of intersection of cylinders. Take for example the sequence of word $u_n := 1 \cdot 0^{2n+1} \cdot 1$ and positions $k_n = n + 1$. We have $\triangleright^{k_n}(u_n) \underset{n \to \infty}{\longrightarrow} 0^Z$,
but $\bigcup_{n \in \mathbb{N}} [u_n]_{k_n} = \emptyset$. However, taking $v_n = 0^{2n+1}$ and $k'_n = n$, we have $[u_n]_{k_n} \subset [v_n]_{k'_n}$ as $u_n = 1 \cdot v_n \cdot 1$ and $\bigcap_{n \in \mathbb{N}} [v_n]_{k'_n} = \{0^\mathbb{Z}\}$.

We now prove Lemma 4.2 which states that any limit language $\vec{L}$ is a subshift.

*Proof of Lemma 4.2.* Let $L \subseteq A^*$. First remark that $\vec{L}$ is straightforwardly shift invariant, because if $x \in \vec{L}$ then by definition $x$ is some limit of $\triangleright^{k_n}(u_n)$ and simply shifting the sequence of indices by $k$ proves that $\triangleright^k(x)$ is in $\vec{L}$ as $\triangleright^{k+k_n}(u_n) \xrightarrow{n \to \infty} \triangleright^k(x)$.

Now we prove similarly that $\vec{L}$ is closed. Let $y \in A^\mathbb{Z}$ be the limit of a sequence $(x_n)_{n \in \mathbb{N}}$ of infinite words in $\vec{L}$. First let us remark that the sequence of central factors of $x_n$ also converges to $y$, that is $(x_n)_{-n} \cdots (x_n)_n \xrightarrow{n \to \infty} y$. Since $x_n \in \vec{L}$, it is the limit of some sequence $(\triangleright^{k_{n,m}} u_{n,m})_{m \in \mathbb{N}}$ where the $k_{n,m}$ are integers and $u_{n,m}$ words in $L$. Hence for each $n$ there exists $f(n)$ such that $\triangleright^{k_{n,f(n)}}(u_{n,f(n)})$ contains $(x_n)_{-n} \cdots (x_n)_n$ and we now have that $\triangleright^{k_{n,f(n)}}(u_{n,f(n)}) \xrightarrow{n \to \infty} y$. Hence $y$ is in $\vec{L}$ and so $\vec{L}$ is closed. $\square$

**Lemma C.3.** A regular language is factor-closed if and only if it is recognized by a finite automaton where all states are initial and final. Furthermore, all the states of the minimal automaton of a factor-closed language are final.

*Proof.* First given an automata $\mathcal{A}$ where all states are initial and final and a word $u$ recognized by $\mathcal{A}$, from an accepting run of $u$ in $\mathcal{A}$ we can directly read accepting runs for all factors of $u$, so the language recognized by $\mathcal{A}$ is factor-closed.

Now, we consider a factor closed regular language $L$. There exist a minimal deterministic automaton $\mathcal{A}$ recognizing $L$. As $L$ is factor closed and $\mathcal{A}$ is deterministic, every accessible and co-accessible state (i.e., on a path from an initial state to an accepting state) is accepting. By minimality, all states are accessible and co-accessible so all states are accepting. Now considering $\mathcal{A}'$ where all states are also initial states. $\mathcal{A}'$ also recognizes $L$. First we have that $L$ is included in the language recognized by $\mathcal{A}'$ because any accepting run in $\mathcal{A}$ is also accepting in $\mathcal{A}'$. Now we prove that the recognized language is exactly $L$. Let $u$ be a word accepted by $\mathcal{A}'$, it is accepted by a path starting on some state $q$, as $q$ is accessible in $\mathcal{A}$ there exist a word $v$ such that $v \cdot u$ is accepted on a path starting from an initial state $q_0$ of $\mathcal{A}$. Therefore $v \cdot u$ is in $L$, by factor closure $u$ is also in $L$. $\square$

**Lemma C.4 (Limit and pruning).** Given a language $L \subseteq A^*$, we have $\text{Fact}(\vec{L}) = \text{Fact}(\text{Prun}(L))$.

This result is quite natural as factors of limit words are precisely the words that have arbitrarily long left-and-right extensions in the language.

*Proof.* We prove this lemma by double inclusion. Let $L$ be a language. First we prove $\text{Fact}(\vec{L}) \subseteq \text{Fact}(\text{Prun}(L))$. Let $v \in \text{Fact}(\vec{L})$, that is there exists $x \in \vec{L}$ such that $v \subseteq x$, that is, there exists $k \in \mathbb{Z} \triangleright^k(v) \subset x$. By definition of $\vec{L}$, there exists two sequences $(u_n)_{n \in \mathbb{N}}$ of words in $L$ and $(k_n)_{n \in \mathbb{N}}$ of integers such that $\lim_{n \to \infty} \triangleright^{k_n}(u_n) = x$. Denote $k' = |k| + |v|$, by definition for any integer $l$ and for any word $v'$ such that $d(x, v') \le 2^{-k'-l}$ we have $x_{[-k'-l, k'+l]} \subseteq v'$ and since $v \subseteq x_{[-k', k']}$ we have $v \subseteq v'$ and the existence of $v_p, v_s$ of length at least $l$ such that $v_p v v_s = v'$. In particular as $(\triangleright^{k_n}(u_n))$ tends to $x$, there exists $n_0$ such that $d(\triangleright^{k_{n_0}}(u_{n_0}), x) \subseteq 2^{-k'}$ so that $v \subseteq u_{n_0} \in L$. Now repeat the same reasoning with $u_{n_0}$, and denote $k'' = |k_{n_0}| + |u_{n_0}|$. As $(\triangleright^{k_n}(u_n))$ tends to $x$, for any $l$ there exists $n$ such that we have
$d(\triangleright^{k_n}(u_n), x) \subseteq 2^{-k''-l}$ so that $u_{n_0} \subseteq u_n$ with a prefix $u_p$ and a suffix $u_s$ of length at least $l$ such that $u_p u_{n_0} u_s = u_n$. That is $v \subseteq u_{n_0}$ and $u_{n_0} \in \text{Prun}(L)$ so that $v \in \text{Fact}(\text{Prun}(L))$.

Now the second inclusion. Let $u \in \text{Fact}(\text{Prun}(L))$, that is $u \subseteq u' \in \text{Prun}(L)$. For simplicity assume that $|u'|$ is odd and denote $k' = \frac{|u'|-1}{2}$. That is, for any $n$ there exists $u_{p,n}, u_{s,n} \in A^{\ge n}$ such that $u_{p,n}u'u_{s,n} \in L$. Denote $k_n = |u_{p,n}| + k'$ and $u_n = u_{p,n}u'u_{s,n}$. By compactness of $A^Z$, $(\triangleright^{k_n}(u_n))$ admits a converging subsequence. Denote $x$ its limit, which by definition is in $\overrightarrow{L}$. Since $u'$ is at the center of each $\triangleright^{k_n}(u_n)$, more precisely $\triangleright^{k_n}(u_n)|_{[-k',k']} = u'$, so we have $u' \subseteq x$ and more precisely $x|_{[-k',k']} = u'$. So $u \subseteq u' \subseteq x$ and $u \in \text{Fact}(\overrightarrow{L})$. $\square$

**Definition C.1** (Orbit, closure). Given a set $X \subseteq A^Z$ we define its orbit $\mathcal{O}(X)$ as the set of all possible shifts of words in $X$, that is $\mathcal{O}(X) := \{\triangleright^k(x), k \in \mathbb{Z}, x \in X\}$.

We also define its orbit-closure $\text{cl}(\mathcal{O}(X))$ as the topological closure of its orbit.

As subshifts are precisely sets of bi-infinite words that are shift-invariant and closed, a set $X \subseteq A^Z$ is a subshift if and only if $X = \text{cl}(\mathcal{O}(X))$. And more generally $\text{cl}(\mathcal{O}(X))$ is the smallest subshift containing $X$.

**Lemma C.5.** For any set $X$ of infinite words we have $\overrightarrow{\text{Fact}(X)} = \text{cl}(\mathcal{O}(X))$.

*Proof.* Let $y \in \text{cl}(X)$, by definition there exists a sequence $(x_n)_{n \in \mathbb{N}}$ of elements of $\mathcal{O}(X)$ such that $x_n \xrightarrow{n \to \infty} y$, by definition there exists for each $n$, $x'_n \in X$ and $k_n \in \mathbb{Z}$ such that $x_n = \triangleright^{k_n}(x'_n)$. Denote $\triangleright^k(u_n) := x_n|_{[-n,n]}$, that is the central word on length $2n+1$ in $x_n$. We have for each $n$, $u_n$ in $\text{Fact}(X)$ as $u_n \subseteq x_n = \triangleright^{k_n}(x'_n)$, and we have by definition that $\triangleright^k(u_n) \xrightarrow{n \to \infty} y$ so that $y \in \overrightarrow{\text{Fact}(X)}$.

Conversely, let $y \in \overrightarrow{\text{Fact}(X)}$. There exists a sequence $(u_n)_{n \in \mathbb{N}}$ of words in $\text{Fact}(X)$ and a sequence $(k_n)_{n \in \mathbb{N}}$ of offsets such that $\triangleright^{k_n}(u_n) \xrightarrow{n \to \infty} y$. By definition for each $u_n$ there exists a $x_n \in \mathcal{O}(X)$ such that $\triangleright^{-|u_n|/2}(u_n) \subseteq x_n$. By definition of the distance on $A^Z$ the sequence $x_n$ also converges and to the same limit $y$. Hence $y$ is in $\text{cl}(\mathcal{O}(X))$. $\square$

**Lemma C.6.** For any set $X \subseteq A^Z$, $\text{Fact}(X)$ is pruned and factor-closed.

*Proof.* Let $X \subseteq A^Z$ and $L = \text{Fact}(X)$.

$L$ is factor closed, indeed for any $u \in L$, there exists $x \in X$ such that $u \subseteq x$ by definition of $\text{Fact}(-)$. For any $v \in L$ we have $v \subseteq u \subseteq x$ so $v \in \text{Fact}(x) \subseteq \text{Fact}(X) = L$. So we have $L = \text{Fact}(L)$.

$L$ is pruned, indeed for any $u \in L$, there exists $x \in X$ and $k \in \mathbb{Z}$ such that $\triangleright^k(u) \subseteq x$. Denote $k_n = k+n$ and $u_n = x_{-k-n} \dots x_{-k+|u|+n}$. For each $n$ we have $u_n \in \text{Fact}(x) \subseteq L$ and we have $u \subseteq_n u_n$. Hence $u \in \text{Prun}(L)$ and $L$ is pruned. $\square$

We now prove Proposition 4.3 which states that $\text{Fact}() : \mathcal{P}(A^Z) \to \mathcal{P}(A^*)$ is, when restricted from sofic subshifts to pruned factor-closed regular languages, is a bijection.

*Proof of Proposition 4.3.* In this proof we denote Sofic $\subseteq \mathcal{P}(A^Z)$ the set of sofic subshifts, Reg $\subseteq \mathcal{P}(A^*)$ the set of regular languages and $\text{Reg}_p^{\text{fc}} \subseteq \text{Reg}$ the set of factor-closed and pruned regular languages.

Let $L \in \text{Reg}_p^{\text{fc}}$, then by Lemma C.4, $\text{Fact}(\overrightarrow{L}) = \text{Fact}(\text{Prun}(L)) = L$.

Let $X \in$ Sofic, by Lemma C.5, $\overrightarrow{\text{Fact}(X)} = \text{cl}(\mathcal{O}(X)) = X$ and since $X$ is sofic, $\text{Fact}(\overrightarrow{\text{Fact}(X)}) = \text{Fact}(X)$ is regular. It is also pruned and factor-closed by Lemma C.6.

Therefore the restriction $\text{Fact}(-) : \text{Sofic} \to \text{Reg}_p^{\text{fc}}$ is bijective and its inverse is the restriction $\xrightarrow{\quad} : \text{Reg}_p^{\text{fc}} \to \text{Sofic}$. $\square$
## C.2 Characterization of the Behavior of a Transducer

We prove Lemma 4.5 which states that the behavior of the infinite transducer is the limit of the behavior of the corresponding finite transducer, that is $\mathcal{L}^{\mathbb{Z}}(\mathcal{T}, A, B, Q) = \overline{\mathcal{L}}(\mathcal{T}, A, B, Q, Q, Q)$.

*Proof of Lemma 4.5.* Let $(\mathcal{T}, A, B, Q)$ be a $\mathbb{Z}$-transducer.

Denote $X_{\mathcal{T}} \subset (A \times B)^{\mathbb{Z}}$ its behavior, that is $X_{\mathcal{T}} = \mathcal{L}^{\mathbb{Z}}(\mathcal{T}, A, B, Q)$. And $\mathcal{L}_{\mathcal{T}} \subset (A \times B)^*$ the behavior of the finite transducer $(\mathcal{T}, A, B, Q, Q, Q)$, that is $\mathcal{L}_{\mathcal{T}} = \mathcal{L}(\mathcal{T}, A, B, Q, Q, Q)$.

We prove $X_{\mathcal{T}} = \overrightarrow{\mathcal{L}_{\mathcal{T}}}.$

This holds because an infinite run in $(\mathcal{T}, A, B, Q)$ is precisely the limit of an increasing sequence of finite runs in $(\mathcal{T}, A, B, Q, Q, Q)$.

We prove that $\overrightarrow{\mathcal{L}_{\mathcal{T}}} \subseteq X_{\mathcal{T}}$. First recall that since all states are initial and final, $\mathcal{L}_{\mathcal{T}}$ is pruned and factor-closed. Hence any sequence $(\triangleright^{k_n}(u_n))_{n \in \mathbb{N}}$ of words in $\mathcal{L}_{\mathcal{T}}$ that converge to a bi-infinite word $x$ can be taken as strictly increasing that is $\triangleright^{k_n}(u_n) \subseteq \triangleright^{k_{n+1}}(u_{n+1})$. Take such a sequence $(\triangleright^{k_n}(u_n))$ in $\mathcal{L}_{\mathcal{T}}$. For each $n$, $u_n = (a_{n,0}, b_{n,0}) \dots (a_{n,k}, b_{n,k})$ admits a run in $(\mathcal{T}, A, B, Q, Q, Q)$ denote $u'_n$ the word in $(A \times B \times Q)$ such that for each $i$ we have $q_{n,i} \xrightarrow{\frac{b_n i}{a_{n,i}}} q_{n,i+1}$.

As $(A \times B \times Q)^{\mathbb{Z}}$ is compact, the sequence $(\triangleright^{k_n}(u'_n))_{n \in \mathbb{N}}$ has subsequence that converges to some bi-infinite word $y$. By hypothesis the projection of $y$ on the first two components of each letter is $x$ and $y$ is the trace of an infinite run in $(\mathcal{T}, A, B, Q)$ and hence $x \in X_{\mathcal{T}}$.

Now we prove the converse, that is $X_{\mathcal{T}} \subseteq \overrightarrow{\mathcal{L}_{\mathcal{T}}}$. Let $x = ((a_i, b_i))_{i \in \mathbb{Z}} \in X_{\mathcal{T}}$, there exists a sequence of states $(q_i)_{i \in \mathbb{N}}$ such that $\dots \xrightarrow{b_{i-1}} q_0 \xrightarrow{b_0} q_1 \xrightarrow{b_1} \dots \xrightarrow{a_1} q_n$ is a bi-infinite run in $(\mathcal{T}, A, B, Q)$. For each $n$, let $k_n = n$ and $u_n = (a_{-n}, b_{-n}) \dots (a_n, b_n)$ (the central subword of length $2n+1$ in $x$).

For each $n$ we have $q_{-n-1} \xrightarrow{b_{-n}} q_{-n} \dots \xrightarrow{b_n} q_n$ which is a run of $(\mathcal{T}, A, B, Q, Q, Q)$ of length $2n+1$. Hence $u_n \in \mathcal{L}_{\mathcal{T}}$. Therefore $x = \lim_{n \to \infty} \triangleright^{k_n}(u_n)$ is in $\overrightarrow{\mathcal{L}_{\mathcal{T}}}$.

□

## C.3 Uniqueness of the Minimal Rooted Right-Resolving Pruned Presentation

We recall that a presentation of a sofic subshift $X$ is simply a $\mathbb{Z}$-transducer with $\mathbb{1}$ for output alphabet, so we start by studying completeness in the case where $B = \mathbb{1}$. A presentation of a sofic subshift is:

**Pruned** if its language is pruned, meaning that for every word $w$ in the language, there exists $u$ and $v$ both non-empty such that $uwv$ is in the language.

**Right-Resolving** whenever its transition relation is a partial function.

**Rooted** whenever there exists a root state $r$ such that

* every accepted word admits an accepted run starting by $r$,

* and every state is accessible from $r$, meaning there is a run from $r$ to that state.

**Lemma C.7 (Pruned Presentation).** For any pruned presentation $(\mathcal{T}, A, Q)$ of the sofic subshift $X$, the language recognized by the presentation is exactly $\text{Fact}(X)$.
*Proof.* Let $L$ be the language recognized by $(\mathcal{T}, A, Q)$. By definition, we have $\vec{L} = X$. By Proposition 4.3, $L = \overline{\text{Fact}(\vec{L})} = \text{Fact}(X)$. $\square$

**Theorem C.8 (Uniqueness).** Every non-empty sofic subshift admits a unique minimal rooted right-resolving pruned presentation, up to isomorphism.

*Proof.* Given a sofic subshift $X$, let us consider the minimal deterministic automaton $(\mathcal{D}, A, Q, \{i\}, F)$ that recognizes $\text{Fact}(X)$. Within that automaton, we write $\xrightarrow{T}$ for the transitions, and $\xrightarrow{w/\mathcal{D}}$ for the iterated transitions.

If we take $w = w_1 \dots w_n \in \text{Fact}(X)$, it corresponds to a run from $i \xrightarrow{w/\mathcal{D}} f \in F$. Since $\text{Fact}(X)$ is factor-closed, we also have $w_1 \dots w_k \in \text{Fact}(X)$ for $0 \le k \le n$, and since $\mathcal{D}$ is deterministic it means that all the states of the run $i \xrightarrow{w/\mathcal{D}} f$ are also final states. This means that if we restrict our automaton to only its final states, so $(\mathcal{D}, A, F, \{i\}, F)$, then the language recognized is identical. Note that $\mathcal{D}$ is now a partial function (except in the case $\text{Fact}(X) = A^*$).

We now consider $q \in F$ and $u \in A^*$ such that there exists a $f \in F$ satisfying $p \xrightarrow{u/\mathcal{D}} f$. In the minimal deterministic automaton, every state is accessible (otherwise the automaton would not be minimal), so there exists $v \in A^*$ such that $i \xrightarrow{v/\mathcal{D}} q$, meaning that $vu \in \text{Fact}(X)$. Since $\text{Fact}(X)$ is factor-closed, this means that $u \in \text{Fact}(X)$, so there exists a run $i \xrightarrow{v/\mathcal{D}} p$ for some $p \in F$. This means that if we extend initial states to be $F$, so the non-deterministic automaton $(\mathcal{D}, A, F, F, F)$, then the language recognized is identical. Additionally, any word accepted by this automaton admits an accepting run that start with $i$, and every state is accessible from $i$. Said otherwise, $(\mathcal{D}, A, F)$ is a representation of the sofic subshift $\overline{\text{Fact}(X)}$, that is pruned, right-resolving and rooted in $i$. Using Proposition 4.3, $\overline{\text{Fact}(X)} = X$.

Now for uniqueness, we consider another minimal pruned right-resolving presentation $(\mathcal{M}, A, P)$, rooted in $r$. If $\mathcal{M}$ is already total (which only happens whenever $\text{Fact}(X) = A^*$), $(\mathcal{M}, A, P, \{r\}, P)$ is the minimal deterministic automaton recognizing $\text{Fact}(X)$. Assuming $\mathcal{M}$ is not a total function, we build a deterministic automaton $(\mathcal{M}_{\perp}, A, P \sqcup \{\perp\}, \{r\}, P)$ where $\mathcal{M}_{\perp}$ is the total function that extends $\mathcal{M}$ by adding a transition toward the new state $\perp$ whenever $\mathcal{M}$ would be undefined. This deterministic automaton recognizes the same language as the presentation, which according to Lemma C.7 is exactly $\text{Fact}(X)$. We argue it is the minimal deterministic automaton recognizing $\text{Fact}(X)$. Indeed, if we take a deterministic automaton recognizing $\text{Fact}(X)$ that is strictly smaller, then by following the same procedure we used above on $\mathcal{D}$ to make it a pruned right-resolving presentation, we would obtain one that is strictly smaller than $\mathcal{M}$, which contradict minimality.

In both cases, we have a minimal deterministic automaton that recognizes the same language as $(\mathcal{D}, A, P, \{i\}, F)$, so by uniqueness of the minimal automata (see [HMU07]) we have an isomorphism $\iota$ between the two. This directly induces an isomorphism between $(\mathcal{D}, A, F)$ and $(\mathcal{M}, A, P)$. $\square$
<figure><img src="image_29.png" /><figcaption>Figure 20: Equations for a Feedback Category.</figcaption></figure>

<figure><img src="image_30.png" /><figcaption>Figure 21: Equations for Faithfully Embedding FinRel.</figcaption></figure>

• The wires and every syntactical construct are in **thick red**, to distinguish them from actual relations. In particular, $\mathcal{R}$ refers to an actual relation while **R** refers to an element of our language.

• Double-line boxes denote the generator, while single-line boxes denote any diagram potentially constituted of many generators, including feedbacks.

• The arrows on the feedback are a reminder that those are not the same as the cup and cap of Section 2.

• Within Figure 20, the gray lines correspond to bracketing, and similarly to Figure 7 the overall consequences of those equations is that bracketing can be safely ignored.

• The equations of Figure 21 ensures that if a diagram does not contain any instance of the “feedback” generator, we can merge all the generators into a single double-line box.

• The current equational theory is incomplete, additional equations will be added in Figure 6 to obtain completeness.

In order to ensure that the equations are not contradictory<fnref n="11" />, we provide a semantics and prove soundness of our equations. The semantics is a strong symmetric monoidal functor from $\mathbb{Z}$-Trans to Rel, which we write $\llbracket - \rrbracket$, and is actually simply “removing the color and adding a $\mathbb{Z}$ everywhere”. We provide an explicit definition in Figure 22.

## D.3 Soundness of the Standard Equations

We now prove the soundness of the equational theory. Soundness means that if one rewrites a diagram **R** into **S** using any of the listed equations, we still have $\llbracket \mathbb{R} \rrbracket = \llbracket \mathbb{S} \rrbracket$. The soundness of the equation of Figure 19 follows immediately from the fact that **Rel** is a strict symmetric monoidal category, so we only need to look at the equations of Figure 20. The top-left and

<footnote n="11">¹¹Which would lead to the trivial category where all the diagrams are equal to one another.</footnote>
<figure><img src="image_31.png" /><figcaption>Figure 22: Inductive Definition of the Semantics $[\neg] : \mathbb{Z}\text{-Trans} \to \mathbb{Z}\text{-Rel}$.</figcaption></figure>

bottom-left equations also follow from the fact that **Rel** is a strict symmetric monoidal category. The top-right is sound because $\Delta_1 = \text{id}_1$, and the bottom-right is sound because $\Delta_C \times \Delta_D = \Delta_{C \times D}$. $\square$

## D.4 Quasi-Normal Form

We now explicitly state the generalization of Proposition 3.3 to the infinite case.

**Proposition D.1 (Quasi-Normal Form).** Any diagram of $\mathbf{R} \in \mathbb{Z}\text{-Trans}$ from $A$ to $B$ can be put in the following form for some finite set $Q$ and $\mathcal{T} \in \text{FinRel}$.

<figure><img src="image_32.png" /></figure>

*Proof.* We start by using the first equation of Figure 20 from right to left to push all the feedbacks at the bottom of the diagram. Then, we use the equations of Figure 21 to merge all the non-feedback into a single box. Lastly, we use the last equation of Figure 20 to merge all the feedbacks into a single feedback. $\square$

## D.5 Universality

We now explicitly state generalization of Theorem 3.4 to the infinite case.

**Theorem D.2 (Universality).** For any $S \in \mathbb{Z}\text{-Trans}$, $[\mathbf{S}]$ is a *sofic relation*. For any *sofic relation* $\mathcal{R}$, there exists $S \in \mathbb{Z}\text{-Trans}$ such that $[\mathbf{S}] = \mathcal{R}$.

*Proof.* It directly follows from Proposition D.1 and Proposition 4.1. $\square$

## D.6 Soundness of the Simulation Principle

<figure><img src="image_33.png" /><figcaption>Figure 23: Simulation Principle for Bi-Infinite Words, and an Equation Deducible from it.</figcaption></figure>
<figure><img src="image_34.png" /><figcaption>Figure 24: Backward-Simulation Principle for Bi-Infinite Words.</figcaption></figure>

<figure><img src="image_35.png" /><figcaption>Figure 25: Forward-Simulation Principle for Bi-Infinite Words.</figcaption></figure>

We start by proving the following compactness result. For any $Z$-transducer ($\mathcal{T}$, $A, B, Q$), we recall that by definition, we have $(a_n)_{n \in \mathbb{Z}} \mathcal{L}^{\mathbb{Z}}(\mathcal{T}, A, B, Q)$ $(b_n)_{n \in \mathbb{Z}}$ if and only if there exists $(q_n)_{n \in \mathbb{Z}}$ such that $\forall n \in \mathbb{Z}, (a_n, q_{n+1}) \mathcal{T} (b_n, q_n)$.

**Theorem D.3 (Compactness).** It is sufficient to only consider finite sequences, meaning that $(a_n)_{n \in \mathbb{Z}} \mathcal{L}^{\mathbb{Z}}(\mathcal{T}, A, B, Q)$ $(b_n)_{n \in \mathbb{Z}}$ if and only if there exists for all $N \le M \in \mathbb{Z}$ a finite sequence $(q_n^{N,M})_{N \le n \le M}$ such that $\forall N \le n < M \in \mathbb{Z}, (a_n, q_{n+1}^{N,M}) \mathcal{T} (b_n, q_n^{N,M})$.

*Proof.* The direct implication is trivial, as we simply take $q_n^{N,M} := q_n$. For the indirect implication, it is in fact enough to only consider the finite sequences centered on zero, that is $(q_n^{-N,N})_{-N \le n \le N}$ for $N \ge 0$, and ignore those that are not centered on zero. From them, we will define inductively $(q_n)_{n \in \mathbb{Z}}$. In order to do so, we add an additional induction hypothesis: there exists an infinite amount of $N \ge n$ such that $\forall -n \le k \le n$, $q_k^{-N,N} = q_k$.

We start by arbitrarily providing a total order $\le_Q$ over the finite set $Q$.

**Base Case:** We look at all the $q \in Q$ and check whether there exists an infinite amount of $N \ge 0$ such that $q_0^{-N,N} = q$. Since $Q$ is finite, there must exists a $q$ satisfying that condition. We take $q_0$ to be the minimal $q$ (for $\le_Q$) satisfying that condition.

**Inductive Case:** We assume that we have defined $q_{-n}, \dots, q_0, \dots, q_n$ such that:

* For all $-n \le k < n$, $(a_n, q_{n+1}) \mathcal{T} (b_n, q_n)$.

* There exists an infinite amount of $N \ge n$ such that $\forall -n \le k \le n$, $q_k^{-N,N} = q_k$.

We look at all the pairs $(q_{\ominus}, q_{\oplus}) \in Q^2$ and check whether there exists an infinite amount of $N \ge n+1$ such that $q_{-n-1}^{-N,N} = q_{\ominus}$ and $q_{n+1}^{-N,N} = q_{\oplus}$. Since $Q^2$ is finite, there must exists a pair $(q_{\ominus}, q_{\oplus})$ satisfying that condition. We take $(q_{-n-1}, q_{n+1})$ to be the minimal pair (for the lexicographic order) satisfying that condition. By definition, both induction hypothesis are preserved. $\square$

We start by proving the soundness of Figure 24 with respect to $\llbracket - \rrbracket$. We need to prove that if we consider $(a_n)_{n \in \mathbb{Z}} \mathcal{L}^{\mathbb{Z}}(\mathcal{R}, A, B, C)$ $(b_n)_{n \in \mathbb{Z}}$ then $(a_n)_{n \in \mathbb{Z}} \mathcal{L}^{\mathbb{Z}}(\mathcal{T}, A, B, D)$ $(b_n)_{n \in \mathbb{Z}}$.

Focusing on the right-hand-side, and using the above Theorem D.3, it is enough to show there exists for all $N \le M \in \mathbb{Z}$ a finite sequence $(d_n^{N,M})_{N \le n \le M}$ such that $\forall N \le n < M \in \mathbb{Z}, (a_n, d_{n+1}^{N,M}) \mathcal{T} (b_n, d_n^{N,M})$. Or, in diagrammatic terms, it is enough to show that the following
relation relates $(a_N, \dots, a_M)$ to $(b_N, \dots, b_M)$.

<figure><img src="image_36.png" /></figure>

Focusing on the left-hand-side, it means that there exists $(c_n)_{n \in \mathbb{Z}}$ such that $\forall n \in \mathbb{Z}$, $(a_n, c_{n+1}) \mathcal{T} (b_n, c_n)$. It implies that for $N \le M$, the following relation relates $(a_N, \dots, a_M)$ to $(b_N, \dots, b_M)$.

<figure><img src="image_37.png" /></figure>

Using the bottom precondition of Figure 24, we can replace the left part of the above diagram by $S \circ \bullet_D$ and the result relation would still relate $(a_N, \dots, a_M)$ to $(b_N, \dots, b_M)$. Then using the top precondition we can slide the $S$ toward the right and transform every $\mathcal{R}$ into a $\mathcal{T}$, and finally using that the full relation is maximal we can replace $\bullet_C \circ S$ by $\bullet_D$. The resulting relation still relates $(a_N, \dots, a_M)$ to $(b_N, \dots, b_M)$. $\square$

Proving the soundness of Figure 25 follows an identical proof, albeit mirrored. And the soundness of the simulation principle of Figure 23 follows from both the backward and forward principle. $\square$

## D.7 Deducing the Sliding Equation

We prove that the bottom equation from Figure 23 can be deduced from the others. For that, we start by using Proposition D.1 on $\mathbf{R}$:

<figure><img src="image_38.png" /></figure>

We can then merge the two feedbacks into one, rewriting both sides of the equation we are trying to prove into:

<figure><img src="image_39.png" /></figure>

We then conclude using the simulation principle, using the following prerequisites and the fact that $\bullet$ is the maximal relation for the inclusion:

<figure><img src="image_40.png" /></figure>
## D.8 Completeness of the Simulation Principle

The core idea of the proof is similar to the finite case, meaning we will determinize then minimize the presentation of our sofic subshift, except we have to start by pruning the states of our presentation that cannot be part of any bi-infinite path. Whenever we consider $(\mathcal{T}, A, Q)$ to be a presentation of sofic subshift, we write $\xrightarrow{\mathcal{T}}$ for the transitions within that presentation, and we write $\xrightarrow{w} \mathcal{T}$ with $w$ a finite word of size $k$ for the iterated transition $\xrightarrow{w_1} \cdots \xrightarrow{w_k} \mathcal{T}$.

**Definition D.1 (Forward-Pruning).** Let $(\mathcal{T}, A, Q)$ be a presentation of a sofic subshift. Its forward-pruning is the presentation $(\mathcal{T}, A, Q^{\to\infty})$, where $Q^{\to\infty}$ is the restriction of $Q$ to the states $q_0$ that are the start of an infinite path $q_0 \xrightarrow{a_1} \mathcal{T} \xrightarrow{a_2} \cdots$, or equivalently of a path of size at least $\text{card}(Q)$ as such a path necessarily loops, and where $\mathcal{T}$ has been restricted to $A \times Q^{\to\infty} \to Q^{\to\infty}$.

**Proposition D.4.** For all presentation of a sofic subshift $(\mathcal{T}, A, Q)$, we have

<figure><img src="image_41.png" /></figure>

where $\overline{=} : Q \to Q^{\to\infty}$ is the usual “equality” relation.

*Proof.* The first equation state that if $q_0$ is the start of an infinite path, and $q_{-1} \xrightarrow{a_0} \mathcal{T} \xrightarrow{a_1} q_0$, then $q_{-1}$ is also the start of an infinite path, which is true.

The second equation is trivially true as the right-hand-side simplifies to $\bullet_{Q \to \infty}$, which is maximal for the inclusion.

The third equation state that if $q_0$ is the start of a path of size $\text{card}(Q)$, then it is the start of an infinite path, which is true because a path of size $\text{card}(Q)$ necessarily loops. $\square$

**Corollary D.5.** For all presentation of a sofic subshift $(\mathcal{T}, A, Q)$, using Figure 6, we have

<figure><img src="image_42.png" /></figure>

**Definition D.2 (Backward-Pruning).** Let $(\mathcal{T}, A, Q)$ be a presentation of a sofic subshift. Its backward-pruning is the presentation $(\mathcal{T}, A, Q^{\to\infty})$, where $Q^{\to\infty}$ is the restriction of $Q$ to the states $q_0$ that are the end of an infinite path $\cdots \xrightarrow{a_{-1}} \mathcal{T} \xrightarrow{a_0} q_0$, or equivalently of a path of size at least $\text{card}(Q)$ as such a path necessarily loops, and where $\mathcal{T}$ has been restricted to $A \times Q^{\to\infty} \to Q^{\to\infty}$.
**Proposition D.6.** For all presentation of a sofic subshift $(\mathcal{T}, A, Q)$, we have

$$ \begin{array}{ccc} \begin{array}{c} A \\ \multicolumn{1}{c}{\text{---}} \\ Q \end{array} \underset{\mathcal{T}}{\rightarrow} \begin{array}{c} \boxed{\mathcal{T}} \\ \multicolumn{1}{c}{\text{---}} \\ Q \end{array} & = & Q \rightarrow \begin{array}{c} A \\ \multicolumn{1}{c}{\text{---}} \\ Q \end{array} \underset{\mathcal{T}}{\rightarrow} \begin{array}{c} \boxed{\mathcal{T}} \\ \multicolumn{1}{c}{\text{---}} \\ Q \end{array} \\ \\ Q \rightarrow \begin{array}{c} \boxed{Q} \\ \multicolumn{1}{c}{\text{---}} \\ Q \end{array} \supseteq Q \rightarrow \begin{array}{c} \boxed{\mathcal{T}} \\ \multicolumn{1}{c}{\text{---}} \\ Q \end{array} \rightarrow \begin{array}{c} \boxed{\mathcal{T}} \\ \multicolumn{1}{c}{\text{---}} \\ Q \end{array} \\ \\ \bullet \underset{\mathcal{T}}{\rightarrow} \boxed{Q} \supseteq \bullet \underset{\text{card}(Q)}{\boxed{\mathcal{T}}} \rightarrow \bullet \underset{\text{card}(Q)}{\boxed{\mathcal{T}}} \end{array} $$

where $\mathcal{T} = Q \rightarrow \mathcal{T} \rightarrow Q$ is the usual “equality” relation.

*Proof.* The first equation states that if $q_0$ is the end of an infinite path, and $q_0 \xrightarrow{a_1} \mathcal{T} \xrightarrow{q_1}$, then $q_1$ is also the end of an infinite path, which is true.

The second equation is trivially true as the left-hand-side simplifies to $\bullet_{Q \rightarrow \mathcal{T}}$, which is maximal for the inclusion.

The third equation states that if $q_0$ is the end of a path of size $\text{card}(Q)$, then it is the end of an infinite path, which is true because a path of size $\text{card}(Q)$ necessarily loops. $\square$

**Corollary D.7.** For all presentation of a sofic subshift $(\mathcal{T}, A, Q)$, using Figure 6, we have

$$ \begin{array}{ccc} \begin{array}{c} A \\ \multicolumn{1}{c}{\text{---}} \\ Q \end{array} \underset{\mathcal{T}}{\rightarrow} \begin{array}{c} \boxed{A} \\ \multicolumn{1}{c}{\text{---}} \\ B \end{array} & = & \begin{array}{ccc} \begin{array}{c} A \\ \multicolumn{1}{c}{\text{---}} \\ Q \end{array} \underset{\mathcal{T}}{\rightarrow} \begin{array}{c} \boxed{A} \\ \multicolumn{1}{c}{\text{---}} \\ B \end{array} & & \begin{array}{c} \boxed{A} \\ \multicolumn{1}{c}{\text{---}} \\ Q \end{array} \end{array} \end{array} $$

**Definition D.3 (Pruning).** Let $(\mathcal{T}, A, Q)$ be a presentation of a sofic subshift. Its pruning is the presentation $(\mathcal{T}, A, Q \xrightarrow{\infty} \infty)$, where $Q \xrightarrow{\infty} \infty$ is the restriction of $Q$ to the states $q_0$ that are on a bi-infinite path $\dots \xrightarrow{a_{-1}} q_{-1} \xrightarrow{a_0} q_0 \xrightarrow{a_1} q_1 \xrightarrow{a_2} \dots$, or equivalently at the middle of a path of size at least $2 \times \text{card}(Q)$ as such a path necessarily loops before and after $q_0$, and where $\mathcal{T}$ has been restricted to $A \times Q \xrightarrow{\infty} \mathcal{T} \xrightarrow{\infty} Q$.

**Lemma D.8.** *The pruning of a presentation is equal to the forward-pruning of its backward-pruning, or equivalently the backward pruning of its forward-pruning. The pruning of a representation is always a *pruned* representation.*

*Proof.* If a state $q_0$ is on a bi-infinite path $(q_n)_{n \in \mathbb{Z}}$, then all the states $q_n$ are on an bi-infinite path, so none of them will be removed by the forward-pruning or backward-pruning, meaning that $Q \xrightarrow{\infty} \infty \subseteq (Q \xrightarrow{\infty}) \xrightarrow{\infty}$. We then take $q_0 \in (Q \xrightarrow{\infty}) \xrightarrow{\infty}$, there is an infinite path $(q_n)_{n \le 0}$ in $(Q \xrightarrow{\infty}) \xrightarrow{\infty}$ that ends on $q_0$, and there is an infinite path $(q_n)_{n \ge 0}$ in $Q \xrightarrow{\infty}$ that starts with $q_0$. So $q_0 \in Q \xrightarrow{\infty} \infty$, hence $Q \xrightarrow{\infty} \infty = (Q \xrightarrow{\infty}) \xrightarrow{\infty}$. The same reasoning can be done to prove $Q \xrightarrow{\infty} \infty = (Q \xrightarrow{\infty}) \xrightarrow{\infty}$. $\square$

**Definition D.4 (Determinization).** Let $(\mathcal{T}, A, Q)$ be a pruned presentation of a non-empty sofic subshift. Its determinization is the **pruned right-resolving rooted** presentation $(\mathcal{P}_{\neq \emptyset}(\mathcal{T}), A, \mathcal{P}_{\neq \emptyset}^{\text{acc}}(Q))$. More precisely, we start by recalling that $\mathcal{P}_{\neq \emptyset}(Q)$ is the set of all non-empty subsets of $Q$. Since our subshift is non-empty, $Q \in \mathcal{P}_{\neq \emptyset}(Q)$. We use $x, y$ for elements of $Q$, and $X, Y$ for elements of $\mathcal{P}_{\neq \emptyset}(Q)$. Then, we define the partial function$^{12}$ $\mathcal{P}_{\neq \emptyset}(\mathcal{T}) : A \times \mathcal{P}_{\neq \emptyset}(Q) \rightarrow \mathcal{P}_{\neq \emptyset}(Q)$ as

$$ \mathcal{P}_{\neq \emptyset}(\mathcal{T})(a, X) = \{y \in Q \mid \exists x \in X, x \xrightarrow{a} y\} \text{ if it is non-empty (undefined otherwise)} $$

<footnote>$^{12}$We consider partial functions to be a special case of relations.</footnote>
We then consider the set $\mathcal{P}_{\neq \emptyset}^{\text{acc}}(Q)$ of subsets of $Q$ accessible by iteration of that function, starting from $Q$. We can now restrict $\mathcal{P}_{\neq \emptyset}(\mathcal{T})$ to a function $A \mapsto \mathcal{P}_{\neq \emptyset}^{\text{acc}}(Q) \to \mathcal{P}_{\neq \emptyset}^{\text{acc}}(Q)$. The root is simply $Q$, and every state is accessible from $Q$, by definition of $\mathcal{P}_{\neq \emptyset}^{\text{acc}}(Q)$.

**Proposition D.9.** For all pruned presentation of a non-empty sofic subshift $(\mathcal{T}, A, Q)$, we have

<figure><img src="image_43.png" /></figure>

where $\exists: \mathcal{P}_{\neq \emptyset}^{\text{acc}}(Q) \to Q$ is the usual “contains” relation, that is $X \ni x$ whenever $x \in X$.

*Proof.* In this proof, we write $\mathcal{P}(\mathcal{T})$ for the total function from $A \times \mathcal{P}(Q) \to \mathcal{P}(Q)$ which extends $\mathcal{P}_{\neq \emptyset}(\mathcal{T})$ as below, and note that $\mathcal{P}_{\neq \emptyset}(\mathcal{T})(a, X)$ is defined if and only if $\mathcal{P}(\mathcal{T})(a, X) \neq \emptyset$.

$$ \mathcal{P}(\mathcal{T})(a, X) = \{y \in Q \mid \exists x \in X, x \xrightarrow{a} \mathcal{T} y\} $$

Using the logical reasoning as in Section 2, we can rewrite the first equation as the following. We are looking at $\forall a \in A, \forall X \in \mathcal{P}_{\neq \emptyset}^{\text{acc}}(Q), \forall y \in Q,$

$$ (\exists x \in Q, (x \in X) \wedge (x \xrightarrow{a} \mathcal{T} y)) \Leftrightarrow (\exists Y \in \mathcal{P}_{\neq \emptyset}^{\text{acc}}(Q), (X \xrightarrow{a} \mathcal{P}_{\neq \emptyset}(\mathcal{T}) Y) \wedge (y \in Y)) $$

We start by reformulating the right side of the equivalence, as $\mathcal{P}_{\neq \emptyset}(\mathcal{T})$ is a partial function, we can replace the $\exists$ and obtain $(\mathcal{P}(\mathcal{T})(a, X) \neq \emptyset) \wedge (y \in \mathcal{P}_{\neq \emptyset}(a, X))$, which is equivalent to $y \in \mathcal{P}(\mathcal{T})(a, X)$. Then, using the definition of $\mathcal{P}(\mathcal{T})$, we obtain that it is equivalent to $\exists x \in X, x \xrightarrow{a} \mathcal{T} y$, which is exactly the left side of the equivalence.

The second and third equations are trivially true as their left-hand-side simplifies to
• $\mathcal{P}_{\neq \emptyset}^{\text{acc}}(Q)$ and •$Q$, which are maximal for the inclusion. $\square$

**Corollary D.10.** For all pruned presentation of a non-empty sofic subshift $(\mathcal{T}, A, Q)$, using Figure 4, we have

<figure><img src="image_44.png" /></figure>

**Definition D.5 (Minimization).** Let $(D, A, P)$ be a pruned right-resolving rooted presentation of a sofic subshift, and we write $r$ for its$^{13}$ root. Its minimization is the right-resolving rooted presentation $(L_D, A, L_{A^*}^{\neq \emptyset})$. More precisely, we write $L_w = \{v \in A^* \mid \exists f \in P, r \xrightarrow{wv} f\}$, and remark that whenever $L_w = L_u$, then for all $a \in A$ we also have $L_{wa} = L_{ua}$. We then define $L_{A^*}^{\neq \emptyset} = \{L_w \neq \emptyset \mid w \in A^*\}$ note that a single element of this

<footnote>$^{13}$While it is possible for that presentation to have multiple roots, choosing a different root have no influence on this minimization, as the $L_w$ defined would be identical.</footnote>
**Proof.** We start two diagrams **R**, **S** of Z-Trans from **A** to **B** and assume [[**R**]] = [[**S**]]. We start by focusing on **R**. We combine it with the cup $\epsilon_B$ to bend its output into an input, and we then use Proposition D.1 to put the result in normal form:

$$ B \xrightarrow[\text{A}]{\text{B}} \text{R} \xrightarrow[\text{A}]{\text{B}} \text{S} \quad = \quad B \times \text{A} \xrightarrow[\text{Q}]{\text{T}} \text{Q} $$

Then, we use Corollaries D.5 and D.7 on $\mathcal{T}$ to prune it, and we distinguish two cases.

**Case 1:** If [[**R**]] is the empty relation, then the result of the pruning is empty, meaning that:

$$ B \xrightarrow[\text{A}]{\text{B}} \text{R} \xrightarrow[\text{A}]{\text{B}} \text{S} \quad = \quad B \times \text{A} \xrightarrow{\emptyset} \text{R} \xrightarrow{\emptyset} \text{S} $$

We can do the same for $\mathcal{S}$, which leads to

$$ B \xrightarrow[\text{A}]{\text{B}} \text{R} \xrightarrow[\text{A}]{\text{B}} \text{S} \quad = \quad B \xrightarrow[\text{A}]{\text{B}} \text{R} \xrightarrow[\text{A}]{\text{B}} \text{S} $$

By combining with the cap $\eta_B$ to bend the input **B** into an output, and using the fact that $(\text{id}_B \times \epsilon_B) \circ (\eta_B \times \text{id}_B) = \text{id}_B$, we obtain **R** = **S**.

**Case 2:** If [[**R**]] is non-empty, then the result of the pruning is non-empty. We can continue and use Corollary D.10 on $\mathcal{T}$ followed by Corollary D.12 on $\mathcal{P}(\mathcal{T})$ to obtain:

$$ B \xrightarrow[\text{A}]{\text{B}} \text{R} \xrightarrow[\text{A}]{\text{B}} \text{S} \quad = \quad L_{(\text{B} \times \text{A}) \cdot}^{\neq \emptyset} L_{(\mathcal{P}(\mathcal{T}) \times \text{A}) \cdot}^{\neq \emptyset} $$

For convenience, we name $(\mathcal{R}_M, B \times A, Q_M)$ the resulting minimal representation. We do the same for $\mathcal{S}$ and write $(\mathcal{S}_N, B \times A, Q_N)$ for the resulting minimal representation. Since [[**R**]] = [[**S**]] and by soundness of the equations, we obtain that:

$$ \left[ \begin{array}{ccc} B \times A & \text{R}_M & Q_M \\ \searrow & \swarrow & \searrow \\ Q_M & \text{R}_M & Q_M \end{array} \right] = \left[ \begin{array}{ccc} B \times A & \mathcal{S}_N & Q_N \\ \searrow & \swarrow & \searrow \\ Q_N & \mathcal{S}_N & Q_N \end{array} \right] $$

Using the definition of [[**-**]] and Proposition 4.1, it follows that $(\mathcal{R}_M, B \times A, Q_M)$ and $(\mathcal{S}_N, B \times A, Q_N)$ represent the same subshift, hence by uniqueness of the minimal (pruned right-resolving rooted) representation of Theorem C.8, we obtain that both representations are equal up to an isomorphism $\iota: Q_M \to Q_N$, hence using the simulation principle with this $\iota$, we obtain

$$ B \times A \xrightarrow[Q_M]{\text{R}_M} Q_M \quad = \quad B \times A \xrightarrow[Q_N]{\mathcal{S}_N} Q_N $$

Which leads to

$$ B \xrightarrow[\text{A}]{\text{B}} \text{R} \xrightarrow[\text{A}]{\text{B}} \text{S} \quad = \quad B \xrightarrow[\text{A}]{\text{B}} \text{R} \xrightarrow[\text{A}]{\text{B}} \text{S} $$

By combining with the cap $\eta_B$ to bend the input **B** into an output, and using the fact that $(\text{id}_B \times \epsilon_B) \circ (\eta_B \times \text{id}_B) = \text{id}_B$, we obtain **R** = **S**. $\square$