Pith. sign in

REVIEW 2 major objections 5 minor 5 references

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

T0 review · 2 major / 5 minor · reviewed 2026-08-08 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper claims that for finite and bi-infinite words, any two transducers with the same behavior can be proved equal by rewriting diagrammatic expressions, using a single simulation principle.

desk verdict Real contribution with a patchable gap: finite-word completeness is solid, bi-infinite completeness needs a fixed uniqueness proof. read the letter →

arxiv 2502.06450 v1 pith:UW6RALJP submitted 2025-02-10 cs.LO cs.DMcs.FL

Titouan Carette , Marc de Visme , Vivien Ducros , Victor Lutfalla , Etienne Moutot This is my paper · ORCID
classification cs.LOcs.DMcs.FL MSC 68Q4568Q7018M0537B10
keywords finitetransducersstringdiagramsequationaltheoryregularrelationssoficsubshiftscompletenessrewritingsimulationprinciple
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper proposes finite relational transducers as a common language for automata, labelled transition systems, and symbolic dynamics, and gives them a diagrammatic syntax made of string diagrams read as relations. Its main result is that the associated equational theories are complete: whenever two diagrams denote the same relation, one can be rewritten into the other using the axioms together with one simulation principle. This holds both for finite words, where behaviors are regular relations, and for bi-infinite words, where behaviors are sofic relations. If the result is correct, equivalence proofs in these three settings can be carried out by local diagram rewiring rather than by explicitly comparing automata or subshifts.

What carries the argument

The machinery is a diagrammatic language for relations: string diagrams in a compact closed symmetric monoidal category, with generators for arbitrary finite relations, cups and caps for transposition, and a feedback loop labeled by the shift relation that encodes internal state. The quasi-normal form puts every diagram into a single feedback with one relation box, and the simulation principle lets a mediating relation S slide through the diagram, turning one transducer's transitions into another's while preserving behavior. In the bi-infinite case the proof additionally uses forward and backward pruning to remove states not lying on bi-infinite paths, followed by determinization and minimization, with the uniqueness of the minimal rooted right-resolving pruned presentation supplying the canonical object that forces any two equivalent diagrams to meet.

What would settle it

Construct a sofic subshift with two non-isomorphic minimal rooted right-resolving pruned presentations, or exhibit a deterministic automaton for its factor language that is strictly smaller than the canonical one yet whose transformation into a pruned right-resolving presentation yields something no larger than the canonical one; either would falsify Theorem 4.4 and with it the bi-infinite completeness theorem.

Watch

Extended reading notes

Core claim

The central discovery is a complete equational theory for transducers, stated as Theorem 3.5 for finite words and Theorem 4.6 for bi-infinite words. For finite words, any two diagrams of the syntactic category Trans with equal relational semantics can be rewritten into each other using the rules of Trans plus the simulation principle of Figure 4; the proof mimics determinization and minimization of finite automata. For bi-infinite words, the analogous statement holds for Z-Trans using the more intricate simulation principle of Figure 6, whose proof relies on a new canonical form: every non-empty sofic subshift has a unique minimal rooted right-resolving pruned presentation, up to isomorphism. Thus language equivalence, trace equivalence, and subshift equivalence all become provable by rewriting in a single compositional formalism.

Load-bearing premise

The bi-infinite completeness proof depends on the claim that every non-empty sofic subshift has a unique minimal rooted right-resolving pruned presentation, and the proof of that uniqueness contains a step that is only sketched in a few lines.

Editorial extensions

