all have a left-gcd that is unique up to invertibles on the right. Thanks to Lemma 4.16, Theorem 2.12 then tells us that the minimal $M$-transducer recognizing a $(\mathbf{KI}(\mathcal{T}_M), 1, 1)$-language $\mathcal{L}$ always exists (and it is given by Corollary 4.20), but it does not tell us how to compute it (in finite time). This section thus discusses two algorithms for computing the minimal transducer, respectively instantiating Algorithms 1 and 2: the first one takes as input two oracles $\text{EVAL}_\mathcal{L}$ and $\text{EQUIV}_\mathcal{L}$ and learns $\text{Min}_\mathcal{L}$ (Section 5.1), while the second one takes as input any finite transducer recognizing $\mathcal{L}$ and transforms it into $\text{Min}_\mathcal{L}$ (Section 5.2). The right-noetherianity of $M$ guarantees that these algorithms will terminate when the minimal transducer has finite state-set:

**Lemma 5.1.** An object $X$ of $\mathbf{KI}(\mathcal{T}_M)$ is $M$-noetherian if and only if it is a finite set, in which case $\text{length}_{\mathcal{M}}(m : Y \to X) = |X| - |Y|$.

**Lemma 5.2.** An object $X$ of $\mathbf{KI}(\mathcal{T}_M)$ is $\mathcal{E}$-artinian if and only if it is a finite set and either $M$ is right-noetherian or $X = \emptyset$, in which case $\text{colength}_{\mathcal{E}}(e : X \dasharrow Y) = |X| - |Y| + \text{rk } e$ where $\text{rk } e = \sum_{e(x)=(v,y)} \text{rk } v$.

Given a function $\Lambda \in (M + 1)_*^I$, we write $\text{rk } \Lambda = \text{rk}(\text{lgcd } \Lambda)$ and, finally, given a transducer $\mathcal{A}$, we then write $\text{rk } \mathcal{A} = \sum_{s \in (\text{Total } \mathcal{A})(\text{st})} \text{rk } \mathcal{L}_s$, $|\mathcal{A}|_{\text{st}}$ for the cardinal of the state-set of $\mathcal{A}$, and $|\mathcal{A}|_{\to}$ for the number of transitions $s \odot a \neq \perp$ in $\mathcal{A}$. We will use these notions to express the complexity of our algorithms.

These two algorithms are modular in $M$: they only require to be given functions computing basic operations and may then be implemented the same no matter the structure of $M$. Hence we also assume that we are given access to the following oracles: one that checks for equality in $M$; $\otimes : M + 1 \to M + 1 \to M + 1$ that computes the product in $M + 1$ (with $v \perp = \perp v = \perp$); $\wedge : M + 1 \to M + 1 \to M + 1$ that computes a left-gcd of two elements of $M + 1$ (with $v \wedge \perp = \perp \wedge v = \perp$); $\text{LEFTDIVIDE}$ that takes as input $\delta, v \in M$ and computes a $v \in M$ such that $v = \delta v$ (or outputs $v = \perp$ when $v = \perp$) or fails when there is no such $v$; and $\text{UPTOINVLEFT}$ that takes as input two families $v, v \in M^I$ indexed by a finite set $I$ and outputs a $\chi \in M^\times$ such that $v = \chi v$ if such a $\chi$ exists, and $\perp$ otherwise. Note that when $M$ is right-cancellative this last oracle may be derived from another oracle that only tests for equality up to invertibles of two elements of $M$ (and not two families), and when $M$ has no non-trivial invertible elements these two oracles just test for equality.

## 5.1. Learning

In this section, we thus first describe an algorithm that, given a subsequential function $\mathcal{L}$, learns $\text{Min}_\mathcal{L}$ using two oracles: $\text{EVAL}_\mathcal{L}$ takes as input a word $w \in A^*$ and computes $\mathcal{L}(\vdash w \triangleleft)$; and $\text{EQUIV}_\mathcal{L}$ takes as input a transducer $\mathcal{A}$, decides whether it recognizes $\mathcal{L}$, and if not outputs a counter-example word $w \in A^*$ such that $(\mathcal{A} \circ \iota)(\vdash w \triangleleft) \neq \mathcal{L}(\vdash w \triangleleft)$.

When $M$ is a free monoid, Vilar gives a very natural generalization of Angluin's $L^*$ algorithm for learning automata that does exactly this [1, 29]. Here we generalize Vilar's algorithm to arbitrary $M$ by instantiating Algorithm 1 within $\mathbf{KI}(\mathcal{T}_M)$: we get Algorithm 4. This instantiation is possible because the conditions on $M$ also guarantee
the existence of the minimal biautomata described in Section 2.3. To the best of the author's knowledge, no other algorithm in the literature solves the problem of learning transducers whose output monoid is not free.

**Algorithm 4** is very similar to Vilar's algorithm, the main difference being that the longest common prefix is now the left-gcd and that, in some places, testing for equality is now testing for equality up to invertibles on the left. It thus maintains two sets $Q$ and $T$ that are respectively prefix-closed and suffix-closed, and tables $\Lambda: Q \times (A \cup \{e\}) \to M + 1$ and $R: Q \times (A \cup \{e\}) \times T \to M + 1$. They satisfy that, for all $a \in A \cup \{e\}$, $\Lambda(q, a)R(q, a, t) = \mathcal{L}(\triangleright qat\triangleleft)$ and $R(q, a, \cdot)$ is left-coprime (hence $\Lambda(q, a)$ is a left-gcd of $(\mathcal{L}(\triangleright qat\triangleleft))_{t \in T}$).

