一句话：用弦图语法为有限状态自动机建立有限完全等式理论，并证明 Kleene 星可派生。
本文研究有限状态自动机的语言等价公理化问题。作者将自动机通常的状态转移图重新解释为二维弦图（string diagrams）语法，从而在纯图示框架中刻画自动机的组合行为。核心贡献是为语言等价给出一个完全的等式理论，并且该公理化是有限的：不同于以往依赖 Kleene 星作为基本算子的做法，这里 Kleene 星是派生概念，可由更基本的代数块分解得到。评估以数学证明为主：证明该等式理论对语言等价完备，并展示星号的可导出性。结果为自动机、形式语言与图示代数语义之间建立了新的联系。
We develop a fully diagrammatic approach to finite-state automata, based on reinterpreting their usual state-transition graphical representation as a two-dimensional syntax of string diagrams. In this setting, we are able to provide a complete equational theory for language equivalence, with two notable features. First, the proposed axiomatisation is finite. Second, the Kleene star is a derived concept, as it can be decomposed into more primitive algebraic blocks.
@article{paperbot2236,
title = {A Finite Axiomatisation of Finite-State Automata Using String Diagrams},
author = {Robin Piedeleu and Fabio Zanasi},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:13)2023}
}