If this is right

  • If the completeness results hold, every equivalence of regular relations and every equivalence of sofic relations is derivable by the rewrite rules, so diagrammatic proof replaces case-by-case automata constructions.
  • Automata minimization and trace-equivalence checking become instances of the same rewriting system, formalizing the folklore similarity among these arguments.
  • The simulation principle simultaneously subsumes forward and backward simulation: mutual simulation between two transducers implies their equivalence, generalizing the classical simulation-based proof method.
  • The uniqueness of the minimal rooted right-resolving pruned presentation gives a canonical form for sofic subshifts, a notion not available from the standard minimal presentations, which are generally not unique.
  • Because the semantics is defined by interpretation in relations, the rewrite system is sound by construction, so any identity proved by rewriting is guaranteed to hold semantically.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural testable direction, left implicit by the authors, is whether the rewriting system can be made terminating or confluent enough to yield a decision procedure for transducer equivalence; the paper proves completeness but does not address normalization.
  • Changing the base category from relations to stochastic kernels or quantum channels, as the authors suggest, would transfer the same diagrammatic completeness scheme to probabilistic or quantum transducers, provided an analogue of the simulation principle can be stated in those settings.
  • The new canonical presentation for sofic subshifts may be useful independently of this paper, for instance in computing invariants or in comparing presentations of symbolic dynamical systems, since it selects a unique minimal object where classical minimal presentations can split.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper introduces two string-diagrammatic equational theories, Trans and Z-Trans, for finite-state transducers on finite words and on bi-infinite words, respectively. The diagrams are interpreted as uniform relations or as relations on bi-infinite words. The authors prove universality (every regular/sofic relation is representable) and soundness of the rewrite rules, and then claim completeness: any two diagrams with equal semantics can be proved equal using the rules plus a simulation principle. The finite-word completeness proof follows the classical determinization/minimization route. The bi-infinite case requires a new canonical form: every non-empty sofic subshift has a unique minimal rooted right-resolving pruned presentation (Theorem 4.4), proved in Appendix C.3, on which the bi-infinite completeness theorem (Theorem 4.6) relies.

Significance. The paper's central claim, if fully established, would give a genuinely unified compositional syntax for regular relations, LTS trace equivalence, and sofic subshifts, with proof rules for equational reasoning. The finite-word completeness proof is sound and elegant, and the proposed simulation principle is a natural generalization of forward/backward simulation. The paper is mostly self-contained and includes direct proofs for soundness, universality, and the main normal-form lemmas. The new uniqueness theorem for rooted pruned presentations is a potentially useful contribution to symbolic dynamics. However, the bi-infinite completeness proof currently rests on a proof step in Appendix C.3 that is not fully justified, and Appendix C.1 contains a false lemma; both are repairable.

major comments (2)
  1. [Appendix C.3, proof of Theorem C.8] The argument that the totalized presentation M⊥ is the minimal complete DFA of Fact(X) is incomplete. After assuming a strictly smaller complete DFA E, the proof says that restricting E to its final states gives a pruned right-resolving rooted presentation strictly smaller than M. This does not follow if |Q_E| = |P| and E has |P| final states; the derived presentation would have |P| states, not fewer. The missing observation is that in the non-total case Fact(X) ≠ A*, so every complete DFA for Fact(X) must have a non-final state (any state reached by a rejected word). Hence |F_E| ≤ |Q_E| - 1 ≤ |P| - 1, giving the required strict contradiction. Since Theorem 4.6 invokes Theorem 4.4 as its key normal-form uniqueness, this step needs to be stated and proved.
  2. [Appendix C.1, Lemma C.3] Lemma C.3 asserts that all states of the minimal automaton of a factor-closed language are final. This is false as stated. For A={a,b} and L=a*, the minimal complete DFA has an initial accepting state and a non-final dead state; the dead state is reachable but not co-accessible. The correct statement is that every state lying on an accepting run is final, and in a complete minimal DFA the only non-final state is the (possibly absent) dead state reached by words outside L. The proof of Theorem C.8 only uses the weaker property, so the main argument can be repaired, but the lemma should be corrected or removed.
minor comments (5)
  1. [Appendix D.3, Theorem D.3] In the induction step of the compactness proof, the first induction hypothesis is misprinted: it should read '(a_k, q_{k+1}) T (b_k, q_k) for all -n ≤ k < n', not '(a_n, q_{n+1}) T (b_n, q_n)'.
  2. [Definition 4.4] Typo: 'every accepted word admits an accepted run starting by r' should be 'starting from r' or 'starting with r'.
  3. [Section 4.3, Figure 6] The preconditions of the bi-infinite simulation principle are hard to read from the diagram. A concise textual statement with explicit quantifiers over states and paths of length card(C) and card(D) would significantly improve clarity.
  4. [Section 3.4, Figure 4] In the finite simulation principle, it would be helpful to state explicitly that S is an arbitrary relation of FinRel from C to D, matching the wires in the diagram, and that the equalities in the preconditions are equalities of relations.
  5. [Appendix D.6, proof of soundness of Figure 24] The sentence 'we can replace the left part of the above diagram by S ◦ •D' would benefit from a short justification that •D is the maximal relation and that the replacement preserves the existence of the connecting sequence; as written, the step is easy to miss.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the completeness theorems are proved against the relation semantics via classical automata-theoretic normal forms, not by assuming the target equivalence.