The algorithm then extends $Q$ and $T$ until some closure and consistency conditions are satisfied, and then build a hypothesis transducer $\mathcal{H}(Q, T)$ using $\Lambda$ and $R$: its state-set $S$ can be constructed by, starting with $e \in Q$, picking as many $q \in Q$ so that $R(q, e, \cdot)$ is never $\perp^T$ and so that, for any two distinct $q, q' \in S$, $R(q, e, \cdot)$ and $R(q', e, \cdot)$ are not equal up to invertibles on the left; it then has initial state $e \in Q$, initialization value $\Lambda(e, e)$, termination function $t = q \in S \mapsto R(q, e, e)$ and transition function given by $q \odot a = (\text{LEFTDIVIDE}(\Lambda(q, e), \Lambda(q, a))\chi, q')$ for $q, q' \in S$ such that $R(q, a, \cdot) = \chi R(q', e, \cdot)$. The algorithm then adds the counter-example given by $\text{EQUIV}_L(\mathcal{H}(Q, T))$ to $Q$ and builds a new hypothesis automaton until no counter-example is returned and $\mathcal{H}(Q, T) = \text{Min } \mathcal{L}$. The three kinds of consistency issues that arise are again explained by the quaternary factorization system of Section 4.4, as the three conditions on line 10 hold when some morphism respectively does not belong to Tot, belongs to Tot but not Inv or belongs to Tot $\cap$ Inv but not Inj.

**Theorem 5.3.** *Algorithm 4 is correct and terminates as soon as $\text{Min } \mathcal{L}$ has finite state-set and $M$ is right-noetherian. It makes at most $3|\text{Min } \mathcal{L}|_{\text{st}} + \text{rk}(\text{Min } \mathcal{L})$ updates to $Q$ (lines 8 and 14) and at most $\text{rk}(\text{Min } \mathcal{L}) + |\text{Min } \mathcal{L}|_{\text{st}}$ updates to $T$ (line 10).*

**Algorithm 4** also differs from Vilar's original learning algorithm in a small additional way: the latter also keeps track of the left-gcds of every $\Lambda(q, \tilde{a})$ where $\tilde{a}$ ranges over $A \cup \{e\}$ and $q \in Q$ is fixed, and checks for consistency issues accordingly. This is a small optimization of the algorithm that does not follow immediately from the categorical framework. In Section 1 we thus actually provided an example run of our version of the algorithm when the output monoid is a free monoid. It also provides example runs of our algorithm for non-free output monoids, as quotienting the output monoid will only remove closure and consistency issues and make the run simpler. For instance letting $\alpha$ commute with $\beta$ for the transducer of Figure 1a would have removed the closure issue and the need to add $a$ to $Q$ while learning the corresponding monoidal transducer, and letting $\alpha$ also commute with $\gamma$ would have removed the first consistency issue to arise and the need to add $a$ to $T$.

## 5.2. Minimization

To transform a transducer $\mathcal{A} = (S, (u_0, s_0), t, \odot)$ recognizing $\mathcal{L}$ into $\text{Min } \mathcal{L}$, a first method is of course to use Algorithm 4, implementing $\text{EVAL}_\mathcal{L}$ using $\mathcal{A}$ and $\text{EQUIV}_\mathcal{L}$ by trying
the existence of the minimal biautomata described in Section 2.3. To the best of the author's knowledge, no other algorithm in the literature solves the problem of learning transducers whose output monoid is not free.

**Algorithm 4** is very similar to Vilar's algorithm, the main difference being that the longest common prefix is now the left-gcd and that, in some places, testing for equality is now testing for equality up to invertibles on the left. It thus maintains two sets $Q$ and $T$ that are respectively prefix-closed and suffix-closed, and tables $\Lambda: Q \times (A \cup \{e\}) \to M + 1$ and $R: Q \times (A \cup \{e\}) \times T \to M + 1$. They satisfy that, for all $a \in A \cup \{e\}$, $\Lambda(q, a)R(q, a, t) = \mathcal{L}(\triangleright qat\triangleleft)$ and $R(q, a, \cdot)$ is left-coprime (hence $\Lambda(q, a)$ is a left-gcd of $(\mathcal{L}(\triangleright qat\triangleleft))_{t \in T}$).

The algorithm then extends $Q$ and $T$ until some closure and consistency conditions are satisfied, and then build a hypothesis transducer $\mathcal{H}(Q, T)$ using $\Lambda$ and $R$: its state-set $S$ can be constructed by, starting with $e \in Q$, picking as many $q \in Q$ so that $R(q, e, \cdot)$ is never $\perp^T$ and so that, for any two distinct $q, q' \in S$, $R(q, e, \cdot)$ and $R(q', e, \cdot)$ are not equal up to invertibles on the left; it then has initial state $e \in Q$, initialization value $\Lambda(e, e)$, termination function $t = q \in S \mapsto R(q, e, e)$ and transition function given by $q \odot a = (\text{LEFTDIVIDE}(\Lambda(q, e), \Lambda(q, a))\chi, q')$ for $q, q' \in S$ such that $R(q, a, \cdot) = \chi R(q', e, \cdot)$. The algorithm then adds the counter-example given by $\text{EQUIV}_\mathcal{L}(\mathcal{H}(Q, T))$ to $Q$ and builds a new hypothesis automaton until no counter-example is returned and $\mathcal{H}(Q, T) = \text{Min} \mathcal{L}$. The three kinds of consistency issues that arise are again explained by the quaternary factorization system of Section 4.4, as the three conditions on line 10 hold when some morphism respectively does not belong to Tot, belongs to Tot but not Inv or belongs to Tot $\cap$ Inv but not Inj.

**Theorem 5.3.** *Algorithm 4 is correct and terminates as soon as $\text{Min} \mathcal{L}$ has finite state-set and $M$ is right-noetherian. It makes at most $3|\text{Min} \mathcal{L}|_{\text{st}} + \text{rk}(\text{Min} \mathcal{L})$ updates to $Q$ (lines 8 and 14) and at most $\text{rk}(\text{Min} \mathcal{L}) + |\text{Min} \mathcal{L}|_{\text{st}}$ updates to $T$ (line 10).*

**Algorithm 4** also differs from Vilar's original learning algorithm in a small additional way: the latter also keeps track of the left-gcds of every $\Lambda(q, \tilde{a})$ where $\tilde{a}$ ranges over $A \cup \{e\}$ and $q \in Q$ is fixed, and checks for consistency issues accordingly. This is a small optimization of the algorithm that does not follow immediately from the categorical framework. In Section 1 we thus actually provided an example run of our version of the algorithm when the output monoid is a free monoid. It also provides example runs of our algorithm for non-free output monoids, as quotienting the output monoid will only remove closure and consistency issues and make the run simpler. For instance letting $\alpha$ commute with $\beta$ for the transducer of Figure 1a would have removed the closure issue and the need to add $a$ to $Q$ while learning the corresponding monoidal transducer, and letting $\alpha$ also commute with $\gamma$ would have removed the first consistency issue to arise and the need to add $a$ to $T$.

## 5.2. Minimization

To transform a transducer $\mathcal{A} = (S, (u_0, s_0), t, \odot)$ recognizing $\mathcal{L}$ into $\text{Min} \mathcal{L}$, a first method is of course to use Algorithm 4, implementing $\text{EVAL}_\mathcal{L}$ using $\mathcal{A}$ and $\text{EQUIV}_\mathcal{L}$ by trying
**Algorithm 4** The FUNL\*-algorithm for monoidal transducers

**Input:** EVAL<sub>L</sub> and EQUIV<sub>L</sub>

**Output:** Min<sub>M</sub>(L)

1: $Q = T = \{e\}$

2: **for** $a \in A \cup \{e\}$ **do**

3:     $\Lambda(e, a) = \text{EVAL}_L(a)$

4:     $R(e, a, e) = \epsilon$

5: **end for**

6: **loop**

7:     **if** there is a $qa \in QA$ such that $\forall q' \in Q, \chi \in M^*, R(q, a, \cdot) \neq \chi R(q', e, \cdot)$ **then**

8:         add $qa$ to $Q$

9:     **else if** there is an $at \in AT$ such that

*   **either** there is a $q \in Q$ such that $R(q, a, t) \neq \perp$ but $R(q, e, T) = \perp^T$;

*   **or** there is a $q \in Q$ such that $\Lambda(q, e)$ does not left-divide $\Lambda(q, a)R(q, a, t)$;

*   **or** there are $q, q' \in Q$ and $\chi \in M^*$ such that $R(q, e, T) = \chi R(q', e, T)$ but $\text{LEFTDIVIDE}(\Lambda(q, e), \Lambda(q, a)R(q, a, t)) \neq \chi \text{LEFTDIVIDE}(\Lambda(q', e), \Lambda(q', a))R(q', a, t))$

**then**

10:     add $at$ to $T$

11: **else**

12:         build $\mathcal{H}(Q, T)$ using $\Lambda$ and $R$

13:         **if** EQUIV<sub>L</sub>(H<sub>Q,T</sub>(L)) outputs some counter-example $w$ **then**

14:             add $w$ and its prefixes to $Q$

15: **else**

16:         **return** $\mathcal{H}(Q, T)$

17: **end if**

18: **end if**

19:     update $\Lambda$ and $R$ using EVAL<sub>L</sub>

20: **end loop**
**Algorithm 4** The FUNL\*-algorithm for monoidal transducers

**Input:** EVAL<sub>L</sub> and EQUIV<sub>L</sub>

**Output:** Min<sub>M</sub>(L)

1: $Q = T = \{e\}$

2: **for** $a \in A \cup \{e\}$ **do**

3:     $\Lambda(e, a) = \text{EVAL}_L(a)$

4:     $R(e, a, e) = \epsilon$

5: **end for**

6: **loop**

7:     **if** there is a $qa \in QA$ such that $\forall q' \in Q, \chi \in M^*, R(q, a, \cdot) \neq \chi R(q', e, \cdot)$ **then**

8:         add $qa$ to $Q$

9:     **else if** there is an $at \in AT$ such that

*   **either** there is a $q \in Q$ such that $R(q, a, t) \neq \perp$ but $R(q, e, T) = \perp^T$;

*   **or** there is a $q \in Q$ such that $\Lambda(q, e)$ does not left-divide $\Lambda(q, a)R(q, a, t)$;

*   **or** there are $q, q' \in Q$ and $\chi \in M^*$ such that $R(q, e, T) = \chi R(q', e, T)$ but $\text{LEFTDIVIDE}(\Lambda(q, e), \Lambda(q, a)R(q, a, t)) \neq \chi \text{LEFTDIVIDE}(\Lambda(q', e), \Lambda(q', a))R(q', a, t))$

**then**

10:     add $at$ to $T$

11: **else**

12:         build $\mathcal{H}(Q, T)$ using $\Lambda$ and $R$

13:         **if** EQUIV<sub>L</sub>(H<sub>Q,T</sub>(L)) outputs some counter-example $w$ **then**

14:             add $w$ and its prefixes to $Q$

15: **else**

16:         **return** $\mathcal{H}(Q, T)$

17: **end if**

18: **end if**

19:     update $\Lambda$ and $R$ using EVAL<sub>L</sub>

20: **end loop**
to compute a morphism of transducers Reach $\mathcal{A} \to \mathcal{H}(Q, T)$. But in practice when $M$ is a free monoid this is not the method that is used: there are algorithms designed specifically for minimizing a transducer, surveyed by Choffrut [9]. These algorithms all decompose the problem into four steps that match exactly those of Definition 4.22.

Computing Reach and Total is straightforward and may be done in linear time using depth-first searches on the underlying graph of $\mathcal{A}$, and this stays true for arbitrary $M$. The problem of computing Prefix and Obs was first tackled in [15], but the solution relied on the existence of an oracle that computes non-trivial left-divisors of countable (but rational) families, and also leaves red $\Lambda$ over when repeatedly applied to some $\Lambda$. In comparison, our instantiation of Algorithm 2 and its dual requires much weaker tools: only `UP TO INV LEFT` and the binary `AND`.

The resulting algorithm itself is not new, as it is exactly the one described in [17]. Our main result relative to minimization is instead that this algorithm can be made to work with not just left- and right-cancellative output monoids: left-cancellativity up to invertibles on the left and right-coprime-cancellativity is enough. Similarly, right-noetherianity is enough to ensure termination, although the resulting complexity now also depends on the rank of elements of $M$. We thus do not describe the implementation in detail, but instead only discuss the insights we get through the big picture of the categorical framework, as well as how easy it is to actually retrieve the concrete algorithms for computing Reach, Total, Prefix and Obs.

**Computing Reach.** Since $\text{KI}(\mathcal{T}_M)$ has all coproducts, Corollary 3.9 holds and to compute Reach we may directly use Algorithm 3. Moreover all split epimorphisms in $\text{KI}(\mathcal{T}_M)$ are in $\text{Surj} = \mathcal{E}$, hence we may also use the optimization of Corollary 3.11. The resulting algorithm is the transducer version of Example 3.12, a depth- or breadth-first search depending on the order in which the to-do list is gone through, and Lemma 5.1 tells us that the complexity is linear in the number of states of $\mathcal{A}$.

There is not much to say here: the instantiation goes smoothly.

**Computing Total.** The case of Total is more interesting, as instantiating the algorithm from the categorical framework is more troublesome, yet the result is still trivial: to remove the states that recognize the empty function, it is enough to do a depth- or breadth-first search on the underlying graph of the transducer, starting from the states where the termination function is defined and following transitions backwards. $\text{KI}(\mathcal{T}_M)$ has all finite products by Proposition 4.12 hence by the dual of Corollary 3.9 we may instantiate this algorithm through the dual of Algorithm 3. But this categorical algorithm tells us to keep track of a $(\text{Surj} \cap \text{Inj} \cap \text{Inv})$-quotient $\mathcal{A}(\text{st}) \twoheadrightarrow_1 \mathcal{A}(\text{st})/T$, that is a partial function that tells us for each state $s \in \mathcal{A}(\text{St})$ whether there is a $t \in T$ such that $\mathcal{A}(t \triangleleft(s) \neq \bot)$. To compute the factorizations incrementally we would then need to factorize the cartesian products of such functions, which, while correct, is quite unnatural.

A more intuitive way to instantiate the algorithm is to notice that $(\text{Surj} \cap \text{Inj} \cap \text{Inv})$-quotients are exactly the split epimorphisms of $\text{KI}(\mathcal{T}_M)$, and, as such, have right inverses.
to compute a morphism of transducers Reach $\mathcal{A} \to \mathcal{H}(Q, T)$. But in practice when $M$ is a free monoid this is not the method that is used: there are algorithms designed specifically for minimizing a transducer, surveyed by Choffrut [9]. These algorithms all decompose the problem into four steps that match exactly those of Definition 4.22.

Computing Reach and Total is straightforward and may be done in linear time using depth-first searches on the underlying graph of $\mathcal{A}$, and this stays true for arbitrary $M$. The problem of computing Prefix and Obs was first tackled in [15], but the solution relied on the existence of an oracle that computes non-trivial left-divisors of countable (but rational) families, and also leaves red $\Lambda$ over when repeatedly applied to some $\Lambda$. In comparison, our instantiation of Algorithm 2 and its dual requires much weaker tools: only `UP TO INV LEFT` and the binary `AND`.

The resulting algorithm itself is not new, as it is exactly the one described in [17]. Our main result relative to minimization is instead that this algorithm can be made to work with not just left- and right-cancellative output monoids: left-cancellativity up to invertibles on the left and right-coprime-cancellativity is enough. Similarly, right-noetherianity is enough to ensure termination, although the resulting complexity now also depends on the rank of elements of $M$. We thus do not describe the implementation in detail, but instead only discuss the insights we get through the big picture of the categorical framework, as well as how easy it is to actually retrieve the concrete algorithms for computing Reach, Total, Prefix and Obs.

**Computing Reach.** Since $\text{KI}(\mathcal{T}_M)$ has all coproducts, Corollary 3.9 holds and to compute Reach we may directly use Algorithm 3. Moreover all split epimorphisms in $\text{KI}(\mathcal{T}_M)$ are in $\text{Surj} = \mathcal{E}$, hence we may also use the optimization of Corollary 3.11. The resulting algorithm is the transducer version of Example 3.12, a depth- or breadth-first search depending on the order in which the to-do list is gone through, and Lemma 5.1 tells us that the complexity is linear in the number of states of $\mathcal{A}$.

There is not much to say here: the instantiation goes smoothly.

**Computing Total.** The case of Total is more interesting, as instantiating the algorithm from the categorical framework is more troublesome, yet the result is still trivial: to remove the states that recognize the empty function, it is enough to do a depth- or breadth-first search on the underlying graph of the transducer, starting from the states where the termination function is defined and following transitions backwards. $\text{KI}(\mathcal{T}_M)$ has all finite products by Proposition 4.12 hence by the dual of Corollary 3.9 we may instantiate this algorithm through the dual of Algorithm 3. But this categorical algorithm tells us to keep track of a $(\text{Surj} \cap \text{Inj} \cap \text{Inv})$-quotient $\mathcal{A}(\text{st}) \twoheadrightarrow_1 \mathcal{A}(\text{st})/T$, that is a partial function that tells us for each state $s \in \mathcal{A}(\text{St})$ whether there is a $t \in T$ such that $\mathcal{A}(t \triangleleft(s) \neq \top)$. To compute the factorizations incrementally we would then need to factorize the cartesian products of such functions, which, while correct, is quite unnatural.

A more intuitive way to instantiate the algorithm is to notice that $(\text{Surj} \cap \text{Inj} \cap \text{Inv})$-quotients are exactly the split epimorphisms of $\text{KI}(\mathcal{T}_M)$, and, as such, have right inverses.
Keeping track of the right inverse of the quotient $\mathcal{A}(st) \dashrightarrow_1 \mathcal{A}(st)/T$ would then mean keeping track of its codomain as a subset of $\mathcal{A}(st)$. This is more natural, only now we cannot compute the factorizations incrementally anymore, as we would want to do so by factorizing the coproduct of such embeddings but this is not encompassed by the dual of Lemma 3.7. This obstacle can be overcome by considering the transducer as the transpose of a non-deterministic transducer, i.e. seeing $\text{Kl}(\mathcal{T}_M)^{\text{op}}$ as a subcategory of $\text{Kl}(\mathcal{P}(M^{\text{op}} \times -))$, where $\mathcal{P}$ is the powerset monad. With this point of view, the states that recognize a non-empty function are exactly those that are reachable in the non-deterministic reverse transducer: computing Total can be done by reversing the transducer, computing Reach in the category of non-deterministic $M^{\text{op}}$-transducers and reversing the result back. This categorical algorithm yields precisely the graph traversal we were looking for, with the same catch as that of Example 3.13: it does not tell us that transitions along the same letter and to the same state can be considered separately.

However we choose to view this instantiation, the $(\text{Surj} \cap \text{Inj} \cap \text{Inv})$-codimension of a set is its cardinal, hence we know the main loop will be run at most once for each state of $\mathcal{A}$.

**Computing Prefix.** The core of the problem is to compute Prefix $\mathcal{A}$ knowing Total $\mathcal{A}$, that is to compute the left-gcds of the functions recognized from each state that is reachable and recognizes a non-empty function. Béal and Carton do it by pulling back letters along the transitions of $\mathcal{A}$ [4], but this relies crucially on $M$ being a free monoid as the letters to pull back must be produced by every transition going out of a given state. This would for instance not be enough to see that the left-gcd of state 3 in Figure 3b is $\alpha$ (when $M$ is the free commutative monoid). Breslauer does it by computing over-approximations and the length of the left-gcds, and then taking the corresponding prefixes [7], but again this algorithm does not generalize to arbitrary $M$ because it relies crucially on the free monoid being graded.

In the general case, Prefix $\mathcal{A}$ may be computed using a fixed-point algorithm, keeping track of a tentative left-gcd $l(s)$ for each state $s \in \mathcal{A}(st)$ and replacing $l(s)$ with $l(s) \wedge \bigwedge_{a \in A}(s \circ a)l(s \cdot a)$ as long as needed [17, Section 4], and this is exactly what we get when we instantiate the dual of Algorithm 3 and the optimization dual to that of Corollary 3.11 for the factorization system $(\mathcal{E}_2, \mathcal{M}_2)$.

An interesting thing to notice here is that since we start from Total $\mathcal{A}$, we may consider that we are computing the $(\text{Surj} \cap \text{Inj}, \text{Inv} \cap \text{Tot})$-factorization of Total $\mathcal{A} \dashrightarrow_1 \mathcal{A}^{\text{final}}(\mathcal{L})$ in the category of total transducers (those whose final morphism to $\mathcal{A}^{\text{final}}$ is in Tot) and total morphisms between them (the morphisms between them are also in Tot, thanks to [8, Lemma 14.9(1)]). Hence we actually compute a $(\text{Surj} \cap \text{Inj} \cap \text{Tot}, \text{Inv} \cap \text{Tot})$-factorization. This is particularly interesting when giving a complexity-bound for the number of times the main loop is run. The $(\text{Surj} \cap \text{Inj})$-codimension of some $e : X \dashrightarrow_2 Y$ is indeed $|X|-|Y|+\text{rk } e$, whereas the $(\text{Surj} \cap \text{Inj} \cap \text{Tot})$-codimension of some $e : X \dashrightarrow_1 Y$ is just $\text{rk } e$: the prior knowledge that the transducer was total got rid of the cardinality term. Still, [17, Lemma 6] gets a much better complexity result than we do: where we
Keeping track of the right inverse of the quotient $\mathcal{A}(st) \dashrightarrow_1 \mathcal{A}(st)/T$ would then mean keeping track of its codomain as a subset of $\mathcal{A}(st)$. This is more natural, only now we cannot compute the factorizations incrementally anymore, as we would want to do so by factorizing the coproduct of such embeddings but this is not encompassed by the dual of Lemma 3.7. This obstacle can be overcome by considering the transducer as the transpose of a non-deterministic transducer, i.e. seeing $\text{Kl}(\mathcal{T}_M)^{\text{op}}$ as a subcategory of $\text{Kl}(\mathcal{P}(M^{\text{op}} \times -))$, where $\mathcal{P}$ is the powerset monad. With this point of view, the states that recognize a non-empty function are exactly those that are reachable in the non-deterministic reverse transducer: computing Total can be done by reversing the transducer, computing Reach in the category of non-deterministic $M^{\text{op}}$-transducers and reversing the result back. This categorical algorithm yields precisely the graph traversal we were looking for, with the same catch as that of Example 3.13: it does not tell us that transitions along the same letter and to the same state can be considered separately.

However we choose to view this instantiation, the $(\text{Surj} \cap \text{Inj} \cap \text{Inv})$-codimension of a set is its cardinal, hence we know the main loop will be run at most once for each state of $\mathcal{A}$.

**Computing Prefix.** The core of the problem is to compute Prefix $\mathcal{A}$ knowing Total $\mathcal{A}$, that is to compute the left-gcds of the functions recognized from each state that is reachable and recognizes a non-empty function. Béal and Carton do it by pulling back letters along the transitions of $\mathcal{A}$ [4], but this relies crucially on $M$ being a free monoid as the letters to pull back must be produced by every transition going out of a given state. This would for instance not be enough to see that the left-gcd of state 3 in Figure 3b is $\alpha$ (when $M$ is the free commutative monoid). Breslauer does it by computing over-approximations and the length of the left-gcds, and then taking the corresponding prefixes [7], but again this algorithm does not generalize to arbitrary $M$ because it relies crucially on the free monoid being graded.

In the general case, Prefix $\mathcal{A}$ may be computed using a fixed-point algorithm, keeping track of a tentative left-gcd $l(s)$ for each state $s \in \mathcal{A}(st)$ and replacing $l(s)$ with $l(s) \wedge \bigwedge_{a \in A}(s \circ a)l(s \cdot a)$ as long as needed [17, Section 4], and this is exactly what we get when we instantiate the dual of Algorithm 3 and the optimization dual to that of Corollary 3.11 for the factorization system $(\mathcal{E}_2, \mathcal{M}_2)$.

An interesting thing to notice here is that since we start from Total $\mathcal{A}$, we may consider that we are computing the $(\text{Surj} \cap \text{Inj}, \text{Inv} \cap \text{Tot})$-factorization of Total $\mathcal{A} \dashrightarrow_1 \mathcal{A}^{\text{final}}(\mathcal{L})$ in the category of total transducers (those whose final morphism to $\mathcal{A}^{\text{final}}$ is in Tot) and total morphisms between them (the morphisms between them are also in Tot, thanks to [8, Lemma 14.9(1)]). Hence we actually compute a $(\text{Surj} \cap \text{Inj} \cap \text{Tot}, \text{Inv} \cap \text{Tot})$-factorization. This is particularly interesting when giving a complexity-bound for the number of times the main loop is run. The $(\text{Surj} \cap \text{Inj})$-codimension of some $e : X \dashrightarrow_2 Y$ is indeed $|X|-|Y|+\text{rk } e$, whereas the $(\text{Surj} \cap \text{Inj} \cap \text{Tot})$-codimension of some $e : X \dashrightarrow_1 Y$ is just $\text{rk } e$: the prior knowledge that the transducer was total got rid of the cardinality term. Still, [17, Lemma 6] gets a much better complexity result than we do: where we
get a complexity linear in rk $\mathcal{A}$, they get one linear in $|\mathcal{A}(\mathbf{st})|$. This is because they use an assumption quite different from right-noetherianity (namely, that if $v$ left-divides $\omega$ and $\nu\omega$ then it left-divides $\nu\upsilon$) that allows them to prove some kind of pumping lemma for transducers.

**Computing Obs.** Computing Obs from Prefix $\mathcal{A}$ is also straightforward when $M$ is the free monoid as it amounts to minimizing a deterministic automaton, which can be done using Hopcroft's algorithm for instance [9]. This is still true when $M$ has no non-trivial invertibles, but for arbitrary $M$ it is not as easy: checking whether two states are equivalent amounts to checking for equality of (left-coprime) subsequential functions up to invertibles.

A general algorithm for computing Obs $\mathcal{A}$ can be designed by extending Moore's partition refinement algorithm with equality up to invertibles. In a nutshell, this algorithm should maintain a partition of the states into equivalence classes and for every pair of equivalent states an invertible element that witnesses the equivalence, and refine this equivalence as long as needed [17, Section 5]. This is, again, exactly the algorithm we get when we instantiate the dual of Algorithm 3 along with the optimization dual to that of Corollary 3.11 for the factorization system $(\mathcal{E}_3, \mathcal{M}_3)$.

Just as for Prefix we restricted ourselves to the category of total transducers, we can restrict ourselves to the category of onwards transducers (those for which the final morphism to $\mathcal{A}^{final}(\mathcal{L})$ is in $\text{Inv} \cap \text{Tot}$) and $(\text{Inv} \cap \text{Tot})$-morphisms between them. In particular, this means the complexity of computing Obs $\mathcal{A}$ from Prefix $\mathcal{A}$ only depends on the number of states of Total $\mathcal{A}$, and we retrieve the same complexity as that of [17, Lemma 13].

**Worklist algorithms everywhere.** A final insight we get from applying the minimization algorithm of our categorical framework is that the algorithms for computing Reach, Total, Prefix and Obs all share the same structure: they are worklist algorithms, that is fixed-points of an operator on a graph defined by dataflow-style equations on each vertex.

Since the technical details of the algorithm are quite heavy to lay out, we also provide a modular **OCaml** implementation for right-cancellative output monoids [2] as a proof-of-concept (it is in particular not fully optimized), that includes implementations of the oracles for trace monoids, the group $\mathbb{Z}$ and products of monoids. It uses the **OCamlGraph** library [12] to represent the underlying graph of a transducer, and its **Fixpoint** module to implement each of Reach, Total, Prefix and Obs as worklist algorithms: this module only requires the dataflow-style equations and computes the corresponding fixpoint automatically.

# 6. Summary and future work

In this work, we extended Colcombet, Petrişan and Stabile's active learning categorical framework with a minimization algorithm, and instantiated it with monoidal transduc-
get a complexity linear in rk $\mathcal{A}$, they get one linear in $|\mathcal{A}(\mathbf{st})|$. This is because they use an assumption quite different from right-noetherianity (namely, that if $v$ left-divides $\omega$ and $\nu\omega$ then it left-divides $\nu\upsilon$) that allows them to prove some kind of pumping lemma for transducers.

**Computing Obs.** Computing Obs from Prefix $\mathcal{A}$ is also straightforward when $M$ is the free monoid as it amounts to minimizing a deterministic automaton, which can be done using Hopcroft's algorithm for instance [9]. This is still true when $M$ has no non-trivial invertibles, but for arbitrary $M$ it is not as easy: checking whether two states are equivalent amounts to checking for equality of (left-coprime) subsequential functions up to invertibles.

A general algorithm for computing Obs $\mathcal{A}$ can be designed by extending Moore's partition refinement algorithm with equality up to invertibles. In a nutshell, this algorithm should maintain a partition of the states into equivalence classes and for every pair of equivalent states an invertible element that witnesses the equivalence, and refine this equivalence as long as needed [17, Section 5]. This is, again, exactly the algorithm we get when we instantiate the dual of Algorithm 3 along with the optimization dual to that of Corollary 3.11 for the factorization system $(\mathcal{E}_3, \mathcal{M}_3)$.

Just as for Prefix we restricted ourselves to the category of total transducers, we can restrict ourselves to the category of onwards transducers (those for which the final morphism to $\mathcal{A}^{final}(\mathcal{L})$ is in $\text{Inv} \cap \text{Tot}$) and $(\text{Inv} \cap \text{Tot})$-morphisms between them. In particular, this means the complexity of computing Obs $\mathcal{A}$ from Prefix $\mathcal{A}$ only depends on the number of states of Total $\mathcal{A}$, and we retrieve the same complexity as that of [17, Lemma 13].

**Worklist algorithms everywhere.** A final insight we get from applying the minimization algorithm of our categorical framework is that the algorithms for computing Reach, Total, Prefix and Obs all share the same structure: they are worklist algorithms, that is fixed-points of an operator on a graph defined by dataflow-style equations on each vertex.

Since the technical details of the algorithm are quite heavy to lay out, we also provide a modular **OCaml** implementation for right-cancellative output monoids [2] as a proof-of-concept (it is in particular not fully optimized), that includes implementations of the oracles for trace monoids, the group $\mathbb{Z}$ and products of monoids. It uses the **OCamlGraph** library [12] to represent the underlying graph of a transducer, and its **Fixpoint** module to implement each of Reach, Total, Prefix and Obs as worklist algorithms: this module only requires the dataflow-style equations and computes the corresponding fixpoint automatically.

# 6. Summary and future work

In this work, we extended Colcombet, Petrişan and Stabile's active learning categorical framework with a minimization algorithm, and instantiated it with monoidal transduc-
ers. We gave some simple sufficient conditions on the output monoid for the minimal
transducer to exist and be unique up to isomorphism, which in particular extend Gerd-
jikov's conditions for minimization to be possible [17]. Finally, we described what the
active learning algorithm of the categorical framework instantiated to in practice un-
der these conditions, relying in particular on the quaternary factorization system in the
output category.

This work was mainly a theoretical excursion and was not motivated by practical
examples where monoidal transducers are used. Although we expect them to be useful
in concurrency theory and in natural language processing, such examples are thus still to
be found. In particular, can monoidal transducers with outputs in trace monoids (and
their learning) to programatically schedule jobs, as mentioned in the introduction. We
also leave the search for other interesting examples for future work.

Some intermediate results of this work go beyond what the categorical framework
currently provides and could be generalized. The use of a quaternary factorization system
(or any *n*-ary factorization system) would split the algorithms into several substeps that
should be easier to work with. Here our factorization systems seemed to arise as the
image of the factorization system on **Set** through the monad *T*<sub>*M*</sub>; generalizing this to
other monads could provide meaningful examples of factorization systems in any Kleisli
category. Finally, we mentioned in Section 4.3 that a problem with the current framework
is that it may only account for the minimization of both finite and infinite transition
systems at the same time, and conjectured that we could restrict to only the finite case
by working in a subcategory of well-behaved transducers: this subcategory is perhaps
an instance of a general construction that has its own version of Theorem 2.12, so as to
still have a generic way to build the initial, final and minimal objects.

References

[1] Dana Angluin. "Learning Regular Sets from Queries and Counterexamples". In: *Information and Computation* 75.2 (Nov. 1, 1987), pp. 87–106. ISSN: 0890-5401. DOI: 10.1016/0890-5401(87)90052-6. URL: https://www.sciencedirect.com/science/article/pii/0890540187900526 (visited on 05/04/2023).

[2] Quentin Aristote. *Monoidal Transducers Minimization*. 2022. URL: https://gitlab.math.univ-paris-diderot.fr/aristote/monoidal-transducers-minimization.

[3] Simone Barlocco, Clemens Kupke, and Jurriaan Rot. “Coalgebra Learning via Duality”. In: *Foundations of Software Science and Computation Structures*. Ed. by Mikołaj Bojańczyk and Alex Simpson. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2019, pp. 62–79. ISBN: 978-3-030-17127-8. DOI: 10.1007/978-3-030-17127-8_4.

[4] Marie-Pierre Béal and Olivier Carton. “Computing the Prefix of an Automaton”. In: *Informatique Théorique et Applications* 34.6 (2000), p. 503. URL: https://hal.science/hal-00619217 (visited on 05/04/2023).
ers. We gave some simple sufficient conditions on the output monoid for the minimal
transducer to exist and be unique up to isomorphism, which in particular extend Gerd-
jikov's conditions for minimization to be possible [17]. Finally, we described what the
active learning algorithm of the categorical framework instantiated to in practice un-
der these conditions, relying in particular on the quaternary factorization system in the
output category.

This work was mainly a theoretical excursion and was not motivated by practical
examples where monoidal transducers are used. Although we expect them to be useful
in concurrency theory and in natural language processing, such examples are thus still to
be found. In particular, can monoidal transducers with outputs in trace monoids (and
their learning) to programatically schedule jobs, as mentioned in the introduction. We
also leave the search for other interesting examples for future work.

Some intermediate results of this work go beyond what the categorical framework
currently provides and could be generalized. The use of a quaternary factorization system
(or any *n*-ary factorization system) would split the algorithms into several substeps that
should be easier to work with. Here our factorization systems seemed to arise as the
image of the factorization system on **Set** through the monad *T*<sub>*M*</sub>; generalizing this to
other monads could provide meaningful examples of factorization systems in any Kleisli
category. Finally, we mentioned in Section 4.3 that a problem with the current framework
is that it may only account for the minimization of both finite and infinite transition
systems at the same time, and conjectured that we could restrict to only the finite case
by working in a subcategory of well-behaved transducers: this subcategory is perhaps
an instance of a general construction that has its own version of Theorem 2.12, so as to
still have a generic way to build the initial, final and minimal objects.

References

[1] Dana Angluin. "Learning Regular Sets from Queries and Counterexamples". In: *Information and Computation* 75.2 (Nov. 1, 1987), pp. 87–106. ISSN: 0890-5401. DOI: 10.1016/0890-5401(87)90052-6. URL: https://www.sciencedirect.com/science/article/pii/0890540187900526 (visited on 05/04/2023).

[2] Quentin Aristote. *Monoidal Transducers Minimization*. 2022. URL: https://gitlab.math.univ-paris-diderot.fr/aristote/monoidal-transducers-minimization.

[3] Simone Barlocco, Clemens Kupke, and Jurriaan Rot. “Coalgebra Learning via Duality”. In: *Foundations of Software Science and Computation Structures*. Ed. by Mikołaj Bojańczyk and Alex Simpson. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2019, pp. 62–79. ISBN: 978-3-030-17127-8. DOI: 10.1007/978-3-030-17127-8_4.

[4] Marie-Pierre Béal and Olivier Carton. “Computing the Prefix of an Automaton”. In: *Informatique Théorique et Applications* 34.6 (2000), p. 503. URL: https://hal.science/hal-00619217 (visited on 05/04/2023).
[5] F. Bergadano and S. Varricchio. "Learning Behaviors of Automata from Multiplicity and Equivalence Queries". In: *Algorithms and Complexity*. Ed. by M. Bonuccelli, P. Crescenzi, and R. Petreschi. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1994, pp. 54–62. ISBN: 978-3-540-48337-3. DOI: 10.1007/3-540-57811-0_6.

[6] Francesco Bergadano and Stefano Varricchio. "Learning Behaviors of Automata from Multiplicity and Equivalence Queries". In: *SIAM Journal on Computing* 25.6 (Dec. 1996), pp. 1268–1280. ISSN: 0097-5397. DOI: 10.1137/S009753979326091X. URL: https://epubs.siam.org/doi/10.1137/S009753979326091X (visited on 05/04/2023).

[7] Dany Breslauer. "The Suffix Tree of a Tree and Minimizing Sequential Transducers". In: *Theoretical Computer Science* 191.1 (Jan. 30, 1998), pp. 131–144. ISSN: 0304-3975. DOI: 10.1016/S0304-3975(96)00319-2. URL: https://www.sciencedirect.com/science/article/pii/S0304397596003192 (visited on 05/04/2023).

[8] Gabriele Castellini et al. "Abstract and Concrete Categories". In: *The American Mathematical Monthly* 98.3 (Mar. 1991), pp. 285–287. ISSN: 0002-9890, 1930-0972. DOI: 10.1080/00029890.1991.11995743. URL: https://www.tandfonline.com/doi/full/10.1080/00029890.1991.11995743 (visited on 03/20/2023).

[9] Christian Choffrut. "Minimizing Subsequential Transducers: A Survey". In: *Theoretical Computer Science*. Selected Papers in Honor of Jean Berstel 292.1 (Jan. 10, 2003), pp. 131–143. ISSN: 0304-3975. DOI: 10.1016/S0304-3975(01)00219-5. URL: https://www.sciencedirect.com/science/article/pii/S0304397501002195 (visited on 05/04/2023).

[10] Thomas Colcombet, Daniela Petrişan, and Riccardo Stabile. *Learning Automata and Transducers: A Categorical Approach*. Oct. 26, 2020. DOI: 10.48550/arXiv.2010.13675. arXiv: 2010.13675 [cs]. URL: http://arxiv.org/abs/2010.13675 (visited on 04/03/2023). preprint.

[11] Thomas Colcombet, Daniela Petrişan, and Riccardo Stabile. "Learning Automata and Transducers: A Categorical Approach". In: *29th EACSL Annual Conference on Computer Science Logic (CSL 2021)*. Ed. by Christel Baier and Jean Goubault-Larrecq. Vol. 183. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021, 15:1–15:17. ISBN: 978-3-95977-175-7. DOI: 10.4230/LIPIcs.CSL.2021.15. URL: https://drops.dagstuhl.de/opus/volltexte/2021/13449 (visited on 05/04/2023).

[12] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. "Designing a Generic Graph Library Using ML Functors". In: *Trends in Functional Programming*. 2008, pp. 124–140. URL: https://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp-8.pdf.
[5] F. Bergadano and S. Varricchio. "Learning Behaviors of Automata from Multiplicity and Equivalence Queries". In: *Algorithms and Complexity*. Ed. by M. Bonuccelli, P. Crescenzi, and R. Petreschi. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1994, pp. 54–62. ISBN: 978-3-540-48337-3. DOI: 10.1007/3-540-57811-0_6.

[6] Francesco Bergadano and Stefano Varricchio. "Learning Behaviors of Automata from Multiplicity and Equivalence Queries". In: *SIAM Journal on Computing* 25.6 (Dec. 1996), pp. 1268–1280. ISSN: 0097-5397. DOI: 10.1137/S009753979326091X. URL: https://epubs.siam.org/doi/10.1137/S009753979326091X (visited on 05/04/2023).

[7] Dany Breslauer. "The Suffix Tree of a Tree and Minimizing Sequential Transducers". In: *Theoretical Computer Science* 191.1 (Jan. 30, 1998), pp. 131–144. ISSN: 0304-3975. DOI: 10.1016/S0304-3975(96)00319-2. URL: https://www.sciencedirect.com/science/article/pii/S0304397596003192 (visited on 05/04/2023).

[8] Gabriele Castellini et al. "Abstract and Concrete Categories". In: *The American Mathematical Monthly* 98.3 (Mar. 1991), pp. 285–287. ISSN: 0002-9890, 1930-0972. DOI: 10.1080/00029890.1991.11995743. URL: https://www.tandfonline.com/doi/full/10.1080/00029890.1991.11995743 (visited on 03/20/2023).

[9] Christian Choffrut. "Minimizing Subsequential Transducers: A Survey". In: *Theoretical Computer Science*. Selected Papers in Honor of Jean Berstel 292.1 (Jan. 10, 2003), pp. 131–143. ISSN: 0304-3975. DOI: 10.1016/S0304-3975(01)00219-5. URL: https://www.sciencedirect.com/science/article/pii/S0304397501002195 (visited on 05/04/2023).

[10] Thomas Colcombet, Daniela Petrişan, and Riccardo Stabile. *Learning Automata and Transducers: A Categorical Approach*. Oct. 26, 2020. DOI: 10.48550/arXiv.2010.13675. arXiv: 2010.13675 [cs]. URL: http://arxiv.org/abs/2010.13675 (visited on 04/03/2023). preprint.

[11] Thomas Colcombet, Daniela Petrişan, and Riccardo Stabile. "Learning Automata and Transducers: A Categorical Approach". In: *29th EACSL Annual Conference on Computer Science Logic (CSL 2021)*. Ed. by Christel Baier and Jean Goubault-Larrecq. Vol. 183. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021, 15:1–15:17. ISBN: 978-3-95977-175-7. DOI: 10.4230/LIPIcs.CSL.2021.15. URL: https://drops.dagstuhl.de/opus/volltexte/2021/13449 (visited on 05/04/2023).

[12] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. "Designing a Generic Graph Library Using ML Functors". In: *Trends in Functional Programming*. 2008, pp. 124–140. URL: https://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp-8.pdf.
[13] Robert Cori and Dominique Perrin. "Automates et commutations partielles". In: *RAIRO. Informatique théorique* 19.1 (1 1985), pp. 21-32. ISSN: 0399-0540, 2777-3337. DOI: 10.1051/ita/1985190100211. URL: https://www.rairo-ita.org/articles/ita/abs/1985/01/ita1985190100211/ita1985190100211.html (visited on 05/04/2023).

[14] Ulrich Dorsch et al. "Efficient Coalgebraic Partition Refinement". In: *28th International Conference on Concurrency Theory (CONCUR 2017)*. Ed. by Roland Meyer and Uwe Nestmann. Vol. 85. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017, 32:1-32:16. ISBN: 978-3-95977-048-4. DOI: 10.4230/LIPIcs.CONCUR.2017.32. URL: http://drops.dagstuhl.de/opus/volltexte/2017/7793 (visited on 07/24/2023).

[15] Jason Eisner. "Simpler and More General Minimization for Weighted Finite-State Automata". In: *Proceedings of the 2003 Conference of the North American Chapter of the Association for Computational Linguistics on Human Language Technology - Volume 1*. NAACL '03. USA: Association for Computational Linguistics, May 27, 2003, pp. 64-71. DOI: 10.3115/1073445.1073454. URL: https://dl.acm.org/doi/10.3115/1073445.1073454 (visited on 05/04/2023).

[16] Charles N. Fischer, Ron K. Cytron, and Richard J. LeBlanc. *Crafting a Compiler*. Crafting a Compiler with C. Boston: Addison-Wesley, 2010. 683 pp. ISBN: 978-0-13-606705-4.

[17] Stefan Gerdjikov. "A General Class of Monoids Supporting Canonisation and Minimisation of (Sub)Sequential Transducers". In: *Language and Automata Theory and Applications*. Ed. by Shmuel Tomi Klein, Carlos Martín-Vide, and Dana Shapira. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2018, pp. 143-155. ISBN: 978-3-319-77313-1. DOI: 10.1007/978-3-319-77313-1_11.

[18] John Hopcroft. "AN n Log n ALGORITHM FOR MINIMIZING STATES IN A FINITE AUTOMATON". In: *Theory of Machines and Computations*. Ed. by Zvi Kohavi and Azaria Paz. Academic Press, Jan. 1, 1971, pp. 189-196. ISBN: 978-0-12-417750-5. DOI: 10.1016/B978-0-12-417750-5.50022-1. URL: https://www.sciencedirect.com/science/article/pii/B9780124177505500221 (visited on 05/16/2023).

[19] Ronald M. Kaplan and Martin Kay. "Regular Models of Phonological Rule Systems". In: *Computational Linguistics* 20.3 (1994), pp. 331-378. URL: https://aclanthology.org/J94-3001 (visited on 05/04/2023).

[20] Kevin Knight and Jonathan May. "Applications of Weighted Automata in Natural Language Processing". In: *Handbook of Weighted Automata*. Ed. by Manfred Droste, Werner Kuich, and Heiko Vogler. Monographs in Theoretical Computer Science. An EATCS Series. Berlin, Heidelberg: Springer, 2009, pp. 571-596. ISBN: 978-3-642-01492-5. DOI: 10.1007/978-3-642-01492-5_14. URL: https://doi.org/10.1007/978-3-642-01492-5_14 (visited on 05/04/2023).
[13] Robert Cori and Dominique Perrin. "Automates et commutations partielles". In: *RAIRO. Informatique théorique* 19.1 (1 1985), pp. 21-32. ISSN: 0399-0540, 2777-3337. DOI: 10.1051/ita/1985190100211. URL: https://www.rairo-ita.org/articles/ita/abs/1985/01/ita1985190100211/ita1985190100211.html (visited on 05/04/2023).

[14] Ulrich Dorsch et al. "Efficient Coalgebraic Partition Refinement". In: *28th International Conference on Concurrency Theory (CONCUR 2017)*. Ed. by Roland Meyer and Uwe Nestmann. Vol. 85. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017, 32:1-32:16. ISBN: 978-3-95977-048-4. DOI: 10.4230/LIPIcs.CONCUR.2017.32. URL: http://drops.dagstuhl.de/opus/volltexte/2017/7793 (visited on 07/24/2023).

[15] Jason Eisner. "Simpler and More General Minimization for Weighted Finite-State Automata". In: *Proceedings of the 2003 Conference of the North American Chapter of the Association for Computational Linguistics on Human Language Technology - Volume 1*. NAACL '03. USA: Association for Computational Linguistics, May 27, 2003, pp. 64-71. DOI: 10.3115/1073445.1073454. URL: https://dl.acm.org/doi/10.3115/1073445.1073454 (visited on 05/04/2023).

[16] Charles N. Fischer, Ron K. Cytron, and Richard J. LeBlanc. *Crafting a Compiler*. Crafting a Compiler with C. Boston: Addison-Wesley, 2010. 683 pp. ISBN: 978-0-13-606705-4.

[17] Stefan Gerdjikov. "A General Class of Monoids Supporting Canonisation and Minimisation of (Sub)Sequential Transducers". In: *Language and Automata Theory and Applications*. Ed. by Shmuel Tomi Klein, Carlos Martín-Vide, and Dana Shapira. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2018, pp. 143-155. ISBN: 978-3-319-77313-1. DOI: 10.1007/978-3-319-77313-1_11.

[18] John Hopcroft. "AN n Log n ALGORITHM FOR MINIMIZING STATES IN A FINITE AUTOMATON". In: *Theory of Machines and Computations*. Ed. by Zvi Kohavi and Azaria Paz. Academic Press, Jan. 1, 1971, pp. 189-196. ISBN: 978-0-12-417750-5. DOI: 10.1016/B978-0-12-417750-5.50022-1. URL: https://www.sciencedirect.com/science/article/pii/B9780124177505500221 (visited on 05/16/2023).

[19] Ronald M. Kaplan and Martin Kay. "Regular Models of Phonological Rule Systems". In: *Computational Linguistics* 20.3 (1994), pp. 331-378. URL: https://aclanthology.org/J94-3001 (visited on 05/04/2023).

[20] Kevin Knight and Jonathan May. "Applications of Weighted Automata in Natural Language Processing". In: *Handbook of Weighted Automata*. Ed. by Manfred Droste, Werner Kuich, and Heiko Vogler. Monographs in Theoretical Computer Science. An EATCS Series. Berlin, Heidelberg: Springer, 2009, pp. 571-596. ISBN: 978-3-642-01492-5. DOI: 10.1007/978-3-642-01492-5_14. URL: https://doi.org/10.1007/978-3-642-01492-5_14 (visited on 05/04/2023).
[21] Saunders Mac Lane. *Categories for the Working Mathematician*. Vol. 5. Graduate Texts in Mathematics. New York, NY: Springer, 1978. ISBN: 978-1-4419-3123-8
978-1-4757-4721-8. DOI: 10.1007/978-1-4757-4721-8. URL: http://link.springer.com/10.1007/978-1-4757-4721-8 (visited on 05/05/2023).

[22] Edward F. Moore. "Gedanken-Experiments on Sequential Machines". In: *Automata Studies*. Annals of Mathematics Studies, No. 34. Princeton University Press, Princeton, N.J., 1956, pp. 129-153.

[23] Daniela Petrişan and Thomas Colcombet. "Automata Minimization: A Functorial Approach". In: *Logical Methods in Computer Science* Volume 16, Issue 1 (Mar. 23, 2020). DOI: 10.23638/LMCS-16(1:32)2020. URL: https://lmcs.episciences.org/6213/pdf (visited on 04/12/2023).

[24] Jacques Sakarovitch. "1. The Simplest Possible Machine". In: *Elements of Automata Theory*. Ed. by Thomas Reuben. Cambridge: Cambridge University Press, 2009, pp. 49-216. DOI: 10.1017/CB09781139195218.005.

[25] M. P. Schützenberger. "On the Definition of a Family of Automata". In: *Information and Control* 4.2 (Sept. 1, 1961), pp. 245-270. ISSN: 0019-9958. DOI: 10.1016/S0019-9958(61)80020-X. URL: https://www.sciencedirect.com/science/article/pii/S001999586180020X (visited on 05/04/2023).

[26] Jenö Szigeti. "On Limits and Colimits in the Kleisli Category". In: *Cahiers de topologie et géométrie différentielle* 24.4 (1983), pp. 381-391. ISSN: 2681-2398. URL: http://www.numdam.org/item/?id=CTGDC_1983_24_4_381_0 (visited on 05/23/2023).

[27] Henning Urbat and Lutz Schröder. "Automata Learning: An Algebraic Approach". In: *Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science*. LICS '20. New York, NY, USA: Association for Computing Machinery, July 8, 2020, pp. 900-914. ISBN: 978-1-4503-7104-9. DOI: 10.1145/3373718.3394775. URL: https://dl.acm.org/doi/10.1145/3373718.3394775 (visited on 05/04/2023).

[28] Gerco van Heerdt, Matteo Sammartino, and Alexandra Silva. "Learning Automata with Side-Effects". In: *Coalgebraic Methods in Computer Science*. Ed. by Daniela Petrişan and Jurriaan Rot. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2020, pp. 68-89. ISBN: 978-3-030-57201-3. DOI: 10.1007/978-3-030-57201-3_5.

[29] Juan Miguel Vilar. "Query Learning of Subsequential Transducers". In: *Grammatical Interference: Learning Syntax from Sentences*. Ed. by Laurent Miclet and Colin de la Higuera. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1996, pp. 72-83. ISBN: 978-3-540-70678-6. DOI: 10.1007/BFb0033343.

[30] Thorsten Wißmann et al. "A Coalgebraic View on Reachability". In: *Commentaciones Mathematicae Universitatis Carolinae* 60.4 (2019), pp. 605-638. ISSN: 0010-2628 (print). URL: https://dml.cz/handle/10338.dmlcz/147977 (visited on 05/05/2023).
[21] Saunders Mac Lane. *Categories for the Working Mathematician*. Vol. 5. Graduate Texts in Mathematics. New York, NY: Springer, 1978. ISBN: 978-1-4419-3123-8
978-1-4757-4721-8. DOI: 10.1007/978-1-4757-4721-8. URL: http://link.springer.com/10.1007/978-1-4757-4721-8 (visited on 05/05/2023).

[22] Edward F. Moore. "Gedanken-Experiments on Sequential Machines". In: *Automata Studies*. Annals of Mathematics Studies, No. 34. Princeton University Press, Princeton, N.J., 1956, pp. 129-153.

[23] Daniela Petrişan and Thomas Colcombet. "Automata Minimization: A Functorial Approach". In: *Logical Methods in Computer Science* Volume 16, Issue 1 (Mar. 23, 2020). DOI: 10.23638/LMCS-16(1:32)2020. URL: https://lmcs.episciences.org/6213/pdf (visited on 04/12/2023).

[24] Jacques Sakarovitch. "1. The Simplest Possible Machine". In: *Elements of Automata Theory*. Ed. by Thomas Reuben. Cambridge: Cambridge University Press, 2009, pp. 49-216. DOI: 10.1017/CB09781139195218.005.

[25] M. P. Schützenberger. "On the Definition of a Family of Automata". In: *Information and Control* 4.2 (Sept. 1, 1961), pp. 245-270. ISSN: 0019-9958. DOI: 10.1016/S0019-9958(61)80020-X. URL: https://www.sciencedirect.com/science/article/pii/S001999586180020X (visited on 05/04/2023).

[26] Jenö Szigeti. "On Limits and Colimits in the Kleisli Category". In: *Cahiers de topologie et géométrie différentielle* 24.4 (1983), pp. 381-391. ISSN: 2681-2398. URL: http://www.numdam.org/item/?id=CTGDC_1983_24_4_381_0 (visited on 05/23/2023).

[27] Henning Urbat and Lutz Schröder. "Automata Learning: An Algebraic Approach". In: *Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science*. LICS '20. New York, NY, USA: Association for Computing Machinery, July 8, 2020, pp. 900-914. ISBN: 978-1-4503-7104-9. DOI: 10.1145/3373718.3394775. URL: https://dl.acm.org/doi/10.1145/3373718.3394775 (visited on 05/04/2023).

[28] Gerco van Heerdt, Matteo Sammartino, and Alexandra Silva. "Learning Automata with Side-Effects". In: *Coalgebraic Methods in Computer Science*. Ed. by Daniela Petrişan and Jurriaan Rot. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2020, pp. 68-89. ISBN: 978-3-030-57201-3. DOI: 10.1007/978-3-030-57201-3_5.

[29] Juan Miguel Vilar. "Query Learning of Subsequential Transducers". In: *Grammatical Interference: Learning Syntax from Sentences*. Ed. by Laurent Miclet and Colin de la Higuera. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1996, pp. 72-83. ISBN: 978-3-540-70678-6. DOI: 10.1007/BFb0033343.

[30] Thorsten Wißmann et al. "A Coalgebraic View on Reachability". In: *Commentaciones Mathematicae Universitatis Carolinae* 60.4 (2019), pp. 605-638. ISSN: 0010-2628 (print). URL: https://dml.cz/handle/10338.dmlcz/147977 (visited on 05/05/2023).
A. Proofs for Section 1 (Introduction)

**Lemma 1.1.** Let $A = \{a\}$, $\Sigma = \{\alpha, \beta, \gamma\}$, let $\Sigma/\sim$ be the monoid $\Sigma^*$ with the additional assumption that $\alpha\beta = \beta\alpha$ and let $\pi : \Sigma^* \to \Sigma/\sim$ be the corresponding quotient. Consider the function $f : A^* \to \Sigma/\sim$ that maps $a^n$ to $\alpha^n\beta^n\gamma = (\alpha\beta)^n\gamma$.

$f$ is recognized by a finite transducer with outputs in $\Sigma/\sim$, yet learning a transducer that recognizes any function $f' : A^* \to \Sigma^*$ such that $f = f' \circ \pi$ with Vilar's algorithm will never terminate if the oracle replies to the membership query for $a^n$ with $\alpha^n\beta^n\gamma \in \Sigma^*$ (which differs from $(\alpha\beta)^n\gamma$ in $\Sigma^*$ but not in $\Sigma/\sim$).

*Proof.* $f$ is recognized by the $\Sigma/\sim$-transducer (Definition 4.9) with one state $s$ that is initial, initial value $v_0 = \epsilon$, transition function $a \odot s = (\alpha\beta, s)$ and termination function $t(s) = \gamma$.

Consider now the run of Vilar's algorithm (Algorithm 4 with $M = \Sigma^*$ and $M^\times = \{\epsilon\}$) with the oracle answering the membership query for $a^n$ with $f'(a^n) = \alpha^n\beta^n\gamma$. We start with $Q = T = \{e\}$, $\Lambda(e) = \gamma$, $\Lambda(a) = \alpha\beta\gamma$ and $R(e, e) = R(a, e) = \epsilon$, where $\Lambda(w)$ for $w \in Q \cup QA$ is the longest common prefix of the $\{f'(wt) | t \in T\}$ and $R(w,t)$ is the suffix such that $f'(wt) = \Lambda(w)R(w,t)$.

Since $\Lambda(e) = \gamma$ is not a prefix of $\Lambda(a) = \alpha\beta\gamma$, there is a consistency issue and we add $a$ to $T$. Taking $n=0$, we are now in the configuration $C_n$ given by $Q = Q_n = \{a^k \mid k \le n\}$, $T = \{e, a\}$, and $\Lambda(a^k) = \alpha^k$, $R(a^k, e) = \beta^k\gamma$ and $R(a^k, a) = \alpha\beta^{k+1}\gamma$ for every $k \le n+1$ (since the oracle replies to the membership query for $a^k$ with $\alpha^k\beta^k\gamma$ and to that for $a^k a$ with $\alpha^{k+1}\beta^{k+1}\gamma$).

Suppose now we are in the configuration $C_n$ for some $n \in \mathbb{N}$. Then there is a closure issue, since for all $k \le n$, $R(a^k, e) = \beta^k\gamma \ne \beta^{n+1}\gamma = R(a^{n+1}, e)$. We thus add $a^{n+1}$ to $Q$. To compute $\Lambda(a^{n+2})$, $R(a^{n+2}, e)$ and $R(a^{n+2}, a)$, we make a membership query for $a^{n+3}$: the oracle answers with $f'(a^{n+3}) = \alpha^{n+3}\beta^{n+3}\gamma$. The longest common prefix of $f'(a^{n+2}) = \Lambda(a^{n+1})R(a^{n+1}, a) = \alpha^{n+2}\beta^{n+2}\gamma$ and $f'(a^{n+2}a) = \alpha^{n+3}\beta^{n+3}\gamma$ is thus $\alpha^{n+2}$, and the corresponding suffixes are $R(a^{n+2}, e) = \beta^{n+2}\gamma$ and $R(a^{n+2}, a) = \alpha\beta^{n+3}\gamma$: we are now in the configuration $C_{n+1}$.

Hence the run of the algorithm never terminates and never even reaches an equivalence query, as it must first go through all the configurations $C_n$ for $n \in \mathbb{N}$. $\square$

B. Proofs for Section 3 (An algorithm for minimizing
$(C, X, Y)$-automata)

**Lemma 3.1** ([23, Remark 2.5]). *The dual of the ($\mathcal{E}$, $\mathcal{M}$)-factorization Obs $\mathcal{A}$ in Auto($\mathcal{L}$) is the ($\mathcal{M}^{\text{op}}$, $\mathcal{E}^{\text{op}}$)-factorization Reach $\mathcal{A}^{\text{op}}$ in Auto($\mathcal{L}^{\text{op}}$).*

*Proof.* Obs $\mathcal{A}$ is given by the ($\mathcal{E}$, $\mathcal{M}$)-factorization $\mathcal{A} \to \text{Obs } \mathcal{A} \to \mathcal{A}^{\text{final}}$ in Auto($\mathcal{L}$). Its dual is thus given by the ($\mathcal{M}^{\text{op}}$, $\mathcal{E}^{\text{op}}$)-factorization ($\mathcal{A}^{\text{final}})^{\text{op}} \to (\text{Obs } \mathcal{A})^{\text{op}} \to \mathcal{A}^{\text{op}}$ in Auto($\mathcal{L}$)$^{\text{op}}$. But $\mathcal{A}^{\text{final}}$ is final in Auto($\mathcal{L}$) hence its dual is initial in Auto($\mathcal{L}$)$^{\text{op}}$. Similarly, ($\mathcal{M}^{\text{op}}$, $\mathcal{E}^{\text{op}}$) is a factorization system in Auto($\mathcal{L}$)$^{\text{op}}$ [8, Proposition 14.3], hence $(\text{Obs } \mathcal{A})^{\text{op}}$ is none other than Reach $\mathcal{A}^{\text{op}}$. $\square$
A. Proofs for Section 1 (Introduction)

**Lemma 1.1.** Let $A = \{a\}$, $\Sigma = \{\alpha, \beta, \gamma\}$, let $\Sigma/\sim$ be the monoid $\Sigma^*$ with the additional assumption that $\alpha\beta = \beta\alpha$ and let $\pi : \Sigma^* \to \Sigma/\sim$ be the corresponding quotient. Consider the function $f : A^* \to \Sigma/\sim$ that maps $a^n$ to $\alpha^n\beta^n\gamma = (\alpha\beta)^n\gamma$.

$f$ is recognized by a finite transducer with outputs in $\Sigma/\sim$, yet learning a transducer that recognizes any function $f' : A^* \to \Sigma^*$ such that $f = f' \circ \pi$ with Vilar's algorithm will never terminate if the oracle replies to the membership query for $a^n$ with $\alpha^n\beta^n\gamma \in \Sigma^*$ (which differs from $(\alpha\beta)^n\gamma$ in $\Sigma^*$ but not in $\Sigma/\sim$).

*Proof.* $f$ is recognized by the $\Sigma/\sim$-transducer (Definition 4.9) with one state $s$ that is initial, initial value $v_0 = \epsilon$, transition function $a \odot s = (\alpha\beta, s)$ and termination function $t(s) = \gamma$.

Consider now the run of Vilar's algorithm (Algorithm 4 with $M = \Sigma^*$ and $M^\times = \{\epsilon\}$) with the oracle answering the membership query for $a^n$ with $f'(a^n) = \alpha^n\beta^n\gamma$. We start with $Q = T = \{e\}$, $\Lambda(e) = \gamma$, $\Lambda(a) = \alpha\beta\gamma$ and $R(e, e) = R(a, e) = \epsilon$, where $\Lambda(w)$ for $w \in Q \cup QA$ is the longest common prefix of the $\{f'(wt) | t \in T\}$ and $R(w,t)$ is the suffix such that $f'(wt) = \Lambda(w)R(w,t)$.

Since $\Lambda(e) = \gamma$ is not a prefix of $\Lambda(a) = \alpha\beta\gamma$, there is a consistency issue and we add $a$ to $T$. Taking $n=0$, we are now in the configuration $C_n$ given by $Q = Q_n = \{a^k \mid k \le n\}$, $T = \{e, a\}$, and $\Lambda(a^k) = \alpha^k$, $R(a^k, e) = \beta^k\gamma$ and $R(a^k, a) = \alpha\beta^{k+1}\gamma$ for every $k \le n+1$ (since the oracle replies to the membership query for $a^k$ with $\alpha^k\beta^k\gamma$ and to that for $a^k a$ with $\alpha^{k+1}\beta^{k+1}\gamma$).

Suppose now we are in the configuration $C_n$ for some $n \in \mathbb{N}$. Then there is a closure issue, since for all $k \le n$, $R(a^k, e) = \beta^k\gamma \ne \beta^{n+1}\gamma = R(a^{n+1}, e)$. We thus add $a^{n+1}$ to $Q$. To compute $\Lambda(a^{n+2})$, $R(a^{n+2}, e)$ and $R(a^{n+2}, a)$, we make a membership query for $a^{n+3}$: the oracle answers with $f'(a^{n+3}) = \alpha^{n+3}\beta^{n+3}\gamma$. The longest common prefix of $f'(a^{n+2}) = \Lambda(a^{n+1})R(a^{n+1}, a) = \alpha^{n+2}\beta^{n+2}\gamma$ and $f'(a^{n+2}a) = \alpha^{n+3}\beta^{n+3}\gamma$ is thus $\alpha^{n+2}$, and the corresponding suffixes are $R(a^{n+2}, e) = \beta^{n+2}\gamma$ and $R(a^{n+2}, a) = \alpha\beta^{n+3}\gamma$: we are now in the configuration $C_{n+1}$.

Hence the run of the algorithm never terminates and never even reaches an equivalence query, as it must first go through all the configurations $C_n$ for $n \in \mathbb{N}$. $\square$

B. Proofs for Section 3 (An algorithm for minimizing
$(C, X, Y)$-automata)

**Lemma 3.1** ([23, Remark 2.5]). *The dual of the ($\mathcal{E}$, $\mathcal{M}$)-factorization Obs $\mathcal{A}$ in Auto($\mathcal{L}$) is the ($\mathcal{M}^{\text{op}}$, $\mathcal{E}^{\text{op}}$)-factorization Reach $\mathcal{A}^{\text{op}}$ in Auto($\mathcal{L}^{\text{op}}$).*

*Proof.* Obs $\mathcal{A}$ is given by the ($\mathcal{E}$, $\mathcal{M}$)-factorization $\mathcal{A} \to \text{Obs } \mathcal{A} \to \mathcal{A}^{\text{final}}$ in Auto($\mathcal{L}$). Its dual is thus given by the ($\mathcal{M}^{\text{op}}$, $\mathcal{E}^{\text{op}}$)-factorization ($\mathcal{A}^{\text{final}})^{\text{op}} \to (\text{Obs } \mathcal{A})^{\text{op}} \to \mathcal{A}^{\text{op}}$ in Auto($\mathcal{L}$)$^{\text{op}}$. But $\mathcal{A}^{\text{final}}$ is final in Auto($\mathcal{L}$) hence its dual is initial in Auto($\mathcal{L}$)$^{\text{op}}$. Similarly, ($\mathcal{M}^{\text{op}}$, $\mathcal{E}^{\text{op}}$) is a factorization system in Auto($\mathcal{L}$)$^{\text{op}}$ [8, Proposition 14.3], hence $(\text{Obs } \mathcal{A})^{\text{op}}$ is none other than Reach $\mathcal{A}^{\text{op}}$. $\square$
**Lemma 3.4.** (similar to [10, Lemma 31]) For any $w \in A^*$ and $Q' \subseteq A^*$ such that $Qw = \{qw | q \in Q\} \subseteq Q'$, there is a unique morphism $\kappa_{Q'w}^{Q'} / \mathcal{A}(w) : Q/\mathcal{A}(\mathbf{st}) \to Q'/\mathcal{A}(\mathbf{st})$ making the two squares in the diagram below commute. Moreover, if $uv = w$ and $Qw \subseteq Q'v \subseteq Q''$, then $\kappa_{Q'v}^{Q''} / \mathcal{A}(v) \circ \kappa_{Q'u}^{Q'} / \mathcal{A}(u) = \kappa_{Q'w}^{Q''} / \mathcal{A}(w)$.

*Proof.* $\kappa_{Q'w}^{Q'} / \mathcal{A}(w)$ arises immediately by the diagonal fill-in property of $(\mathcal{E}, \mathcal{M})$ applied to $m_{Q'} \circ (e_{Q'} \circ \coprod_{q \in Q} \kappa_q) = (\mathcal{A}(w) \circ m_Q) \circ e_Q$. Since this diagonal fill-in is unique, by composing these diagrams we get the last equality. $\square$

**Theorem 3.6.** If $\mathcal{A}(\mathbf{st})$ is $\mathcal{M}$-noetherian, Algorithm 2 is correct, terminates, and the condition on line 5 is satisfied at most length$_{\mathcal{M}}(m_{\emptyset} : \emptyset / \mathcal{A}(\mathbf{st}) \to \mathcal{A}(\mathbf{st}))$ times.

*Proof.* We first focus on termination, then on correctness.

**Termination.** Every time line 7 is executed, the condition on line 5 must hold. Hence if we write $Q_n$ for the value of $Q_{\text{done}}$ after $n$ executions of line 7, then $Q_0 = \emptyset$ and $(Q_n / \mathcal{A}(\mathbf{st}) \to Q_{n+1} / \mathcal{A}(\mathbf{st}))_n$ forms a strict chain of $\mathcal{M}$-subobjects of $\mathcal{A}(\mathbf{st})$ (it is strict because the morphisms it contains are not $\mathcal{E}$-morphisms hence not isomorphisms). But $\mathcal{A}(\mathbf{st})$ is $\mathcal{M}$-noetherian by assumption hence this chain must be finite and line 7 and thus line 6 must be executed a finite number of times, and in particular at most length$_{\mathcal{M}} m_{Q_0} = \text{length}_{\mathcal{M}} m_{\emptyset}$ times. But we only add at most $|\mathcal{A}|$ elements to the to-do list on line 6, hence the while loop is run a finite number of times, in particular at most $1 + |\mathcal{A}| \text{ length}_{\mathcal{M}}(m_{\emptyset})$ times.

**Correctness.** Let us first show some preliminary results.

**Lemma B.1.** Consider the following diagonal fill-in (where $g$ is an $\mathcal{M}$-morphism):

$$ \begin{array}{ccc} Y_1 & \xrightarrow{e_y} & Y_1/Y_2 \xrightarrow{m_y} Y_2 \\ \frown & & \frown_{f/g} \\ X_1 & \xrightarrow{e_x} & X_1/X_2 \xrightarrow{m_x} X_2 \end{array} $$

$f/g$ is an $\mathcal{M}$-morphism, and it is an isomorphism if and only if there is an $h$ such that the following diagram commutes:

$$ \begin{array}{ccc} Y_1 & \xrightarrow{e_y} & Y_1/Y_2 \\ \frown & & \frown_{f/g} \\ X_1 & \xrightarrow{e_x} & X_1/X_2 \end{array} $$

*Proof.* $f/g$ is an $\mathcal{M}$-morphism by [8, Proposition 14.9(1)]. If it is an isomorphism, then $h = (f/g)^{-1} \circ e_y$ immediately makes the diagram above commute.

Conversely, assume such an $h$ exists and $(\mathcal{E}, \mathcal{M})$-factor it as $h = m \circ e : Y_1 \to Z \to X_1/X_2$. By unicity of the diagonal fill-in, there is an isomorphism $\chi : Y_1/Y_2 \cong Z$ such
**Lemma 3.4.** (similar to [10, Lemma 31]) For any $w \in A^*$ and $Q' \subseteq A^*$ such that $Qw = \{qw | q \in Q\} \subseteq Q'$, there is a unique morphism $\kappa_{Q'w}^{Q'} / \mathcal{A}(w) : Q/\mathcal{A}(\mathbf{st}) \to Q'/\mathcal{A}(\mathbf{st})$ making the two squares in the diagram below commute. Moreover, if $uv = w$ and $Qw \subseteq Q'v \subseteq Q''$, then $\kappa_{Q'v}^{Q''} / \mathcal{A}(v) \circ \kappa_{Q'u}^{Q'} / \mathcal{A}(u) = \kappa_{Q'w}^{Q''} / \mathcal{A}(w)$.

*Proof.* $\kappa_{Q'w}^{Q'} / \mathcal{A}(w)$ arises immediately by the diagonal fill-in property of $(\mathcal{E}, \mathcal{M})$ applied to $m_{Q'} \circ (e_{Q'} \circ \coprod_{q \in Q} \kappa_q) = (\mathcal{A}(w) \circ m_Q) \circ e_Q$. Since this diagonal fill-in is unique, by composing these diagrams we get the last equality. $\square$

**Theorem 3.6.** If $\mathcal{A}(\mathbf{st})$ is $\mathcal{M}$-noetherian, Algorithm 2 is correct, terminates, and the condition on line 5 is satisfied at most length$_{\mathcal{M}}(m_{\emptyset} : \emptyset / \mathcal{A}(\mathbf{st}) \to \mathcal{A}(\mathbf{st}))$ times.

*Proof.* We first focus on termination, then on correctness.

**Termination.** Every time line 7 is executed, the condition on line 5 must hold. Hence if we write $Q_n$ for the value of $Q_{\text{done}}$ after $n$ executions of line 7, then $Q_0 = \emptyset$ and $(Q_n / \mathcal{A}(\mathbf{st}) \to Q_{n+1} / \mathcal{A}(\mathbf{st}))_n$ forms a strict chain of $\mathcal{M}$-subobjects of $\mathcal{A}(\mathbf{st})$ (it is strict because the morphisms it contains are not $\mathcal{E}$-morphisms hence not isomorphisms). But $\mathcal{A}(\mathbf{st})$ is $\mathcal{M}$-noetherian by assumption hence this chain must be finite and line 7 and thus line 6 must be executed a finite number of times, and in particular at most length$_{\mathcal{M}} m_{Q_0} = \text{length}_{\mathcal{M}} m_{\emptyset}$ times. But we only add at most $|\mathcal{A}|$ elements to the to-do list on line 6, hence the while loop is run a finite number of times, in particular at most $1 + |\mathcal{A}| \text{ length}_{\mathcal{M}}(m_{\emptyset})$ times.

**Correctness.** Let us first show some preliminary results.

**Lemma B.1.** Consider the following diagonal fill-in (where $g$ is an $\mathcal{M}$-morphism):

$$ \begin{array}{ccc} Y_1 & \xrightarrow{e_y} & Y_1/Y_2 \xrightarrow{m_y} Y_2 \\ \frown & & \frown_{f/g} \\ X_1 & \xrightarrow{e_x} & X_1/X_2 \xrightarrow{m_x} X_2 \end{array} $$

$f/g$ is an $\mathcal{M}$-morphism, and it is an isomorphism if and only if there is an $h$ such that the following diagram commutes:

$$ \begin{array}{ccc} Y_1 & \xrightarrow{e_y} & Y_1/Y_2 \\ \frown & & \frown_{f/g} \\ X_1 & \xrightarrow{e_x} & X_1/X_2 \end{array} $$

*Proof.* $f/g$ is an $\mathcal{M}$-morphism by [8, Proposition 14.9(1)]. If it is an isomorphism, then $h = (f/g)^{-1} \circ e_y$ immediately makes the diagram above commute.

Conversely, assume such an $h$ exists and $(\mathcal{E}, \mathcal{M})$-factor it as $h = m \circ e : Y_1 \to Z \to X_1/X_2$. By unicity of the diagonal fill-in, there is an isomorphism $\chi : Y_1/Y_2 \cong Z$ such
that $e = \chi \circ e_y$ and $f/g \circ m \circ \chi = \text{id}$. We claim that $m \circ \chi$ is the inverse of $f/g$: we already have that $f/g \circ m \circ \chi = \text{id}$, but also

$$ 
\begin{aligned}
g \circ m_x \circ m \circ \chi \circ f/g &= m_y \circ f/g \circ m \circ \chi \circ f/g \\
&= m_y \circ f/g \\
&= g \circ m_x
\end{aligned}
$$

and

$$ 
\begin{aligned}
m \circ \chi \circ f/g \circ e_x &= m \circ \chi \circ e_y \circ f \\
&= h \circ f \\
&= e_x
\end{aligned}
$$

hence by unicity of the diagonal fill-in (within the square composed of two copies of $e_x$ and $g \circ m_x$), $m \circ \chi \circ f/g = \text{id}$. $\square$

**Definition B.2** (prefix-closedness). $Q \subseteq A^*$ is said to be prefix-closed if it contains the empty word and if for every $q \in A^*$ and $a \in A$, if $qa \in Q$ then $q \in Q$.

**Proposition B.3.** Let $Q \subseteq A^*$ be prefix-closed. If $\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st})$ is an isomorphism, then so is $\kappa_Q^{A^*} / \mathcal{A}(\text{st})$.

