Complete Compositional Syntax for Finite Transducers on Finite and Bi-Infinite Words
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913685140668416 |
|---|---|
| author | Carette, Titouan de Visme, Marc Ducros, Vivien Lutfalla, Victor Moutot, Etienne |
| author_facet | Carette, Titouan de Visme, Marc Ducros, Vivien Lutfalla, Victor Moutot, Etienne |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_06450 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Complete Compositional Syntax for Finite Transducers on Finite and Bi-Infinite Words Carette, Titouan de Visme, Marc Ducros, Vivien Lutfalla, Victor Moutot, Etienne Logic in Computer Science Discrete Mathematics Formal Languages and Automata Theory 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. |
| title | Complete Compositional Syntax for Finite Transducers on Finite and Bi-Infinite Words |
| topic | Logic in Computer Science Discrete Mathematics Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2502.06450 |