full rationale

The paper's central claims are the completeness theorems for finite and bi-infinite word transducers (Theorems 3.5 and 4.6). The derivation chain is self-contained: the equational theories Trans and Z-Trans are interpreted semantically in UniRel and Z-Rel, and the soundness of every rewriting rule, including the simulation principles, is proved directly against that semantics (Appendix B.4 for Figure 4; Appendix D.6 for Figure 6). Completeness is then obtained by a two-stage normal-form argument: determinization and minimization, followed by an appeal to uniqueness of the minimal deterministic automaton from the external textbook [HMU07] in the finite case, and to the in-paper Theorem 4.4 in the bi-infinite case. Theorem 4.4 is itself proved in Appendix C.3 from the same classical minimal-DFA uniqueness plus pruning/rooting constructions; it is not imported from a prior author-specific uniqueness theorem, and its proof does not assume the completeness statement it supports. The simulation principles are axioms of the equational theory whose soundness is shown semantically; they are not fitted parameters, and no predicted quantity is defined in terms of the data it is said to predict. The self-citations present in the paper ([CM24], [CDP21]) appear in the introduction and conclusion as context or related work and are not load-bearing for the completeness proofs. The skeptical concern about the compressed minimality step in Appendix C.3 is a potential proof gap or correctness risk, not a circularity: even if that step required a fuller argument, the claim being proved is not, by construction, identical to its input. Consequently, no step reduces to its own target by definition, and the circularity score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central claims rest only on standard results from category theory, automata theory, and symbolic dynamics. No free parameters, fitted constants, or ad-hoc mathematical objects are introduced; the new 'rooted right-resolving pruned presentation' is a definition, not a postulated entity.

assumptions (4)
  • standard math FinRel and UniRel are compact closed strict symmetric monoidal categories.
    Used throughout Section 2 and Appendix A to justify string-diagram manipulation, cups/caps, and the lifting functor (−)∗.
  • standard math The minimal deterministic automaton recognizing a regular language is unique up to isomorphism (Myhill-Nerode).
    Invoked in the proofs of Theorem 3.5 and Theorem 4.4 to identify two automata after determinization and minimization (see Corollaries 3.9 and 4.12).
  • domain assumption A subshift is sofic if and only if its factor language is regular, and the factor-language/pruned-language correspondence is a bijection between sofic subshifts and pruned factor-closed regular languages.
    The paper proves Proposition 4.3 in Appendix C.1 using compactness of AZ and standard facts about regular languages; this is a central correspondence for the bi-infinite case.
  • standard math AZ with the Cantor distance is compact.
    Used in Lemma 4.2 (limit languages are closed), Lemma 4.5 (infinite runs are limits of finite runs), and Theorem D.3 (compactness for the simulation principle).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Complete Compositional Syntax for Finite Transducers on Finite and Bi-Infinite Words." pith.science (2026). https://pith.science/paper/UW6RALJP

@misc{pith2026250206450,
  author       = {Pith},
  title        = {Pith review of: Complete Compositional Syntax for Finite Transducers on Finite and Bi-Infinite Words},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UW6RALJP}},
  note         = {Machine review of arXiv:2502.06450}
}
read the original abstract

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

Figures

Figures reproduced from arXiv: 2502.06450 by the authors.