*Proof.* We apply Lemma B.1 and build a morphism $h : \coprod_{A^*} \mathcal{A}(\text{in}) \to Q/\mathcal{A}(\text{st})$ that makes the corresponding diagram commute. We thus let $h \circ \kappa_\epsilon = e_Q \circ \kappa_\epsilon$ (this is possible because $Q$ is prefix-closed hence contains $\epsilon$) and, by induction, for $w \in A^*$ and $a \in A$ we let $h \circ \kappa_{wa} = (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} \circ \kappa_{Q \cdot a}^{Q \cup QA} / \mathcal{A}(a) \circ h \circ \kappa_w$.

We then have that $e_Q = h \circ [\kappa_q]_{q \in Q}$. The proof is by induction on $Q$, which is possible because $Q$ is prefix-closed. We already have $h \circ \kappa_\epsilon = e_Q \circ \kappa_\epsilon$ by definition, and if $h \circ \kappa_w = e_Q \circ \kappa_w$, then for $a \in A$ we have

$$ 
\begin{aligned}
h \circ \kappa_{wa} &= (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} \circ \kappa_{Q \cdot a}^{Q \cup QA} / \mathcal{A}(a) \circ h \circ \kappa_w \\
&= (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} \circ \kappa_{Q \cdot a}^{Q \cup QA} / \mathcal{A}(a) \circ e_Q \circ \kappa_w \\
&= (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} \circ e_Q \cup \mathcal{QA} \circ [\kappa_{qa}]_{q \in Q} \circ \kappa_w \\
&= (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} \circ e_Q \cup \mathcal{QA} \circ [\kappa_q]_{q \in Q} \circ \kappa_{wa} \\
&= e_Q \circ \kappa_{wa}
\end{aligned}
$$

Moreover, for all $w \in A^*$, we have $\kappa_{Q \cdot w}^{A^*} / \mathcal{A}(w) = \kappa_{Q \cup QA \cdot w}^{A^*} / \mathcal{A}(w) \circ \kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st})$ hence $\kappa_{Q \cdot w}^{A^*} / \mathcal{A}(w) \circ (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} = \kappa_{Q \cup QA \cdot w}^{A^*} / \mathcal{A}(w)$ and it follows by induction
that $e = \chi \circ e_y$ and $f/g \circ m \circ \chi = \text{id}$. We claim that $m \circ \chi$ is the inverse of $f/g$: we already have that $f/g \circ m \circ \chi = \text{id}$, but also

$$ 
\begin{aligned}
g \circ m_x \circ m \circ \chi \circ f/g &= m_y \circ f/g \circ m \circ \chi \circ f/g \\
&= m_y \circ f/g \\
&= g \circ m_x
\end{aligned}
$$

and

$$ 
\begin{aligned}
m \circ \chi \circ f/g \circ e_x &= m \circ \chi \circ e_y \circ f \\
&= h \circ f \\
&= e_x
\end{aligned}
$$

hence by unicity of the diagonal fill-in (within the square composed of two copies of $e_x$ and $g \circ m_x$), $m \circ \chi \circ f/g = \text{id}$. $\square$

**Definition B.2** (prefix-closedness). $Q \subseteq A^*$ is said to be *prefix-closed* if it contains the empty word and if for every $q \in A^*$ and $a \in A$, if $qa \in Q$ then $q \in Q$.

**Proposition B.3.** Let $Q \subseteq A^*$ be prefix-closed. If $\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st})$ is an isomorphism, then so is $\kappa_Q^{A^*} / \mathcal{A}(\text{st})$.

*Proof.* We apply Lemma B.1 and build a morphism $h : \coprod_{A^*} \mathcal{A}(\text{in}) \to Q/\mathcal{A}(\text{st})$ that makes the corresponding diagram commute. We thus let $h \circ \kappa_\epsilon = e_Q \circ \kappa_\epsilon$ (this is possible because $Q$ is prefix-closed hence contains $\epsilon$) and, by induction, for $w \in A^*$ and $a \in A$ we let $h \circ \kappa_{wa} = (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} \circ \kappa_{Q \cdot a}^{Q \cup QA} / \mathcal{A}(a) \circ h \circ \kappa_w$.

We then have that $e_Q = h \circ [\kappa_q]_{q \in Q}$. The proof is by induction on $Q$, which is possible because $Q$ is prefix-closed. We already have $h \circ \kappa_\epsilon = e_Q \circ \kappa_\epsilon$ by definition, and if $h \circ \kappa_w = e_Q \circ \kappa_w$, then for $a \in A$ we have

$$ 
\begin{aligned}
h \circ \kappa_{wa} &= (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} \circ \kappa_{Q \cdot a}^{Q \cup QA} / \mathcal{A}(a) \circ h \circ \kappa_w \\
&= (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} \circ \kappa_{Q \cdot a}^{Q \cup QA} / \mathcal{A}(a) \circ e_Q \circ \kappa_w \\
&= (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} \circ e_Q \cup \mathcal{QA} \circ [\kappa_{qa}]_{q \in Q} \circ \kappa_w \\
&= (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} \circ e_Q \cup \mathcal{QA} \circ [\kappa_q]_{q \in Q} \circ \kappa_{wa} \\
&= e_Q \circ \kappa_{wa}
\end{aligned}
$$

Moreover, for all $w \in A^*$, we have $\kappa_{Q \cdot w}^{A^*} / \mathcal{A}(w) = \kappa_{Q \cup QA \cdot w}^{A^*} / \mathcal{A}(w) \circ \kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st})$ hence $\kappa_{Q \cdot w}^{A^*} / \mathcal{A}(w) \circ (\kappa_Q^{Q \cup QA} / \mathcal{A}(\text{st}))^{-1} = \kappa_{Q \cup QA \cdot w}^{A^*} / \mathcal{A}(w)$ and it follows by induction
(again, thanks to the prefix-closedness of $\mathcal{Q}$) that