Figure 1
Figure 1. Equations for the Cup and Cap. Nevertheless, those graphical representations remain practical, especially when repre￾senting various kind of compositions. The usual ones are the sequential compositions of R : A → B with S : B → C, and the parallel composition of R : A → B and S : C → D, which are defined as follows: A R S C B A R C S B D S ◦ R = {(a, c) | ∃b ∈ B, a R b, b S c} R × S = {((a, c),(b, d)) | a R b, c S d… view at source ↗
Figure 1
Figure 1. We redirect to [Sel11] for a survey of variations ar [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Equations for a Feedback Category. = idA A A = γA,B A B B A AA A B B A A C R S B = A C S ◦ R R S A B C D = R × S A B C D [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figures from the paper (21 more)
Figure 4
Figure 4. Figure 4: to obtain completeness. In order to ensure that the equations are not contradictory6 , we provide a semantics and prove soundness of our equations. The semantics is a strong symmetric monoidal functor from Trans to UniRel, which we write J−K, and is actually simply “re…
Figure 5
Figure 5. Figure 5: Sliding. Theorem 3.5 (Completeness). For R and T two diagrams of Trans from A to B. When￾ever JRK = JTK, we can rewrite R into T by using only the rules of Trans and [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]
Figure 6
Figure 6. Figure 6: Simulation Principle for Bi-Infinite Words, and an [PITH_FULL_IMAGE:figures/full_fig_p014_6.png]
Figure 7
Figure 7. Figure 7: Equations for a Strict Symmetric Monoidal Categor [PITH_FULL_IMAGE:figures/full_fig_p017_7.png]
Figure 8
Figure 8. Figure 8: Equations for the Cup and Cap A The Category of Relations All the diagrams of Section 2 can actually be formalized using string diagrams from category theory [Mac98]. Indeed, finite sets and relations is well known to be a strict symmetric monoidal category, called Fin…
Figure 9
Figure 9. Figure 9: Generators of Trans. We start by recalling the generators of our language and all its equations in Figures 9 to 12. Then we formally define the semantics J−K : Trans → Rel inductively on the syntax, as shown in [PITH_FULL_IMAGE:figures/full_fig_p018_9.png]
Figure 10
Figure 10. Figure 10: Equations for a Strict Symmetric Monoidal Catego [PITH_FULL_IMAGE:figures/full_fig_p019_10.png]
Figure 11
Figure 11. Figure 11: Equations for a Feedback Category. We now prove the soundness of the equational theory. The soundness of the equations stating that Trans is a strict symmetric monoidal category follows immediately from the fact that Rel is a strict symmetric monoidal category, so we …
Figure 12
Figure 12. Figure 12: Equations for Faithfully Embedding FinRel. R . B1 . . A1 R B C I | F A C A A A B B A An Bm . . . 7→ A∗ A∗ 7→ A∗ B∗ B∗ A∗ 7→ R∗ B∗ . 1 . . A∗ 1 A∗ n B∗ m . . . 7→ JRK C ∗ I | F A∗ C ∗ B∗ R S B A C 7→ C A∗ B ∗ ∗ JRK JSK R S A 7→ C ∗ A∗ JRK JSK B C D B∗ D∗ [PITH_FULL_IM…
Figure 13
Figure 13. Figure 13: Inductive Definition of the Semantics J−K : Trans → UniRel. B.5 Minimization of finite transducers We provide the full proof of Proposition 3.8. Using the logical reasoning as in Section 2, we can rewrite the equation as the following. We are looking at ∀a ∈ A, ∀p ∈ Q…
Figure 14
Figure 14. Figure 14: Semantics of the Simulation Principle for Finite [PITH_FULL_IMAGE:figures/full_fig_p020_14.png]
Figure 15
Figure 15. Figure 15: Backward-Simulation Principle for Finite Words [PITH_FULL_IMAGE:figures/full_fig_p021_15.png]
Figure 17
Figure 17. Figure 17: Deducible Equation. 21 [PITH_FULL_IMAGE:figures/full_fig_p021_17.png]
Figure 18
Figure 18. Figure 18: Generators of Z-Trans. R A B S C T D = R A B S C T D R A B = R A B = R BA R A B C S D E T F = R A B C S D E T F R A B = R A B R A B = R A B C R A B S C T D E F = T D U FE R A B C S D R A B C S DD B A C = = A B A B A B S U [PITH_FULL_IMAGE:figures/full_fig_p027_18.png]
Figure 19
Figure 19. Figure 19: Equations for a Strict Symmetric Monoidal Catego [PITH_FULL_IMAGE:figures/full_fig_p027_19.png]
Figure 20
Figure 20. Figure 20: Equations for a Feedback Category. = idA A A = γA,B A B B A AA A B B A A C R S B = A C S ◦ R R S A B C D = R × S A B C D [PITH_FULL_IMAGE:figures/full_fig_p028_20.png]
Figure 21
Figure 21. Figure 21: Equations for Faithfully Embedding FinRel. • The wires and every syntactical construct are in thick red, to distinguish them from actual relations. In particular, R refers to an actual relation while R refers to an element of our language. • Double-line boxes denote t…
Figure 22
Figure 22. Figure 22: Inductive Definition of the Semantics J−K : Z-Trans → Z-Rel. bottom-left equations also follow from the fact that Rel is a strict symmetric monoidal category. The top-right is sound because ⊲1 = id1, and the bottom-right is sound because ⊲C × ⊲D = ⊲C×D. D.4 Quasi-Norm…
Figure 23
Figure 23. Figure 23: Simulation Principle for Bi-Infinite Words, and a [PITH_FULL_IMAGE:figures/full_fig_p029_23.png]
Figure 24
Figure 24. Figure 24: Backward-Simulation Principle for Bi-Infinite Wo [PITH_FULL_IMAGE:figures/full_fig_p030_24.png]
Figure 25
Figure 25. Figure 25: Forward-Simulation Principle for Bi-Infinite Wo [PITH_FULL_IMAGE:figures/full_fig_p030_25.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

5 extracted references · 3 canonical work pages

  1. [1]

    A categorical semantics of signal flow graphs

    [BSZ14] Filippo Bonchi, Pawe/suppress l Soboci´ nski, and Fabio Zanasi. “A categorical semantics of signal flow graphs”. In: International Conference on Concurrency Theory . Springer. 2014, pp. 435–450. [BSZ21] Filippo Bonchi, Pawe/suppress l Soboci´ nski, and Fabio Zanasi. “A survey of compositional signal flow theory”. In: Advancing Research in Informatio...

    work page 2021

  2. [1997]

    Differentiab le causal computations via delayed trace

    isbn: 978-0-534-94728-6. [SK19] David Sprunger and Shin-ya Katsumata. “Differentiab le causal computations via delayed trace”. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . IEEE. 2019, pp. 1–12. [Wet20] John van de Wetering. “ZX-calculus for the working q uantum computer scien- tist”. In: arXiv preprint arXiv:2012.13966 (202...

    arXiv 2020

  3. [1998]

    A String Diagr ammatic Axiomatisation of Finite-State Automata

    isbn: 0-387-98403-8. [PZ+21] Robin Piedeleu, Fabio Zanasi, et al. “A String Diagr ammatic Axiomatisation of Finite-State Automata.” In: FoSSaCS. 2021, pp. 469–489. [Sel11] Peter Selinger. “A survey of graphical languages fo r monoidal categories”. In: New structures for physics (2011), pp. 289–355. [Sip97] Michael Sipser. Introduction to the theory of com...

    work page 2011

  4. [2007]

    Coherence for compact c losed categories

    isbn: 978-0-321-47617-3. [KL80] G.M. Kelly and M.L. Laplaza. “Coherence for compact c losed categories”. In: Journal of Pure and Applied Algebra 19 (1980), pp. 193–213. issn: 0022-4049. doi: https://doi.org/10.1016/0022-4049(80)90101-2. url: https://www.sciencedirect.co [KSW02] Katis, P., Sabadini, Nicoletta, and Walters, Rober t F.C. “Feedback, trace and...

    doi:10.1016/0022-4049(80)90101-2 1980

  5. [2024]

    Aperiodicity in Quantum Wang Tilings

    arXiv: 2302.04503 [quant-ph]. url: https://arxiv.org/abs/2302.04503. [DFR22] Elena Di Lavore, Giovanni de Felice, and Mario Rom´ a n. “Monoidal streams for dataflow programming”. In: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science . 2022, pp. 1–14. [EM65] Calvin C. Elgot and Jorge E. Mezei. “On Relations Defin ed by Generalize...

    work page Pith review arXiv 1965

Pith tools

Reviewed August 8, 2026 · model on record in the stance chip above.