$$ \begin{aligned} \kappa_Q^{A^*} / \mathcal{A}(\mathbf{st}) \circ h \circ \kappa_w &= \kappa_{Q \cdot w}^{A^*} / \mathcal{A}(w) \circ e_Q \circ \kappa_{\epsilon} \\ &= e_{A^*} \circ [\kappa_{qw}]_{q \in Q} \circ \kappa_{\epsilon} \\ &= e_{A^*} \circ \kappa_w \end{aligned} $$

hence that $\kappa_Q^{A^*} / \mathcal{A}(\mathbf{st}) \circ h = e_{A^*}$. $\square$

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

**Lemma B.4** (generalization of [10, Lemma 40]). For every $k$ in some set $K$, let $P_k \subseteq Q_k \subseteq A^*$ be such that $\kappa_{P_k}^{Q_k} / \mathcal{A}(\mathbf{st})$ is an isomorphism. Also assume that $Q_k \cap Q_{k'} = P_k \cap P_{k'}$ for all $k \neq k' \in K$. Then, $\kappa_{\cup_k Q_k}^{\cup_k P_k} / \mathcal{A}(\mathbf{st})$ is also an isomorphism.

*Proof.* We apply Lemma B.1 and build $h: \coprod_{\cup_k Q_k} \mathcal{A}(\mathbf{in}) \to \cup_k P_k / \mathcal{A}(\mathbf{st})$. If $p \in P_l$ for some $l \in K$, set $h \circ \kappa_p = e_{\cup_k P_k} \circ \kappa_p$. Otherwise, for $q \in Q_l$ for some (unique) $l \in K$, set $h \circ \kappa_q = \kappa_{P_l}^{\cup_k P_k} / \mathcal{A}(\mathbf{st}) \circ h_l \circ \kappa_q$ where $h_l: \coprod_{Q_l} \mathcal{A}(\mathbf{in}) \to P_l / \mathcal{A}(\mathbf{st})$ witnesses that $\kappa_{P_l}^{Q_l} / \mathcal{A}(\mathbf{st})$ is an isomorphism.

We then have by definition $h \circ [\kappa_w]_{w \in \cup_k P_k} = e_{\cup_k P_k}$ and in particular $\kappa_{\cup_k Q_k}^{\cup_k P_k} / \mathcal{A}(\mathbf{st}) \circ h \circ \kappa_p = e_{\cup_k Q_k} \circ \kappa_p$ when $p \in \cup_{k \in K} P_k$. Moreover, for some $l \in K$ and $q \in Q_l$ such that $q \notin \cup_{k \in K} P_k$, we have

$$ \begin{aligned} \kappa_{\cup_k P_k}^{\cup_k Q_k} / \mathcal{A}(\mathbf{st}) \circ h \circ \kappa_q &= \kappa_{P_l}^{\cup_k Q_k} / \mathcal{A}(\mathbf{st}) \circ h_l \circ \kappa_q \\ &= \kappa_{Q_l}^{\cup_k Q_k} / \mathcal{A}(\mathbf{st}) \circ \kappa_{P_l}^{Q_l} / \mathcal{A}(\mathbf{st}) \circ h_l \circ \kappa_q \\ &= \kappa_{Q_l}^{\cup_k Q_k} / \mathcal{A}(\mathbf{st}) \circ e_{Q_l} \circ \kappa_q \\ &= e_{\cup_k Q_k} \circ \kappa_q \end{aligned} $$

hence $h$ has the relevant diagram commute. $\square$

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

We now have everything we need to show the algorithm is correct.

First note that it is easy to show by induction that all the subsets that go through to-do list are pairwise disjoint, hence why we use disjoint unions in the algorithm. But the fact that these unions are disjoint is not needed for the proof of correctness.

Consider some $q \in Q_{done}$ after the algorithm has stopped, and some $a \in A$. The only way to get added to $Q_{done}$ is through line 7 of the algorithm, hence $q$ must have belonged to some $\mathcal{Q}$. Hence there was an $\tilde{\mathcal{A}}$ such that $a \in \tilde{\mathcal{A}}$ for which $\mathcal{Q}\tilde{\mathcal{A}}$ must have been added to the to-do list and thus have been considered in a run of the if statement on line 5. During this run, either $\kappa_{Q_{done}}^{Q_{done} \cup Q\tilde{\mathcal{A}}} / \mathcal{A}(\mathbf{st})$ was already an isomorphism and nothing changed; or it was not, in which case $\mathcal{Q}\tilde{\mathcal{A}}$ was added to $Q_{done}$ so that $Q_{done} = Q_{done} \cup \mathcal{Q}\tilde{\mathcal{A}}$ right after, and we would thus still get that $\kappa_{Q_{done}}^{Q_{done} \cup Q\tilde{\mathcal{A}}} / \mathcal{A}(\mathbf{st})$ had become an $\mathcal{E}$-morphism
(again, thanks to the prefix-closedness of $\mathcal{Q}$) that

$$ 
\begin{align*}
\kappa_Q^{A^*} / \mathcal{A}(\mathbf{st}) \circ h \circ \kappa_w &= \kappa_{Q \cdot w}^{A^*} / \mathcal{A}(w) \circ e_Q \circ \kappa_{\epsilon} \\
&= e_{A^*} \circ [\kappa_{qw}]_{q \in \mathcal{Q}} \circ \kappa_{\epsilon} \\
&= e_{A^*} \circ \kappa_w
\end{align*}
$$

hence that $\kappa_Q^{A^*} / \mathcal{A}(\mathbf{st}) \circ h = e_{A^*}$. $\square$

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

**Lemma B.4** (generalization of [10, Lemma 40]). For every $k$ in some set $K$, let $P_k \subseteq Q_k \subseteq A^*$ be such that $\kappa_{P_k}^{Q_k} / \mathcal{A}(\mathbf{st})$ is an isomorphism. Also assume that $Q_k \cap Q_{k'} = P_k \cap P_{k'}$ for all $k \neq k' \in K$. Then, $\kappa_{\cup_k Q_k}^{\cup_k P_k} / \mathcal{A}(\mathbf{st})$ is also an isomorphism.

*Proof.* We apply Lemma B.1 and build $h: \coprod_{\cup_k Q_k} \mathcal{A}(\mathbf{in}) \to \cup_k P_k / \mathcal{A}(\mathbf{st})$. If $p \in P_l$ for some $l \in K$, set $h \circ \kappa_p = e_{\cup_k P_k} \circ \kappa_p$. Otherwise, for $q \in Q_l$ for some (unique) $l \in K$, set $h \circ \kappa_q = \kappa_{P_l}^{\cup_k P_k} / \mathcal{A}(\mathbf{st}) \circ h_l \circ \kappa_q$ where $h_l: \coprod_{Q_l} \mathcal{A}(\mathbf{in}) \to P_l / \mathcal{A}(\mathbf{st})$ witnesses that $\kappa_{P_l}^{Q_l} / \mathcal{A}(\mathbf{st})$ is an isomorphism.

We then have by definition $h \circ [\kappa_w]_{w \in \cup_k P_k} = e_{\cup_k P_k}$ and in particular $\kappa_{\cup_k Q_k}^{\cup_k P_k} / \mathcal{A}(\mathbf{st}) \circ h \circ \kappa_p = e_{\cup_k Q_k} \circ \kappa_p$ when $p \in \cup_{k \in K} P_k$. Moreover, for some $l \in K$ and $q \in Q_l$ such that $q \notin \cup_{k \in K} P_k$, we have

$$ 
\begin{align*}
\kappa_{\cup_k P_k}^{\cup_k Q_k} / \mathcal{A}(\mathbf{st}) \circ h \circ \kappa_q &= \kappa_{P_l}^{\cup_k Q_k} / \mathcal{A}(\mathbf{st}) \circ h_l \circ \kappa_q \\
&= \kappa_{Q_l}^{\cup_k Q_k} / \mathcal{A}(\mathbf{st}) \circ \kappa_{P_l}^{Q_l} / \mathcal{A}(\mathbf{st}) \circ h_l \circ \kappa_q \\
&= \kappa_{Q_l}^{\cup_k Q_k} / \mathcal{A}(\mathbf{st}) \circ e_{Q_l} \circ \kappa_q \\
&= e_{\cup_k Q_k} \circ \kappa_q
\end{align*}
$$

hence $h$ has the relevant diagram commute. $\square$

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

We now have everything we need to show the algorithm is correct.

First note that it is easy to show by induction that all the subsets that go through to-do list are pairwise disjoint, hence why we use disjoint unions in the algorithm. But the fact that these unions are disjoint is not needed for the proof of correctness.

Consider some $q \in Q_{done}$ after the algorithm has stopped, and some $a \in A$. The only way to get added to $Q_{done}$ is through line 7 of the algorithm, hence $q$ must have belonged to some $\mathcal{Q}$. Hence there was an $\tilde{\mathcal{A}}$ such that $a \in \tilde{\mathcal{A}}$ for which $\mathcal{Q}\tilde{\mathcal{A}}$ must have been added to the to-do list and thus have been considered in a run of the if statement on line 5. During this run, either $\kappa_{Q_{done}}^{Q_{done} \cup Q\tilde{\mathcal{A}}} / \mathcal{A}(\mathbf{st})$ was already an isomorphism and nothing changed; or it was not, in which case $\mathcal{Q}\tilde{\mathcal{A}}$ was added to $Q_{done}$ so that $Q_{done} = Q_{done} \cup \mathcal{Q}\tilde{\mathcal{A}}$ right after, and we would thus still get that $\kappa_{Q_{done}}^{Q_{done} \cup Q\tilde{\mathcal{A}}} / \mathcal{A}(\mathbf{st})$ had become an $\mathcal{E}$-morphism
hence an isomorphism (by the dual of [8, Proposition 14.9(1)]), because the morphism
$\coprod_{Q_{done}} \mathcal{A}(\mathbf{in}) \to \coprod_{Q_{done} \cup Q\tilde{A}} \mathcal{A}(\mathbf{in})$ is an isomorphism).

By Lemma B.4, for any $Q_1 \subseteq Q_2 \subseteq A^*$, if $\kappa_{Q_1}^{Q_1 \cup Q} / \mathcal{A}(\mathbf{st})$ is an isomorphism then so is $\kappa_{Q_2}^{Q_2 \cup Q} / \mathcal{A}(\mathbf{st})$. Hence since $Q_{done}$ may only grow and since we just showed that at some point of the execution of the algorithm the morphism $\kappa_{Q_{done}}^{Q_{done} \cup Q\tilde{A}} / \mathcal{A}(\mathbf{st})$ is an isomorphism, it stays so until the algorithm stops.

Hence at the end of the algorithm, for every $q \in Q_{done}$ and $a \in A$ there is some $Q\tilde{A}$ such that $qa \in Q\tilde{A}$ and $\kappa_{Q_{done}}^{Q_{done} \cup Q\tilde{A}} / \mathcal{A}(\mathbf{st})$ is an isomorphism. Using Lemma B.4 again, we get that $\kappa_{Q_{done}}^{Q_{done} \cup Q_{done}A} / \mathcal{A}(\mathbf{st})$ is an isomorphism. But $Q_{done}$ must be prefix-closed: $\epsilon$ has gone through $Q_{todo}$ and $qa \in Q\tilde{A}$ only gets added to $Q_{todo}$ if $q \in Q$ has been added to $Q_{done}$ already. Hence Proposition B.3 applies and $\kappa_{Q_{done}}^{A*} / \mathcal{A}(\mathbf{st}) : Q_{done} / \mathcal{A}(\mathbf{st}) \cong (\text{Reach } \mathcal{A})(\mathbf{st})$ is an isomorphism at the end of the algorithm, and it is easy to check that it forms a morphism of automata between the automaton produced by the algorithm and Reach $\mathcal{A}$. $\square$

**Lemma 3.7.** For every $Q, Q' \subseteq A^*$, if the coproduct $Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st})$ exists, $[m_Q, m_{Q'}] : Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st}) \to \mathcal{A}(\mathbf{st})$ $(\mathcal{E}, \mathcal{M})$-factors into

$$m_{Q \sqcup Q'} \circ [\kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\mathbf{st}), \kappa_{Q'}^{Q' \sqcup Q'} / \mathcal{A}(\mathbf{st})] : Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st}) \twoheadrightarrow (Q \sqcup Q')/\mathcal{A}(\mathbf{st}) \twoheadrightarrow \mathcal{A}(\mathbf{st})$$

*Proof.* Factor $[m_Q, m_{Q'}] : Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st}) \to \mathcal{A}(\mathbf{st})$ as $e = [z_Q, z_{Q'}] : Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st}) \twoheadrightarrow Z$ and $m : Z \to \mathcal{A}(\mathbf{st})$. Since $e_Q + e_{Q'} : \coprod_Q \mathcal{A}(\mathbf{in}) + \coprod_{Q'} \mathcal{A}(\mathbf{in}) \twoheadrightarrow Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st})$ is an $\mathcal{E}$-morphism (as a coproduct of $\mathcal{E}$-morphisms, by the dual of [8, Proposition 14.15]), $e \circ (e_Q + e_{Q'}) : \coprod_{Q \sqcup Q'} \mathcal{A}(\mathbf{in}) \twoheadrightarrow Z$ and $m : Z \to \mathcal{A}(\mathbf{st})$ form a factorization of $[m_Q \circ e_Q, m_{Q'} \circ e_{Q'}] = [\mathcal{A}(\triangleright q \triangleleft)]_{q \in Q \sqcup Q'} : \coprod_{Q \sqcup Q'} \mathcal{A}(\mathbf{in}) \to \mathcal{A}(\mathbf{st})$ as in Definition 3.3. By unicity of the diagonal fill-in, there is an isomorphism $x : Z \cong (Q \sqcup Q')/\mathcal{A}(\mathbf{st})$ such that $m = m_{Q \sqcup Q'} \circ x$ and $x \circ e \circ (e_Q + e_{Q'}) = e_{Q \sqcup Q'}$.

In particular, $x \circ z_Q \circ e_Q = e_{Q \sqcup Q'} \circ [\kappa_q]_{q \in Q}$ and $m_{Q \sqcup Q'} \circ x \circ z_Q = m_Q$, hence by unicity of the diagonal fill-in $x \circ z_Q = \kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\mathbf{st})$. The same results holds for $Q'$ hence $[m_Q, m_Q'] = (m \circ x^{-1}) \circ [x \circ z_Q, x \circ z_{Q'}]$ yields the expected factorization. $\square$

**Lemma 3.8.** For every $Q \subseteq A^*$, $\mathcal{A}(a) \circ m_Q (\mathcal{E}, \mathcal{M})$-factors into $m_{Qa} \circ \kappa_{Q \cdot a}^{Qa} / \mathcal{A}(\mathbf{st}) : Q/\mathcal{A}(\mathbf{st}) \twoheadrightarrow Qa/\mathcal{A}(\mathbf{st}) \twoheadrightarrow \mathcal{A}(\mathbf{st})$.

*Proof.* The equality holds by definition of $\kappa_{Q \cdot a}^{Qa} / \mathcal{A}(\mathbf{st})$ in Lemma 3.4. This morphism is an $\mathcal{E}$-morphism because $[\kappa_{qa}]_{q \in Q}$ is an isomorphism hence the dual of [8, Proposition 14.9(1)] applies. $\square$

**Lemma 3.10.** If $\kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\mathbf{st}) : Q/\mathcal{A}(\mathbf{st}) \twoheadrightarrow (Q \sqcup Q')/\mathcal{A}(\mathbf{st})$ is an isomorphism then

$$m_{Q'} = m_Q \circ (\kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\mathbf{st}))^{-1} \circ (\kappa_{Q'}^{Q' \sqcup Q'} / \mathcal{A}(\mathbf{st}))$$
hence an isomorphism (by the dual of [8, Proposition 14.9(1)]), because the morphism $\coprod_{Q_{done}} \mathcal{A}(\mathbf{in}) \to \coprod_{Q_{done} \cup Q\tilde{A}} \mathcal{A}(\mathbf{in})$ is an isomorphism).

By Lemma B.4, for any $Q_1 \subseteq Q_2 \subseteq A^*$, if $\kappa_{Q_1}^{Q_1 \cup Q} / \mathcal{A}(\mathbf{st})$ is an isomorphism then so is $\kappa_{Q_2}^{Q_2 \cup Q} / \mathcal{A}(\mathbf{st})$. Hence since $Q_{done}$ may only grow and since we just showed that at some point of the execution of the algorithm the morphism $\kappa_{Q_{done}}^{Q_{done} \cup Q\tilde{A}} / \mathcal{A}(\mathbf{st})$ is an isomorphism, it stays so until the algorithm stops.

Hence at the end of the algorithm, for every $q \in Q_{done}$ and $a \in A$ there is some $Q\tilde{A}$ such that $qa \in Q\tilde{A}$ and $\kappa_{Q_{done}}^{Q_{done} \cup Q\tilde{A}} / \mathcal{A}(\mathbf{st})$ is an isomorphism. Using Lemma B.4 again, we get that $\kappa_{Q_{done}}^{Q_{done} \cup Q_{done}A} / \mathcal{A}(\mathbf{st})$ is an isomorphism. But $Q_{done}$ must be prefix-closed: $\epsilon$ has gone through $Q_{todo}$ and $qa \in Q\tilde{A}$ only gets added to $Q_{todo}$ if $q \in Q$ has been added to $Q_{done}$ already. Hence Proposition B.3 applies and $\kappa_{Q_{done}}^{A*} / \mathcal{A}(\mathbf{st}) : Q_{done} / \mathcal{A}(\mathbf{st}) \cong (\text{Reach } \mathcal{A})(\mathbf{st})$ is an isomorphism at the end of the algorithm, and it is easy to check that it forms a morphism of automata between the automaton produced by the algorithm and Reach $\mathcal{A}$. $\square$

**Lemma 3.7.** For every $Q, Q' \subseteq A^*$, if the coproduct $Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st})$ exists, $[m_Q, m_{Q'}] : Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st}) \to \mathcal{A}(\mathbf{st})$ ($\mathcal{E}, \mathcal{M}$)-factors into

$$m_{Q \sqcup Q'} \circ [\kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\mathbf{st}), \kappa_{Q'}^{Q' \sqcup Q'} / \mathcal{A}(\mathbf{st})] : Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st}) \to (Q \sqcup Q')/\mathcal{A}(\mathbf{st}) \to \mathcal{A}(\mathbf{st})$$

*Proof.* Factor $[m_Q, m_{Q'}] : Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st}) \to \mathcal{A}(\mathbf{st})$ as $e = [z_Q, z_{Q'}] : Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st}) \to Z$ and $m : Z \to \mathcal{A}(\mathbf{st})$. Since $e_Q + e_{Q'} : \coprod_Q \mathcal{A}(\mathbf{in}) + \coprod_{Q'} \mathcal{A}(\mathbf{in}) \to Q/\mathcal{A}(\mathbf{st}) + Q'/\mathcal{A}(\mathbf{st})$ is an $\mathcal{E}$-morphism (as a coproduct of $\mathcal{E}$-morphisms, by the dual of [8, Proposition 14.15]), $e \circ (e_Q + e_{Q'}) : \coprod_{Q \sqcup Q'} \mathcal{A}(\mathbf{in}) \to Z$ and $m : Z \to \mathcal{A}(\mathbf{st})$ form a factorization of $[m_Q \circ e_Q, m_{Q'} \circ e_{Q'}] = [\mathcal{A}(\triangleright q \triangleleft)]_{q \in Q \sqcup Q'} : \coprod_{Q \sqcup Q'} \mathcal{A}(\mathbf{in}) \to \mathcal{A}(\mathbf{st})$ as in Definition 3.3. By unicity of the diagonal fill-in, there is an isomorphism $x : Z \cong (Q \sqcup Q')/\mathcal{A}(\mathbf{st})$ such that $m = m_{Q \sqcup Q'} \circ x$ and $x \circ e \circ (e_Q + e_{Q'}) = e_{Q \sqcup Q'}$.

In particular, $x \circ z_Q \circ e_Q = e_{Q \sqcup Q'} \circ [\kappa_q]_{q \in Q}$ and $m_{Q \sqcup Q'} \circ x \circ z_Q = m_Q$, hence by unicity of the diagonal fill-in $x \circ z_Q = \kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\mathbf{st})$. The same results holds for $Q'$ hence $[m_Q, m_Q'] = (m \circ x^{-1}) \circ [x \circ z_Q, x \circ z_{Q'}]$ yields the expected factorization. $\square$

**Lemma 3.8.** For every $Q \subseteq A^*$, $\mathcal{A}(a) \circ m_Q$ ($\mathcal{E}, \mathcal{M}$)-factors into $m_{Qa} \circ \kappa_{Q \cdot a}^{Qa} / \mathcal{A}(\mathbf{st}) : Q/\mathcal{A}(\mathbf{st}) \to Qa/\mathcal{A}(\mathbf{st}) \to \mathcal{A}(\mathbf{st})$.

*Proof.* The equality holds by definition of $\kappa_{Q \cdot a}^{Qa} / \mathcal{A}(\mathbf{st})$ in Lemma 3.4. This morphism is an $\mathcal{E}$-morphism because $[\kappa_{qa}]_{q \in Q}$ is an isomorphism hence the dual of [8, Proposition 14.9(1)] applies. $\square$

**Lemma 3.10.** If $\kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\mathbf{st}) : Q/\mathcal{A}(\mathbf{st}) \to (Q \sqcup Q')/\mathcal{A}(\mathbf{st})$ is an isomorphism then

$$m_{Q'} = m_Q \circ (\kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\mathbf{st}))^{-1} \circ (\kappa_{Q'}^{Q' \sqcup Q'} / \mathcal{A}(\mathbf{st}))$$
Conversely, in the context of Lemma 3.7, assume also that all split epimorphisms are in $\mathcal{E}$ (if $e \circ s = \text{id}$ for some $e, s$ then $e \in \mathcal{E}$). If $m_{Q'}$ factors as $m_Q \circ f$ for some $f : Q/\mathcal{A}(\text{st}) \to (Q \sqcup Q')/\mathcal{A}(\text{st})$ then $\kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\text{st})$ is an isomorphism.

*Proof.* We immediately have that

$$ m_{Q'} = m_{Q \sqcup Q'} \circ \kappa_{Q'}^{Q \sqcup Q'} / \mathcal{A}(\text{st}) \\ = m_Q \circ (\kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\text{st}))^{-1} \kappa_{Q'}^{Q \sqcup Q'} / \mathcal{A}(\text{st}) $$

$$ \text{since } m_Q = m_{Q \sqcup Q'} \circ \kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\text{st}). $$

Conversely, assume $m_{Q'} = m_Q \circ f$ for some $f$. Then $[m_Q, m_{Q'}] = m_Q \circ [\text{id}, f]$. But $[\text{id}, f]$ is a split epimorphism $([\text{id}, f] \circ \kappa_1 = \text{id})$ hence it is also an $\mathcal{E}$-morphism. We thus get two $(\mathcal{E}, \mathcal{M})$-factorizations for $[m_Q, m_{Q'}]$:

$$ m_Q \circ [\text{id}, f] = m_{Q \sqcup Q'} \circ \left[ \kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\text{st}) , \kappa_{Q'}^{Q \sqcup Q'} / \mathcal{A}(\text{st}) \right] $$

□

## C. Proofs for Section 4 (The category of monoidal transducers)

**Lemma 4.6.** *M is right-noetherian if and only if for any sequences $(u_n)_{n \in \mathbb{N}}$ and $(v_n)_{n \in \mathbb{N}}$ of M such that $v_n = v_{n+1}u_n$ for all $n \in \mathbb{N}$, there is some $n \in \mathbb{N}$ such that for all $i \ge n$, $u_i$ is invertible.*

*Proof.* The reverse implication is trivial. Now assume M right-noetherian, and consider $(u_n)_{n \in \mathbb{N}}$ and $(v_n)_{n \in \mathbb{N}}$ such that $v_n = v_{n+1}u_n$ for all $n \in \mathbb{N}$. Consider the set $I = \{i_0 < i_1 < \dots\}$ of all the indices $i$ such that $u_i$ is not invertible and, letting $i_{-1} = -1$, define $u'_n = u_{i_n} \cdots u_{i_{n-1}+1}$ and $v'_n = v_{i_n+1}$ for all $n \in \mathbb{N}$. Then $u'_n$ is never invertible because $u_{i_n}$ is not but $u_{i_{n-1}}$, $\dots$, $u_{i_{n-1}+1}$ are (by definition), yet we still have by induction that $v'_n = v'_{n+1}u'_n$. Since M is left-noetherian, $I$ must be finite hence there is some $n \in \mathbb{N}$ such that for all $i \ge n$, $m_i$ is invertible. □

**Lemma 4.7.** *If M is right-noetherian then all its right- and left-invertibles are invertible.*

*Proof.* Assume M right-noetherian and consider some $x$ that is right-invertible with $x_r$ its right-inverse. For $n \in \mathbb{N}$, set $u_{2n} = x_r$, $v_{2n} = \epsilon$ and $u_{2n+1} = v_{2n+1} = x$. Then $v_n = v_{n+1}u_n$ for all $n \in \mathbb{N}$ hence by right-noetherianity $x$ is invertible. If $x$ is left-invertible instead, its left-inverse is right-invertible hence invertible and therefore so is $x$. □

**Proposition 4.12.** *The following are equivalent:*

(1) $\text{KI}(\mathcal{T}_M)$ has all countable powers of 1;
Conversely, in the context of Lemma 3.7, assume also that all split epimorphisms are in $\mathcal{E}$ (if $e \circ s = \text{id}$ for some $e, s$ then $e \in \mathcal{E}$). If $m_{Q'}$ factors as $m_Q \circ f$ for some $f : Q/\mathcal{A}(\text{st}) \to (Q \sqcup Q')/\mathcal{A}(\text{st})$ then $\kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\text{st})$ is an isomorphism.

*Proof.* We immediately have that

$$ m_{Q'} = m_{Q \sqcup Q'} \circ \kappa_{Q'}^{Q \sqcup Q'} / \mathcal{A}(\text{st}) \\ = m_Q \circ (\kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\text{st}))^{-1} \kappa_{Q'}^{Q \sqcup Q'} / \mathcal{A}(\text{st}) $$

$$ \text{since } m_Q = m_{Q \sqcup Q'} \circ \kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\text{st}). $$

Conversely, assume $m_{Q'} = m_Q \circ f$ for some $f$. Then $[m_Q, m_{Q'}] = m_Q \circ [\text{id}, f]$. But $[\text{id}, f]$ is a split epimorphism $([\text{id}, f] \circ \kappa_1 = \text{id})$ hence it is also an $\mathcal{E}$-morphism. We thus get two $(\mathcal{E}, \mathcal{M})$-factorizations for $[m_Q, m_{Q'}]$:

$$ m_Q \circ [\text{id}, f] = m_{Q \sqcup Q'} \circ \left[ \kappa_Q^{Q \sqcup Q'} / \mathcal{A}(\text{st}), \kappa_{Q'}^{Q \sqcup Q'} / \mathcal{A}(\text{st}) \right] $$

□

## C. Proofs for Section 4 (The category of monoidal transducers)

**Lemma 4.6.** *M is right-noetherian if and only if for any sequences $(u_n)_{n \in \mathbb{N}}$ and $(v_n)_{n \in \mathbb{N}}$ of M such that $v_n = v_{n+1}u_n$ for all $n \in \mathbb{N}$, there is some $n \in \mathbb{N}$ such that for all $i \ge n$, $u_i$ is invertible.*

*Proof.* The reverse implication is trivial. Now assume M right-noetherian, and consider $(u_n)_{n \in \mathbb{N}}$ and $(v_n)_{n \in \mathbb{N}}$ such that $v_n = v_{n+1}u_n$ for all $n \in \mathbb{N}$. Consider the set $I = \{i_0 < i_1 < \dots\}$ of all the indices $i$ such that $u_i$ is not invertible and, letting $i_{-1} = -1$, define $u'_n = u_{i_n} \cdots u_{i_{n-1}+1}$ and $v'_n = v_{i_n+1}$ for all $n \in \mathbb{N}$. Then $u'_n$ is never invertible because $u_{i_n}$ is not but $u_{i_{n-1}}$, $\dots$, $u_{i_{n-1}+1}$ are (by definition), yet we still have by induction that $v'_n = v'_{n+1}u'_n$. Since M is left-noetherian, $I$ must be finite hence there is some $n \in \mathbb{N}$ such that for all $i \ge n$, $m_i$ is invertible. □

**Lemma 4.7.** *If M is right-noetherian then all its right- and left-invertibles are invertible.*

*Proof.* Assume M right-noetherian and consider some $x$ that is right-invertible with $x_r$ its right-inverse. For $n \in \mathbb{N}$, set $u_{2n} = x_r$, $v_{2n} = \epsilon$ and $u_{2n+1} = v_{2n+1} = x$. Then $v_n = v_{n+1}u_n$ for all $n \in \mathbb{N}$ hence by right-noetherianity $x$ is invertible. If $x$ is left-invertible instead, its left-inverse is right-invertible hence invertible and therefore so is $x$. □

**Proposition 4.12.** *The following are equivalent:*

(1) $\text{KI}(\mathcal{T}_M)$ has all countable powers of 1;
(2) there are two functions $\text{lgcd} : (M+1)_*^N \to M$ and $\text{red} : (M+1)_*^N \to (M+1)_*^N$ such that

a) for all $\Lambda \in (M+1)_*^N$, $\Lambda = \text{lgcd}(\Lambda) \text{red}(\Lambda)$;

b) for all $\Gamma, \Lambda \in (M+1)_*^N$ and $v, v \in M$, if $v \text{red}(\Gamma) = v \text{red}(\Lambda)$ then $v = v$ and $\text{red} \Gamma = \text{red} \Lambda$;

(3) $\text{KI}(\mathcal{T}_M)$ has all countable products.

Moreover when these hold, since any countable set $I$ embeds into $\mathbb{N}$, $\text{lgcd}$ and $\text{red}$ can be extended to $(M+1)_*^I$. $\text{lgcd}$ $\Lambda$ is then a left-gcd of $(\Lambda(i))_{i|\Lambda(i) \neq \perp}$ and the product of $(X_i)_{i \in I}$ for some $I \subseteq \mathbb{N}$ is the set of pairs $(\Lambda, (x_i)_{i \in I})$ such that $\Lambda \in \text{red}((M+1)_*^I)$ and, for all $i \in I$, $x_i \in X_i$ if $\Lambda(i) \neq \perp$ and $x_i = \perp$ otherwise. In particular, the $I$-th power of $1$ is the set of irreducible partial functions $I \to M+1$:

$$ \prod_I 1 = \text{Irr}(I, M) = \{\text{red } \Lambda \in (M+1)_*^I \mid \Lambda \in (M+1)_*^I\} $$

*Proof.* (3) ⇒ (1) holds by definition.

Let us now show (1) ⇒ (2). If $\Pi_{\mathbb{N}}1$ exists, then for any $\Lambda \in (M+1)_*^N$ the cone $(\Lambda(n) : 1 \to M+1)_{n \in \mathbb{N}}$ factors through some $h : 1 \to \Pi_{\mathbb{N}}$ given by some $h(*) = (\delta, x_{\Lambda})$, as if $h(*) = \perp$ then $\Lambda = \perp^N$. We thus set $\text{lgcd} \Lambda = \delta$ and $\text{red}(\Lambda)(n) = \pi_n(x_{\Lambda})$ for all $n \in \mathbb{N}$, so that in particular $\text{red}(\Lambda) \neq \perp^N$. Since $\Lambda(n) = \pi_n \circ h$ for all $n \in \mathbb{N}$ we get that $\Lambda = \text{lgcd}(\Lambda) \text{red}(\Lambda)$, and if $\Xi = v \text{red}(\Gamma) = v \text{red}(\Lambda)$, then $(*) \mapsto \Xi(n))_{n \in \mathbb{N}}$ factors through both $g(*) = (v, x_{\Gamma})$ and $h(*) = (v, x_{\Lambda}) : g = h$ hence $u = v$ and $\text{red} \Gamma = \text{red} \Lambda$. $\text{lgcd}$ and $\text{red}$ thus satisfy conditions (2)a and (2)b.

In particular when these conditions are satisfied $\text{lgcd}(\Lambda) \text{red}(\Lambda) = \Lambda$ hence $\text{lgcd} \Lambda$ left-divides $(\Lambda(i))_{i|\Lambda(i) \neq \perp}$ and if $\delta$ left-divides this family then $\Lambda = \delta \Gamma$ for some $\Gamma \neq \perp^N$ hence $\Lambda = (\delta \text{lgcd}(\Gamma)) \text{red}(\Gamma)$ and thus $\delta$ left-divides $\text{lgcd}(\Lambda) = \delta \text{lgcd}(\Gamma)$.

Finally, let us show (2) ⇒ (3) along with the formula for the product of a countable number of objects. Given $(X_i)_{i \in I}$ indexed by some $I \subseteq \mathbb{N}$, define $\prod_I X_i$ as in the statement of the proposition and the projection $\pi_j : \prod_I X_i \to X_j$ by $\pi_j(\Lambda, (x_i)_{i \in I}) = (\Lambda(j), x_j)$ if $\Lambda(j) \neq \perp$ and $\pi_j(\Lambda, (x_i)_{i \in I}) = \perp$ otherwise. Given a cone $(f_i : 1 \to X_i)$ and some $i \in I$, write $f_i(*) = (\Lambda(i), x_i)$ when $f_i \neq \perp$ and $\Lambda(i) = x_i = \perp$ otherwise. Define now $h : 1 \to \prod_I X_i$ by $h(*) = (\text{lgcd} \Lambda, (\text{red} \Lambda, (x_i)_{i \in I}))$ if $\Lambda \neq \perp^N$ and $h(*) = \perp$ otherwise. We immediately have that $f_i = \pi_i \circ h$ by condition (2)a, and that $h$ is the only such function by condition (2)b. $\square$

**Lemma 4.13.** *Conditions (2)a and (2)b are equivalent to saying that*

(4) a) $\langle \text{lgcd}, \text{red} \rangle$ is injective;

b) for all $\Lambda \in (M+1)_*^N$, $\text{lgcd}(\text{red} \Lambda) = \epsilon$ and $\text{red}(\text{red} \Lambda) = \text{red} \Lambda$;

c) for all $\Lambda \in (M+1)_*^N$ and $v \in M$, $\text{lgcd}(v\Lambda) = v \text{lgcd}(\Lambda)$ and $\text{red}(v\Lambda) = \text{red}(\Lambda)$.

*Proof.* Assuming conditions (2)a and (2)b, we get that
(2) there are two functions $\text{lgcd} : (M+1)_*^N \to M$ and $\text{red} : (M+1)_*^N \to (M+1)_*^N$ such that

a) for all $\Lambda \in (M+1)_*^N$, $\Lambda = \text{lgcd}(\Lambda) \text{red}(\Lambda)$;

b) for all $\Gamma, \Lambda \in (M+1)_*^N$ and $v, \nu \in M$, if $v \text{red}(\Gamma) = \nu \text{red}(\Lambda)$ then $v = \nu$ and $\text{red} \Gamma = \text{red} \Lambda$;

(3) $\text{KI}(\mathcal{T}_M)$ has all countable products.

Moreover when these hold, since any countable set $I$ embeds into $\mathbb{N}$, $\text{lgcd}$ and $\text{red}$ can be extended to $(M+1)_*^I$. $\text{lgcd}$ $\Lambda$ is then a left-gcd of $(\Lambda(i))_{i|\Lambda(i) \neq \perp}$ and the product of $(X_i)_{i \in I}$ for some $I \subseteq \mathbb{N}$ is the set of pairs $(\Lambda, (x_i)_{i \in I})$ such that $\Lambda \in \text{red}((M+1)_*^I)$ and, for all $i \in I$, $x_i \in X_i$ if $\Lambda(i) \neq \perp$ and $x_i = \perp$ otherwise. In particular, the $I$-th power of $1$ is the set of irreducible partial functions $I \to M+1$:

$$ \prod_I 1 = \text{Irr}(I, M) = \{\text{red } \Lambda \in (M+1)_*^I \mid \Lambda \in (M+1)_*^I\} $$

*Proof.* (3) ⇒ (1) holds by definition.

Let us now show (1) ⇒ (2). If $\Pi_{\mathbb{N}}1$ exists, then for any $\Lambda \in (M+1)_*^N$ the cone $(\Lambda(n) : 1 \to M+1)_{n \in \mathbb{N}}$ factors through some $h : 1 \to \Pi_{\mathbb{N}}$ given by some $h(*) = (\delta, x_\Lambda)$, as if $h(*) = \perp$ then $\Lambda = \perp^N$. We thus set $\text{lgcd} \Lambda = \delta$ and $\text{red}(\Lambda)(n) = \pi_n(x_\Lambda)$ for all $n \in \mathbb{N}$, so that in particular $\text{red}(\Lambda) \neq \perp^N$. Since $\Lambda(n) = \pi_n \circ h$ for all $n \in \mathbb{N}$ we get that $\Lambda = \text{lgcd}(\Lambda) \text{red}(\Lambda)$, and if $\Xi = v \text{red}(\Gamma) = \nu \text{red}(\Lambda)$, then $(*) \mapsto \Xi(n))_{n \in \mathbb{N}}$ factors through both $g(*) = (v, x_\Gamma)$ and $h(*) = (v, x_\Lambda) : g = h$ hence $u = v$ and $\text{red} \Gamma = \text{red} \Lambda$. $\text{lgcd}$ and $\text{red}$ thus satisfy conditions (2)a and (2)b.

In particular when these conditions are satisfied $\text{lgcd}(\Lambda) \text{red}(\Lambda) = \Lambda$ hence $\text{lgcd} \Lambda$ left-divides $(\Lambda(i))_{i|\Lambda(i) \neq \perp}$ and if $\delta$ left-divides this family then $\Lambda = \delta\Gamma$ for some $\Gamma \neq \perp^N$ hence $\Lambda = (\delta \text{lgcd}(\Gamma)) \text{red}(\Gamma)$ and thus $\delta$ left-divides $\text{lgcd}(\Lambda) = \delta \text{lgcd}(\Gamma)$.

Finally, let us show (2) ⇒ (3) along with the formula for the product of a countable number of objects. Given $(X_i)_{i \in I}$ indexed by some $I \subseteq \mathbb{N}$, define $\prod_I X_i$ as in the statement of the proposition and the projection $\pi_j : \prod_I X_i \twoheadrightarrow X_j$ by $\pi_j(\Lambda, (x_i)_{i \in I}) = (\Lambda(j), x_j)$ if $\Lambda(j) \neq \perp$ and $\pi_j(\Lambda, (x_i)_{i \in I}) = \perp$ otherwise. Given a cone $(f_i : 1 \to X_i)$ and some $i \in I$, write $f_i(*) = (\Lambda(i), x_i)$ when $f_i \neq \perp$ and $\Lambda(i) = x_i = \perp$ otherwise. Define now $h : 1 \to \prod_I X_i$ by $h(*) = (\text{lgcd} \Lambda, (\text{red} \Lambda, (x_i)_{i \in I}))$ if $\Lambda \neq \perp^N$ and $h(*) = \perp$ otherwise. We immediately have that $f_i = \pi_i \circ h$ by condition (2)a, and that $h$ is the only such function by condition (2)b. $\square$

**Lemma 4.13.** *Conditions (2)a and (2)b are equivalent to saying that*

(4) a) $\langle \text{lgcd}, \text{red} \rangle$ is injective;

b) for all $\Lambda \in (M+1)_*^N$, $\text{lgcd}(\text{red} \Lambda) = \epsilon$ and $\text{red}(\text{red} \Lambda) = \text{red} \Lambda$;

c) for all $\Lambda \in (M+1)_*^N$ and $v \in M$, $\text{lgcd}(v\Lambda) = v \text{lgcd}(\Lambda)$ and $\text{red}(v\Lambda) = \text{red}(\Lambda)$.

*Proof.* Assuming conditions (2)a and (2)b, we get that
• (4)a: if $\text{lgcd } \Gamma = \text{lgcd } \Lambda$ and $\text{red } \Gamma = \text{red } \Lambda$ then

$$ 
\begin{aligned}
\Gamma &= \text{lgcd}(\Gamma) \text{red}(\Gamma) \\
&= \text{lgcd}(\Lambda) \text{red}(\Lambda) \\
&= \Lambda
\end{aligned}
 $$

• (4)b: $\text{red } \Lambda = \text{lgcd}(\text{red } \Lambda) \text{red}(\text{red } \Lambda)$ hence $\text{lgcd}(\text{red } \Lambda) = \epsilon$ and $\text{red}(\text{red } \Lambda) = \text{red } \Lambda$;

• (4)c: $(\nu \text{lgcd}(\Lambda)) \text{red}(\Lambda) = \nu \Lambda$ hence $\nu \text{lgcd}(\Lambda) = \text{lgcd}(\nu \Lambda)$ and $\text{red}(\nu \Lambda) = \text{red } \Lambda$.

And conversely, assuming conditions (4)a, (4)b and (4)c, we get that

• (2)a: by injectivity, $\Lambda = \text{lgcd}(\Lambda) \text{red}(\Lambda)$ since

$$ 
\begin{aligned}
\text{lgcd}(\text{lgcd}(\Lambda) \text{red}(\Lambda)) &= \text{lgcd}(\Lambda) \text{lgcd}(\text{red } \Lambda) & \text{red}(\text{lgcd}(\Lambda) \text{red}(\Lambda)) &= \text{red}(\text{red } \Lambda) \\
&= \text{lgcd } \Lambda & &= \text{red } \Lambda
\end{aligned}
 $$

• (2)b: if $\nu \text{red}(\Gamma) = \nu \text{red}(\Lambda)$ then

$$ 
\begin{aligned}
\nu &= \nu \text{lgcd}(\text{red } \Gamma) & \text{red } \Gamma &= \text{red}(\text{red } \Gamma) \\
&= \text{lgcd}(\nu \text{red}(\Gamma)) & &= \text{red}(\nu \text{red}(\Gamma)) \\
&= \text{lgcd}(\nu \text{red}(\Lambda)) & &= \text{red}(\nu \text{red}(\Lambda)) \\
&= \nu \text{lgcd}(\text{red } \Lambda) & &= \text{red}(\text{red } \Lambda) \\
&= \nu & &= \text{red } \Lambda
\end{aligned}
 $$

□

**Lemma 4.15.** If right- and left-invertibles of $M$ are all invertibles and if $\text{KI}(\mathcal{T}_M)$ has all countable powers of 1 then $M$ is both left-cancellative up to invertibles on the left and right-coprime-cancellative, and all non-empty countable families of $M$ have a unique left-gcd up to invertibles on the right.

*Proof.* Let us first show left-cancellativity up to invertibles. If $\nu \gamma_i = \nu \lambda_i$ for some $\nu \in M$ and two countable families $(\gamma_i)_{i \in I}$, $(\lambda_i)_{i \in I}$ of elements of $M$ with $I \subseteq \mathbb{N}_{>0}$, then defining $\Gamma(0) = \Lambda(0) = \epsilon$, $\Gamma(i) = \gamma_i$ and $\Lambda(i) = \lambda_i$ for all $i \in I$ and $\Gamma(j) = \Lambda(j) = \perp$ for all $j \notin I$, we have that $\nu \Gamma = \nu \Lambda$. Hence $\text{red } \Gamma = \text{red } \Lambda$ and $\nu \text{lgcd}(\Gamma) = \nu \text{lgcd}(\Lambda)$. But $\text{lgcd } \Gamma$ and $\text{lgcd } \Lambda$ left-divide $\epsilon = \Gamma(0) = \Lambda(0)$ hence they are right-invertible and thus invertible: $\gamma_i$ and $\lambda_i = \text{lgcd}(\Lambda)\text{lgcd}(\Gamma)^{-1}\gamma_i$ are equal up to an invertible (that does not depend on $i$) on the left.

Moreover, if $\nu \Lambda = \nu \Lambda$ for some $\Lambda$ such that $(\Lambda(i))_{i \mid \Lambda(i) \neq \perp}$ is left-coprime, then $\text{lgcd } \Lambda$ is right-invertible (by definition of left-coprimesity) and thus since

$$ 
\begin{aligned}
\nu \text{lgcd}(\Lambda) &= \text{lgcd}(\nu \Lambda) \\
&= \text{lgcd}(\nu \Lambda) \\
&= \nu \text{lgcd}(\Lambda)
\end{aligned}
 $$
• (4)a: if $\text{lgcd } \Gamma = \text{lgcd } \Lambda$ and $\text{red } \Gamma = \text{red } \Lambda$ then

$$ \begin{aligned} \Gamma &= \text{lgcd}(\Gamma) \text{red}(\Gamma) \\ &= \text{lgcd}(\Lambda) \text{red}(\Lambda) \\ &= \Lambda \end{aligned} $$

• (4)b: $\text{red } \Lambda = \text{lgcd}(\text{red } \Lambda) \text{red}(\text{red } \Lambda)$ hence $\text{lgcd}(\text{red } \Lambda) = \epsilon$ and $\text{red}(\text{red } \Lambda) = \text{red } \Lambda$;

• (4)c: $(v \text{lgcd}(\Lambda)) \text{red}(\Lambda) = v \Lambda$ hence $v \text{lgcd}(\Lambda) = \text{lgcd}(v \Lambda)$ and $\text{red}(u \Lambda) = \text{red } \Lambda$.

And conversely, assuming conditions (4)a, (4)b and (4)c, we get that

• (2)a: by injectivity, $\Lambda = \text{lgcd}(\Lambda) \text{red}(\Lambda)$ since

$$ \begin{aligned} \text{lgcd}(\text{lgcd}(\Lambda) \text{red}(\Lambda)) &= \text{lgcd}(\Lambda) \text{lgcd}(\text{red } \Lambda) & \text{red}(\text{lgcd}(\Lambda) \text{red}(\Lambda)) &= \text{red}(\text{red } \Lambda) \\ &= \text{lgcd } \Lambda & &= \text{red } \Lambda \end{aligned} $$

• (2)b: if $v \text{red}(\Gamma) = v \text{red}(\Lambda)$ then

$$ \begin{aligned} v &= v \text{lgcd}(\text{red } \Gamma) & \text{red } \Gamma &= \text{red}(\text{red } \Gamma) \\ &= \text{lgcd}(v \text{red}(\Gamma)) & &= \text{red}(v \text{red}(\Gamma)) \\ &= \text{lgcd}(v \text{red}(\Lambda)) & &= \text{red}(v \text{red}(\Lambda)) \\ &= v \text{lgcd}(\text{red } \Lambda) & &= \text{red}(\text{red } \Lambda) \\ &= v & &= \text{red } \Lambda \end{aligned} $$

□

**Lemma 4.15.** If right- and left-invertibles of $M$ are all invertibles and if $\text{KI}(\mathcal{T}_M)$ has all countable powers of 1 then $M$ is both left-cancellative up to invertibles on the left and right-coprime-cancellative, and all non-empty countable families of $M$ have a unique left-gcd up to invertibles on the right.

*Proof.* Let us first show left-cancellativity up to invertibles. If $v\gamma_i = v\lambda_i$ for some $v \in M$ and two countable families $(\gamma_i)_{i \in I}$, $(\lambda_i)_{i \in I}$ of elements of $M$ with $I \subseteq \mathbb{N}_{>0}$, then defining $\Gamma(0) = \Lambda(0) = \epsilon$, $\Gamma(i) = \gamma_i$ and $\Lambda(i) = \lambda_i$ for all $i \in I$ and $\Gamma(j) = \Lambda(j) = \perp$ for all $j \notin I$, we have that $v\Gamma = v\Lambda$. Hence $\text{red } \Gamma = \text{red } \Lambda$ and $v \text{lgcd}(\Gamma) = v \text{lgcd}(\Lambda)$. But $\text{lgcd } \Gamma$ and $\text{lgcd } \Lambda$ left-divide $\epsilon = \Gamma(0) = \Lambda(0)$ hence they are right-invertible and thus invertible: $\gamma_i$ and $\lambda_i = \text{lgcd}(\Lambda)\text{lgcd}(\Gamma)^{-1}\gamma_i$ are equal up to an invertible (that does not depend on $i$) on the left.

Moreover, if $v\Lambda = v\Lambda$ for some $\Lambda$ such that $(\Lambda(i))_{i \mid \Lambda(i) \neq \perp}$ is left-coprime, then $\text{lgcd } \Lambda$ is right-invertible (by definition of left-coprimality) and thus since

$$ \begin{aligned} v \text{lgcd}(\Lambda) &= \text{lgcd}(v\Lambda) \\ &= \text{lgcd}(v\Lambda) \\ &= v \text{lgcd}(\Lambda) \end{aligned} $$
by left-invertibility of $\text{lgcd} \Lambda$, $v = v$.

Finally, consider $\delta$ a left-gcd of some non-empty countable family encoded as $\Lambda \in (M+1)_*^N$. Then there is some $v$ such that $\delta = \text{lgcd}(\Lambda)v$ (since $\text{lgcd}(\Lambda)$ left-divides $\Lambda$) and some $\Gamma$ such that $\delta\Gamma = \Lambda$. Hence

$$ \begin{aligned} \text{lgcd} \Lambda &= \text{lgcd}(\delta\Gamma) \\ &= \delta \text{lgcd}(\Gamma) \\ &= \text{lgcd}(\Lambda)v \text{lgcd}(\Gamma) \end{aligned} $$

By left-cancellativity up to invertibles, $v \text{lgcd}(\Gamma) \in M^\times$ so $v$ is right-invertible hence invertible : $\delta = \text{lgcd} \Lambda$ up to invertibles on the right. $\square$

**Lemma 4.16.** If $M$ is both left-cancellative up to invertibles on the left and right-coprime-cancellative, and all non-empty countable subsets of $M$ have a unique left-gcd up to invertibles on the right, then $\text{KI}(\mathcal{T}_M)$ has all countable powers of 1.

*Proof.* Split the set of those $\Lambda \in (M+1)_*^N$ such that $(\Lambda(i))_{i|\Lambda(i)\neq\perp}$ is left-coprime into the equivalence classes given by $\chi\Lambda \sim \Lambda$ for all $\chi \in M^\times$. Then, for each equivalence class $C$ pick a red $C$ in $C$ (using the axiom of choice) and for all $v \in M$ define $\text{lgcd}(v \text{red}(C)) = v$ and $\text{red}(v \text{red}(C)) = \text{red} C$ so that in particular $\text{lgcd}(\text{red} C) = \epsilon$ and $\text{red}(\text{red} C) = \text{red} C$.

This is well-defined because if $v \text{red}(C) = \nu \text{red}(D)$ for $v, \nu \in M$ and two equivalence classes $C, D$, then if $\delta$ is a left-gcd of $v \text{red}(C)$ we have that $\delta = vv'$ for some $v'$ (since $v$ left-divides $v \text{red}(C)$) and there is some $\Lambda$ such that $v \text{red}(C) = vv'\Lambda$. But then by left-cancellativity up to invertibles, there is some $\chi \in M^\times$ such that $v'\Lambda = \chi \text{red}(C)$, hence $\chi^{-1}v'$ left-divides red $C$ and as such is right-invertible (it left-divides $\epsilon$, a left-gcd of red $C$), making $v'$ right-invertible as well. This shows that $v$ is a left-gcd of $v \text{red}(C) = \nu \text{red}(D)$ and we show similarly that this is also true of $\nu$, hence by unicity of the left-gcd there is a $\xi \in M^\times$ such that $v = \nu\xi$. Therefore by left-cancellativity up to invertibles there is another invertible $\xi' \in M^\times$ such that $\xi \text{red}(C) = \xi' \text{red}(D)$ hence by definition $C = D$ and, by right-coprime-cancellativity, $v = \nu$.

Moreover this defines $\text{lgcd} \Lambda$ and $\text{red} \Lambda$ for any $\Lambda$ because if $\delta$ is a left-gcd of $\Lambda$, then $\Lambda = \delta\Gamma$ for some left-coprime $\Gamma$ (if $\delta'$ left-divides $\Gamma$ then $\delta\delta'$ left-divides $\Lambda$ hence $\delta$, therefore $\delta'$ is invertible by left-cancellativity up to invertibles) hence $\Lambda = \delta\chi \text{red}(C)$ if $\Gamma \in C$ and $\Gamma = \chi \text{red}(C)$.

We have thus defined two functions $\text{lgcd}$ and $\text{red}$ that immediately satisfy the conditions (2)a and (2)b of Proposition 4.12. $\square$

**Lemma 4.18.** In $\text{KI}(\mathcal{T}_M)$, $\text{Iso} = \text{Surj} \cap \text{Inj} \cap \text{Inv} \cap \text{Tot}$, and these four classes are all closed under composition (within themselves).

*Proof.* Closure under composition is immediate.

If $f: X \to M \times Y + 1$ is in $\text{Surj} \cap \text{Inj} \cap \text{Inv} \cap \text{Tot}$, it can be restricted to a function $\langle f_1, f_2 \rangle: X \to M \times Y$ ($f \in \text{Tot}$). $f_2$ must be bijective ($f \in \text{Surj} \cap \text{Inj}$) and $f_1(X) \subseteq M^\times$ ($f \in \text{Inv}$). Hence $f$ has an inverse, given by $(f^{-1})(y) = ((f_1(f_2^{-1}(y)))^{-1}, f_2^{-1}(y))$.
by left-invertibility of $\text{lgcd} \Lambda$, $v = v$.

Finally, consider $\delta$ a left-gcd of some non-empty countable family encoded as $\Lambda \in (M+1)_*^N$. Then there is some $v$ such that $\delta = \text{lgcd}(\Lambda)v$ (since $\text{lgcd}(\Lambda)$ left-divides $\Lambda$) and some $\Gamma$ such that $\delta\Gamma = \Lambda$. Hence

$$ \begin{aligned} \text{lgcd} \Lambda &= \text{lgcd}(\delta\Gamma) \\ &= \delta \text{lgcd}(\Gamma) \\ &= \text{lgcd}(\Lambda)v \text{lgcd}(\Gamma) \end{aligned} $$

By left-cancellativity up to invertibles, $v \text{lgcd}(\Gamma) \in M^\times$ so $v$ is right-invertible hence invertible : $\delta = \text{lgcd} \Lambda$ up to invertibles on the right. $\square$

**Lemma 4.16.** If $M$ is both left-cancellative up to invertibles on the left and right-coprime-cancellative, and all non-empty countable subsets of $M$ have a unique left-gcd up to invertibles on the right, then $\text{KI}(\mathcal{T}_M)$ has all countable powers of 1.

*Proof.* Split the set of those $\Lambda \in (M+1)_*^N$ such that $(\Lambda(i))_{i|\Lambda(i) \neq \emptyset}$ is left-coprime into the equivalence classes given by $\chi\Lambda \sim \Lambda$ for all $\chi \in M^\times$. Then, for each equivalence class $C$ pick a red $C$ in $C$ (using the axiom of choice) and for all $v \in M$ define $\text{lgcd}(v \text{red}(C)) = v$ and $\text{red}(v \text{red}(C)) = \text{red} C$ so that in particular $\text{lgcd}(\text{red} C) = \epsilon$ and $\text{red}(\text{red} C) = \text{red} C$.

This is well-defined because if $v \text{red}(C) = \nu \text{red}(D)$ for $v, \nu \in M$ and two equivalence classes $C, D$, then if $\delta$ is a left-gcd of $v \text{red}(C)$ we have that $\delta = vv'$ for some $v'$ (since $v$ left-divides $v \text{red}(C)$) and there is some $\Lambda$ such that $v \text{red}(C) = vv'\Lambda$. But then by left-cancellativity up to invertibles, there is some $\chi \in M^\times$ such that $v'\Lambda = \chi \text{red}(C)$, hence $\chi^{-1}v'$ left-divides red $C$ and as such is right-invertible (it left-divides $\epsilon$, a left-gcd of red $C$), making $v'$ right-invertible as well. This shows that $v$ is a left-gcd of $v \text{red}(C) = \nu \text{red}(D)$ and we show similarly that this is also true of $\nu$, hence by unicity of the left-gcd there is a $\xi \in M^\times$ such that $v = \nu\xi$. Therefore by left-cancellativity up to invertibles there is another invertible $\xi' \in M^\times$ such that $\xi \text{red}(C) = \xi' \text{red}(D)$ hence by definition $C = D$ and, by right-coprime-cancellativity, $v = \nu$.

Moreover this defines $\text{lgcd} \Lambda$ and $\text{red} \Lambda$ for any $\Lambda$ because if $\delta$ is a left-gcd of $\Lambda$, then $\Lambda = \delta\Gamma$ for some left-coprime $\Gamma$ (if $\delta'$ left-divides $\Gamma$ then $\delta\delta'$ left-divides $\Lambda$ hence $\delta$, therefore $\delta'$ is invertible by left-cancellativity up to invertibles) hence $\Lambda = \delta\chi \text{red}(C)$ if $\Gamma \in C$ and $\Gamma = \chi \text{red}(C)$.

We have thus defined two functions $\text{lgcd}$ and $\text{red}$ that immediately satisfy the conditions (2)a and (2)b of Proposition 4.12. $\square$

**Lemma 4.18.** In $\text{KI}(\mathcal{T}_M)$, $\text{Iso} = \text{Surj} \cap \text{Inj} \cap \text{Inv} \cap \text{Tot}$, and these four classes are all closed under composition (within themselves).

*Proof.* Closure under composition is immediate.

If $f: X \to M \times Y + 1$ is in $\text{Surj} \cap \text{Inj} \cap \text{Inv} \cap \text{Tot}$, it can be restricted to a function $\langle f_1, f_2 \rangle: X \to M \times Y$ ($f \in \text{Tot}$). $f_2$ must be bijective ($f \in \text{Surj} \cap \text{Inj}$) and $f_1(X) \subseteq M^\times$ ($f \in \text{Inv}$). Hence $f$ has an inverse, given by $(f^{-1})(y) = ((f_1(f_2^{-1}(y)))^{-1}, f_2^{-1}(y))$.
Conversely, if $f: X \to M \times Y + 1$ is an isomorphism it has an inverse $f^{-1}: Y \to M \times X + 1$ such that $f \circ f^{-1} = \text{id}_Y$ and $f^{-1} \circ f = \text{id}_X$. For all $x \in X$, $(f^{-1})^{\dagger}(f(x)) = (\epsilon, x)$ hence $f(x) \neq \perp$: $f \in \text{Tot}$, and similarly for $f^{-1}$. Writing $f = \langle f_1, f_2 \rangle$ and $f^{-1} = \langle (f^{-1})_1, (f^{-1})_2 \rangle$, we have that $f_2$ is a bijection with inverse $f_2^{-1} = (f^{-1})_2$, hence $f \in \text{Surj} \cap \text{Inj}$. Finally, for all $x \in X$ we have that $f_1(x)(f^{-1})_1(f_2(x)) = \epsilon$ and conversely, hence $f_1(x)$ is invertible and $f \in \text{Inv}$. $\square$

**Proposition 4.19.** ($\mathcal{E}_1, \mathcal{M}_1$) = (Surj $\cap$ Inj $\cap$ Inv, Tot), ($\mathcal{E}_2, \mathcal{M}_2$) = (Surj $\cap$ Inj, Inv $\cap$ Tot) and ($\mathcal{E}_3, \mathcal{M}_3$) = (Surj, Inj $\cap$ Inv $\cap$ Tot) are all factorization systems in $\mathbf{Kl}(\mathcal{T}_M)$.

*Proof.* By Lemma 4.18 we only need to show for each $i \in \{1, 2, 3\}$ that every $f: X \to Y$ may be factored as $m \circ e$ with $e \in \mathcal{E}_i$ and $m \in \mathcal{M}_i$, and that $\mathcal{E}_i$ and $\mathcal{M}_i$ satisfy the diagonal fill-in property of Definition 2.6.

* ($\mathcal{E}_1, \mathcal{M}_1$). Any $f: X \to M \times Y + 1$ may be factored through $e: X \to M \times f^{-1}(M \times Y) + 1$ (given by $e(x) = (\epsilon, x)$ if $e(x) \neq \perp$ and $e(x) = \perp$ otherwise) and $m: f^{-1}(M \times Y) \to M \times Y + 1$ (given by $m(x) = e(x)$ when $e(x) \neq \perp$).

Moreover, given a commuting diagram

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

the only possible choice for a $\phi: Y_1 \to M \times Y_2 + 1$ is given by $\phi(y_1) = \perp$ if $v(y_1) = \perp$ and $\phi(y_1) = (v_e^{-1}v_u, y_2)$ if $e(x) = (v_e, y_1)$, $u(x) = (v_u, y_2)$, $v(y_1) = (v_v, z)$, $m(y_2) = (v_m, z)$ and $v_e v_v = v_u v_m$. This definition does not depend on the choice of $x$ because of the bijectiveness property of $e$, and we immediately have the commuting diagram

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

by definition.

* ($\mathcal{E}_2, \mathcal{M}_2$). Any $f: X \to M \times Y + 1$ may be factored through $e: X \to M \times f^{-1}(M \times Y) + 1$ (given by $e(x) = (v, x)$ if $e(x) = (v, -)$ and $e(x) = \perp$ otherwise) and $m: f^{-1}(M \times Y) \to M \times Y + 1$ (given by $m(x) = (\epsilon, y)$ when $e(x) = (-, y)$).

Finally, given a commuting diagram

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

the only possible choice for a $\phi: Y_1 \to M \times Y_2 + 1$ is given by $\phi(y_1) = \perp$ if $v(y_1) = \perp$ and $\phi(y_1) = (v_v v_m^{-1}, y_2)$ if $e(x) = (v_e, y_1)$, $u(x) = (v_u, y_2)$, $v(y_1) =$
Conversely, if $f : X \to M \times Y + 1$ is an isomorphism it has an inverse $f^{-1} : Y \to M \times X + 1$ such that $f \circ f^{-1} = \mathrm{id}_Y$ and $f^{-1} \circ f = \mathrm{id}_X$. For all $x \in X$, $(f^{-1})^{\dagger}(f(x)) = (\epsilon, x)$ hence $f(x) \neq \perp$: $f \in \mathrm{Tot}$, and similarly for $f^{-1}$. Writing $f = \langle f_1, f_2 \rangle$ and $f^{-1} = \langle (f^{-1})_1, (f^{-1})_2 \rangle$, we have that $f_2$ is a bijection with inverse $f_2^{-1} = (f^{-1})_2$, hence $f \in \mathrm{Surj} \cap \mathrm{Inj}$. Finally, for all $x \in X$ we have that $f_1(x)(f^{-1})_1(f_2(x)) = \epsilon$ and conversely, hence $f_1(x)$ is invertible and $f \in \mathrm{Inv}$. $\square$

**Proposition 4.19.** ($\mathcal{E}_1, \mathcal{M}_1$) = (Surj $\cap$ Inj $\cap$ Inv, Tot), ($\mathcal{E}_2, \mathcal{M}_2$) = (Surj $\cap$ Inj, Inv $\cap$ Tot) and ($\mathcal{E}_3, \mathcal{M}_3$) = (Surj, Inj $\cap$ Inv $\cap$ Tot) are all factorization systems in $\mathrm{Kl}(\mathcal{T}_M)$.

*Proof.* By Lemma 4.18 we only need to show for each $i \in \{1, 2, 3\}$ that every $f : X \to Y$ may be factored as $m \circ e$ with $e \in \mathcal{E}_i$ and $m \in \mathcal{M}_i$, and that $\mathcal{E}_i$ and $\mathcal{M}_i$ satisfy the diagonal fill-in property of Definition 2.6.

* ($\mathcal{E}_1, \mathcal{M}_1$). Any $f : X \to M \times Y + 1$ may be factored through $e : X \to M \times f^{-1}(M \times Y) + 1$ (given by $e(x) = (\epsilon, x)$ if $e(x) \neq \perp$ and $e(x) = \perp$ otherwise) and $m : f^{-1}(M \times Y) \to M \times Y + 1$ (given by $m(x) = e(x)$ when $e(x) \neq \perp$).

Moreover, given a commuting diagram

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

the only possible choice for a $\phi : Y_1 \to M \times Y_2 + 1$ is given by $\phi(y_1) = \perp$ if $v(y_1) = \perp$ and $\phi(y_1) = (v_e^{-1}v_u, y_2)$ if $e(x) = (v_e, y_1)$, $u(x) = (v_u, y_2)$, $v(y_1) = (v_v, z)$, $m(y_2) = (v_m, z)$ and $v_e v_v = v_u v_m$. This definition does not depend on the choice of $x$ because of the bijectiveness property of $e$, and we immediately have the commuting diagram

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

by definition.

* ($\mathcal{E}_2, \mathcal{M}_2$). Any $f : X \to M \times Y + 1$ may be factored through $e : X \to M \times f^{-1}(M \times Y) + 1$ (given by $e(x) = (v, x)$ if $e(x) = (v, -)$ and $e(x) = \perp$ otherwise) and $m : f^{-1}(M \times Y) \to M \times Y + 1$ (given by $m(x) = (\epsilon, y)$ when $e(x) = (-, y)$).

Finally, given a commuting diagram

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

the only possible choice for a $\phi : Y_1 \to M \times Y_2 + 1$ is given by $\phi(y_1) = \perp$ if $v(y_1) = \perp$ and $\phi(y_1) = (v_v v_m^{-1}, y_2)$ if $e(x) = (v_e, y_1)$, $u(x) = (v_u, y_2)$, $v(y_1) =$
$(v_v, z), m(y_2) = (v_m, z)$ and $v_e v_v = v_u v_m$. This definition does not depend on the choice of $x$ because of the bijectiveness property of $e$, and we immediately have the commuting diagram

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

by definition.

• $(\mathcal{E}_3, \mathcal{M}_3)$. Any morphism $f: X \to M \times Y + 1$ factors through $e: X \to M \times Z + 1$ and $m: Z \to M \times Y + 1$ with

$$Z = \{y \in Y \mid \exists x \in X, f(x) = (-, y)\}$$

$e(x) = f(x)$ and $m(y) = (\epsilon, y)$.

Finally, given a commuting diagram

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

the only possible choice for a $\phi: Y_1 \to M \times Y_2 + 1$ is given by $\phi(y_1) = \perp$ if $v(y_1) = \perp$ and $\phi(y_1) = (v_v v_m^{-1}, y_2)$ if $e(x) = (v_e, y_1)$, $u(x) = (v_u, y_2)$, $v(y_1) = (v_v, z)$, $m(y_2) = (v_m, z)$ and $v_e v_v = v_u v_m$. This definition does not depend on the choice of $x$ because $m$ is injective on $Y$, and we immediately have the commuting diagram

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

by definition.

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

# D. Proofs for Section 5 (Algorithms on monoidal transducers)

**Lemma 5.1.** An object $X$ of $\mathrm{KI}(\mathcal{T}_M)$ is $\mathcal{M}$-noetherian if and only if it is a finite set, in which case $\mathrm{length}_{\mathcal{M}}(m: Y \to X) = |X| - |Y|$.

*Proof.* Let $(x_i : 1 \to X)_{i \in \mathbb{N}}$ be an infinite sequence of distinct elements of an infinite set $X$. Then the $m_n = [\kappa_i]_{i=0}^n : \coprod_{i=0}^n 1 \to \coprod_{i=0}^{n+1} 1$ provide a counter-example to the $\mathcal{M}$-noetherianity of $X$ as none of them are isomorphisms (they are not surjective) yet $[x_i]_{i=0}^{n+1} \circ m_n = [x_i]_{i=0}^n$ and $[x_i]_{i=0}^n$ is always an $\mathcal{M}$-morphism. Hence infinite sets are never $\mathcal{M}$-noetherian. If $X$ and the sequence $(x_i)_{i \in \mathbb{N}}$ were finite instead, this example would prove that $\mathrm{length}_{\mathcal{M}}(m: Y \to X) \ge |X| - |Y|$.
$(v_v, z)$, $m(y_2) = (v_m, z)$ and $v_e v_v = v_u v_m$. This definition does not depend on the choice of $x$ because of the bijectiveness property of $e$, and we immediately have the commuting diagram

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

by definition.

• $(\mathcal{E}_3, \mathcal{M}_3)$. Any morphism $f: X \to M \times Y + 1$ factors through $e: X \to M \times Z + 1$ and $m: Z \to M \times Y + 1$ with

$$Z = \{y \in Y \mid \exists x \in X, f(x) = (-, y)\}$$

$e(x) = f(x)$ and $m(y) = (\epsilon, y)$.

Finally, given a commuting diagram

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

the only possible choice for a $\phi: Y_1 \to M \times Y_2 + 1$ is given by $\phi(y_1) = \perp$ if $v(y_1) = \perp$ and $\phi(y_1) = (v_v v_m^{-1}, y_2)$ if $e(x) = (v_e, y_1)$, $u(x) = (v_u, y_2)$, $v(y_1) = (v_v, z)$, $m(y_2) = (v_m, z)$ and $v_e v_v = v_u v_m$. This definition does not depend on the choice of $x$ because $m$ is injective on $Y$, and we immediately have the commuting diagram

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

by definition.

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

# D. Proofs for Section 5 (Algorithms on monoidal transducers)

**Lemma 5.1.** An object $X$ of $\mathrm{KI}(\mathcal{T}_M)$ is $\mathcal{M}$-noetherian if and only if it is a finite set, in which case $\mathrm{length}_{\mathcal{M}}(m: Y \to X) = |X| - |Y|$.

*Proof.* Let $(x_i : 1 \to X)_{i \in \mathbb{N}}$ be an infinite sequence of distinct elements of an infinite set $X$. Then the $m_n = [\kappa_i]_{i=0}^n : \coprod_{i=0}^n 1 \to \coprod_{i=0}^{n+1} 1$ provide a counter-example to the $\mathcal{M}$-noetherianity of $X$ as none of them are isomorphisms (they are not surjective) yet $[x_i]_{i=0}^{n+1} \circ m_n = [x_i]_{i=0}^n$ and $[x_i]_{i=0}^n$ is always an $\mathcal{M}$-morphism. Hence infinite sets are never $\mathcal{M}$-noetherian. If $X$ and the sequence $(x_i)_{i \in \mathbb{N}}$ were finite instead, this example would prove that $\mathrm{length}_{\mathcal{M}}(m: Y \to X) \ge |X| - |Y|$.
Conversely, a strict chain of $\mathcal{M}$-subobjects of $X$ is a strict chain of subsets $X_0 \subsetneq X_1 \subsetneq \dots$ of $X$. In particular, the cardinality of these subsets is strictly increasing: if $X$ is finite, the chain must be finite as well, and its length at most $|X| - |X_0|$. $\square$

**Lemma 5.2.** An object $X$ of $\mathbf{KI}(\mathcal{T}_M)$ is $\mathcal{E}$-artinian if and only if it is a finite set and either $M$ is right-noetherian or $X = \emptyset$, in which case colength$_\mathcal{E}(e : X \dashrightarrow Y) = |X| - |Y| + \text{rk } e$ where $\text{rk } e = \sum_{e(x)=(v,y)} \text{rk } v$.

*Proof.* Let $(x_i)_{i \in \mathbb{N}}$ be an infinite sequence of distincts elements of an infinite set $X$, and set $X_n = \{x_i \mid 0 \le i \le n\}$. Let $e_n : X \dashrightarrow X_n$ be defined by $e(x_i) = (\epsilon, x_i)$ for $i \le n$ and $e(x) = \perp$ otherwise, and let $e_n^{n+1} : X_{n+1} \dashrightarrow X_n$ be the restriction of $e_n$ to $X_{n+1}$. None of the $e_n^{n+1}$ are isomorphisms (they are not total) yet $e_n^{n+1} \circ e_{n+1} = e_n$: infinite sets are never $\mathcal{E}$-artinian.

Assume now $X$ is not empty and $M$ is not right-noetherian: there is an element $x_* \in X$ and two sequences $(v_n)_{n \in \mathbb{N}}$ and $(\nu_n)_{n \in \mathbb{N}}$ of elements of $M$ such that for all $n \in \mathbb{N}$, $v_n \notin M^\times$ and $\nu_n = \nu_{n+1}v_n$. Let $e_n : X \dashrightarrow 1$ be defined by $e_n(x_*) = (\nu_n, *)$ and $e_n(x) = \perp$ for all other $x \in X$, and let $e_n^{n+1} : 1 \dashrightarrow 1$ be defined by $e_n^{n+1}(*) = (\nu_n, *)$. None of the $e_n^{n+1}$ are isomorphisms (they do not only produce invertible elements of $M$) yet $e_n^{n+1} \circ e_{n+1} = e_n$: non-empty sets are never $\mathcal{E}$-artinian when $M$ is not right-noetherian.

Conversely, if $X$ is empty then it is immediately $\mathcal{E}$-artinian: there is only one $\mathcal{E}$-morphism out of $X$, $\text{id}_X$. Suppose now that $X$ is finite and $M$ right-noetherian, and consider a cochain $e_n^{n+1} : X_{n+1} \dashrightarrow X_n$ of $\mathcal{E}$-quotients $e_n : X \dashrightarrow X_n$. Since $X$ is finite, at most $|X| - |X_0|$ of the $\mathcal{E}$-quotients $X_{n+1} \dashrightarrow X_n$ witness a decrease of the cardinality from their domain to their codomain and are not in $\text{Inj} \cap \text{Tot}$. Fix now an $x \in X$ such that $e_0(x) \ne \perp$ and write $e_n(x) = (\nu_n, x_n)$ and $e_n^{n+1}(x_{n+1}) = (\nu_n, x_n)$ (this is well-defined because $e_n^{n+1} \circ e_{n+1} = e_n$). Then $\nu_n = \nu_{n+1}\nu_n$ for all $n \in \mathbb{N}$, hence since $M$ is right-noetherian only a finite number of the $e_n^{n+1}$, at most $\text{rk } \nu_0$, produce a non-invertible element on $x_{n+1}$. This is true for all $x \in X$, hence a finite number of the $e_n^{n+1}$, at most $\text{rk } e_0$, are not in $\text{Inv}$, and a finite number of them, at most $|X| - |X_0| + \text{rk } e_0$, are not in $\text{Iso}: X$ is $\mathcal{E}$-artinian and colength$_\mathcal{E}(e_0 : X \dashrightarrow X_0) \le |X| - |X_0| + \text{rk } e_0$.

Finally, if $\text{rk } e$ is finite, in light of this proof it is now easy to build a strict cochain of $\mathcal{E}$-quotients of $X$ starting with $e : X \dashrightarrow Y$ that has length exactly $|X| - |Y| + \text{rk } e$. For each $\nu(x) \in M$ such that $e(x) = (\nu(x), y)$ for some $x \in X$ and $y \in Y$, write indeed $v_1(x), \dots, v_{\text{rk } \nu(x)}(x)$ for a sequence of non-invertible divisors of $\nu$ of maximum length. Each morphism between two consecutive $\mathcal{E}$-quotients in the cochain should either decrease the size of the quotient by 1, or produce exactly one of the $v_i(x)$ on $x$ for exactly one $x \in X$. Similarly, if $\text{rk } e$ is infinite there sequences of divisors of some $\nu(x)$ or arbitrary length and it is then easy to build strict cochains of $\mathcal{E}$-quotients of $X$ of arbitrary lengths. $\square$

**Theorem 5.3.** *Algorithm 4 is correct and terminates as soon as $\text{Min } \mathcal{L}$ has finite state-set and $M$ is right-noetherian. It makes at most 3 $|\text{Min } \mathcal{L}|_{\text{st}} + \text{rk}(\text{Min } \mathcal{L})$ updates to $Q$ (lines 8 and 14) and at most $\text{rk}(\text{Min } \mathcal{L}) + |\text{Min } \mathcal{L}|_{\text{st}}$ updates to $T$ (line 10).*
Conversely, a strict chain of $\mathcal{M}$-subobjects of $X$ is a strict chain of subsets $X_0 \subsetneq X_1 \subsetneq \dots$ of $X$. In particular, the cardinality of these subsets is strictly increasing: if $X$ is finite, the chain must be finite as well, and its length at most $|X| - |X_0|$. $\square$

**Lemma 5.2.** An object $X$ of $\mathbf{KI}(\mathcal{T}_M)$ is $\mathcal{E}$-artinian if and only if it is a finite set and either $M$ is right-noetherian or $X = \emptyset$, in which case colength$_\mathcal{E}(e : X \dashrightarrow Y) = |X| - |Y| + \text{rk } e$ where $\text{rk } e = \sum_{e(x)=(v,y)} \text{rk } v$.

*Proof.* Let $(x_i)_{i \in \mathbb{N}}$ be an infinite sequence of distincts elements of an infinite set $X$, and set $X_n = \{x_i \mid 0 \le i \le n\}$. Let $e_n : X \dashrightarrow X_n$ be defined by $e(x_i) = (\epsilon, x_i)$ for $i \le n$ and $e(x) = \perp$ otherwise, and let $e_n^{n+1} : X_{n+1} \dashrightarrow X_n$ be the restriction of $e_n$ to $X_{n+1}$. None of the $e_n^{n+1}$ are isomorphisms (they are not total) yet $e_n^{n+1} \circ e_{n+1} = e_n$: infinite sets are never $\mathcal{E}$-artinian.

Assume now $X$ is not empty and $M$ is not right-noetherian: there is an element $x_* \in X$ and two sequences $(v_n)_{n \in \mathbb{N}}$ and $(\nu_n)_{n \in \mathbb{N}}$ of elements of $M$ such that for all $n \in \mathbb{N}$, $v_n \notin M^\times$ and $\nu_n = \nu_{n+1}v_n$. Let $e_n : X \dashrightarrow 1$ be defined by $e_n(x_*) = (\nu_n, *)$ and $e_n(x) = \perp$ for all other $x \in X$, and let $e_n^{n+1} : 1 \dashrightarrow 1$ be defined by $e_n^{n+1}(*) = (\nu_n, *)$. None of the $e_n^{n+1}$ are isomorphisms (they do not only produce invertible elements of $M$) yet $e_n^{n+1} \circ e_{n+1} = e_n$: non-empty sets are never $\mathcal{E}$-artinian when $M$ is not right-noetherian.

Conversely, if $X$ is empty then it is immediately $\mathcal{E}$-artinian: there is only one $\mathcal{E}$-morphism out of $X$, $\text{id}_X$. Suppose now that $X$ is finite and $M$ right-noetherian, and consider a cochain $e_n^{n+1} : X_{n+1} \dashrightarrow X_n$ of $\mathcal{E}$-quotients $e_n : X \dashrightarrow X_n$. Since $X$ is finite, at most $|X| - |X_0|$ of the $\mathcal{E}$-quotients $X_{n+1} \dashrightarrow X_n$ witness a decrease of the cardinality from their domain to their codomain and are not in $\text{Inj} \cap \text{Tot}$. Fix now an $x \in X$ such that $e_0(x) \ne \perp$ and write $e_n(x) = (\nu_n, x_n)$ and $e_n^{n+1}(x_{n+1}) = (\nu_n, x_n)$ (this is well-defined because $e_n^{n+1} \circ e_{n+1} = e_n$). Then $\nu_n = \nu_{n+1}\nu_n$ for all $n \in \mathbb{N}$, hence since $M$ is right-noetherian only a finite number of the $e_n^{n+1}$, at most $\text{rk } \nu_0$, produce a non-invertible element on $x_{n+1}$. This is true for all $x \in X$, hence a finite number of the $e_n^{n+1}$, at most $\text{rk } e_0$, are not in $\text{Inv}$, and a finite number of them, at most $|X| - |X_0| + \text{rk } e_0$, are not in $\text{Iso}: X$ is $\mathcal{E}$-artinian and colength$_\mathcal{E}(e_0 : X \dashrightarrow X_0) \le |X| - |X_0| + \text{rk } e_0$.

Finally, if $\text{rk } e$ is finite, in light of this proof it is now easy to build a strict cochain of $\mathcal{E}$-quotients of $X$ starting with $e : X \dashrightarrow Y$ that has length exactly $|X| - |Y| + \text{rk } e$. For each $\nu(x) \in M$ such that $e(x) = (\nu(x), y)$ for some $x \in X$ and $y \in Y$, write indeed $v_1(x), \dots, v_{\text{rk } \nu(x)}(x)$ for a sequence of non-invertible divisors of $\nu$ of maximum length. Each morphism between two consecutive $\mathcal{E}$-quotients in the cochain should either decrease the size of the quotient by 1, or produce exactly one of the $v_i(x)$ on $x$ for exactly one $x \in X$. Similarly, if $\text{rk } e$ is infinite there sequences of divisors of some $\nu(x)$ or arbitrary length and it is then easy to build strict cochains of $\mathcal{E}$-quotients of $X$ of arbitrary lengths. $\square$

**Theorem 5.3.** *Algorithm 4 is correct and terminates as soon as $\text{Min } \mathcal{L}$ has finite state-set and $M$ is right-noetherian. It makes at most 3 $|\text{Min } \mathcal{L}|_{\text{st}} + \text{rk}(\text{Min } \mathcal{L})$ updates to $Q$ (lines 8 and 14) and at most $\text{rk}(\text{Min } \mathcal{L}) + |\text{Min } \mathcal{L}|_{\text{st}}$ updates to $T$ (line 10).*
Proof. Notice first that Algorithm 4 is indeed the instance of Algorithm 1 in $\mathbf{KI}(\mathcal{T}_M)$: for all $q \in Q$ and $a \in A \cup \{\epsilon\}$, $\Lambda(q, a)$ is a left-gcd of $L(q, a, \cdot) = (\mathcal{L}(\triangleright qat\triangle))_{t \in T} = \Lambda(q, a)R(q, a, \cdot)$, hence $R(q, a, \cdot)$ is left-coprime and there is a $\chi \in M^\times$ such that $\Lambda(q, a)\chi^{-1} = \text{lgcd}(L(q, a, \cdot))$ and $\chi R(q, a, \cdot) = \text{red}(L(q, a, \cdot))$. Hence $Q/T = \{\text{red}(L(q, e, \cdot)) \mid q \in Q, L(q, e, \cdot) \neq \perp^T\}$ is the quotient of the set $\{R(q, e, \cdot) \mid q \in Q, R(q, e, \cdot) \neq \perp^T\}$ by equality up to invertibles on the left. It follows that $Q/T \to (Q \cup \{qa\})/T$ is an $\mathcal{E}$-morphism if and only if it is surjective, that is if and only if the condition on line 7 is not satisfied, and $Q/(T \cup \{at\}) \to Q/T$ is an $M$-morphism if and only if it is total, produces only invertibles elements and is injective, that is if and only if it respectively does not satisfy any of the three conditions on line 9: it is easy to see that it is total if and only if the first condition is not satisfied; it is total but does not only produce invertible elements if and only if there is some $q \in Q$ and $at \in AT$ such that $L(q, a, t)$ is not left-divisible by $\Lambda(q, e)$ which is equivalent to the second condition holding; and finally it is easy to see that it is total and only produces invertible elements but is not injective if and only if the third condition holds.

The correction and termination is then given by Theorem 2.16, thanks to Lemmas 5.1 and 5.2. These two lemmas also provide the complexity bound of the algorithm, as Theorem 2.16 is proven in [10] by showing that each addition to $T$ contributes to a morphism in a strict chain of $M$-subobjects of $(\text{Min } \mathcal{L})(\text{st})$ starting with $\{\epsilon\}/A^* \to A^*/A^* = (\text{Min } \mathcal{L})(\text{st})$ [10, Lemma 33], and each addition to $Q$ contributes to a morphism in a chain of $\mathcal{E}$-quotients of $(\text{Min } \mathcal{L})(\text{st})$ ending with $(\text{Min } \mathcal{L})(\text{st}) = A^*/A^* \to A^*/\{\epsilon\}$ [10, Lemma 33] and whose isomorphisms may only be contributed by the addition of a counter-example outputted by $\text{EQUIV}_\mathcal{L}$ and are immediately followed by a non-isomorphism in the chain for $T$ or the cochain for $Q$ [10, Lemma 36]. $\square$
*Proof.* Notice first that Algorithm 4 is indeed the instance of Algorithm 1 in $\mathbf{KI}(\mathcal{T}_M)$: for all $q \in Q$ and $a \in A \cup \{\epsilon\}$, $\Lambda(q, a)$ is a left-gcd of $L(q, a, \cdot) = (\mathcal{L}(\triangleright qat\triangle))_{t \in T} = \Lambda(q, a)R(q, a, \cdot)$, hence $R(q, a, \cdot)$ is left-coprime and there is a $\chi \in M^\times$ such that $\Lambda(q, a)\chi^{-1} = \text{lgcd}(L(q, a, \cdot))$ and $\chi R(q, a, \cdot) = \text{red}(L(q, a, \cdot))$. Hence $Q/T = \{\text{red}(L(q, e, \cdot)) \mid q \in Q, L(q, e, \cdot) \neq \perp^T\}$ is the quotient of the set $\{R(q, e, \cdot) \mid q \in Q, R(q, e, \cdot) \neq \perp^T\}$ by equality up to invertibles on the left. It follows that $Q/T \to (Q \cup \{qa\})/T$ is an $\mathcal{E}$-morphism if and only if it is surjective, that is if and only if the condition on line 7 is not satisfied, and $Q/(T \cup \{at\}) \to Q/T$ is an $M$-morphism if and only if it is total, produces only invertibles elements and is injective, that is if and only if it respectively does not satisfy any of the three conditions on line 9: it is easy to see that it is total if and only if the first condition is not satisfied; it is total but does not only produce invertible elements if and only if there is some $q \in Q$ and $at \in AT$ such that $L(q, a, t)$ is not left-divisible by $\Lambda(q, e)$ which is equivalent to the second condition holding; and finally it is easy to see that it is total and only produces invertible elements but is not injective if and only if the third condition holds.

The correction and termination is then given by Theorem 2.16, thanks to Lemmas 5.1 and 5.2. These two lemmas also provide the complexity bound of the algorithm, as Theorem 2.16 is proven in [10] by showing that each addition to $T$ contributes to a morphism in a strict chain of $M$-subobjects of $(\text{Min } \mathcal{L})(\text{st})$ starting with $\{\epsilon\}/A^* \to A^*/A^* = (\text{Min } \mathcal{L})(\text{st})$ [10, Lemma 33], and each addition to $Q$ contributes to a morphism in a chain of $\mathcal{E}$-quotients of $(\text{Min } \mathcal{L})(\text{st})$ ending with $(\text{Min } \mathcal{L})(\text{st}) = A^*/A^* \to A^*/\{\epsilon\}$ [10, Lemma 33] and whose isomorphisms may only be contributed by the addition of a counter-example outputted by $\text{EQUIV}_\mathcal{L}$ and are immediately followed by a non-isomorphism in the chain for $T$ or the cochain for $Q$ [10, Lemma 36]. $\square$