单子、余单子与转换器
Monads, Comonads, and Transducers
AI总结：
本文提出基于单子与余单子的可识别转换器框架，统一推广 Mealy 机、有理转换及无限词和 term 上的转换，并在相干公理下证明其复合封闭性，且用 Coq 完成形式化证明。
摘要：
本文提出了一种基于单子（monads）和余单子（comonads）的可识别转换器定义，该定义架起了当前正则性研究中两项重要持续工作之间的桥梁。第一项工作是对正则转换的研究，它将正则性的概念从语言扩展到词到词函数。另一项重要工作是将正则语言的概念从词推广到任意单子，这一推广由 arXiv:1502.04898 引入。本文给出了若干适用于所提框架的转换器类别示例。特别地，我们证明了我们的类别推广了 Mealy 机和有理转换的类别。我们还给出了针对无限词以及一种被称为 term 的特定类型树的可识别转换器示例。本文的主要结果是一个定理，该定理表明：在单子结构与余单子结构之间满足某些相干公理的条件下，可识别转换类别对复合封闭。由于其复杂性，我们在 Coq Proof Assistant 中形式化了该定理的证明。在证明中，我们引入了针对 Eilenberg-Moore 代数的上下文概念和广义圈积概念，它们可能成为研究这些代数的有价值工具。
英文摘要：
This paper proposes a definition of recognizable transducers over monads and comonads, which bridges two important ongoing efforts in the current research on regularity. The first effort is the study of regular transductions, which extends the notion of regularity from languages into word-to-word functions. The other important effort is generalizing the notion of regular languages from words to arbitrary monads, introduced in arXiv:1502.04898. In this paper, we present a number of examples of transducer classes that fit the proposed framework. In particular we show that our class generalizes the classes of Mealy machines and rational transductions. We also present examples of recognizable transducers for infinite words and a specific type of trees called terms. The main result of this paper is a theorem, which states the class of recognizable transductions is closed under composition, subject to some coherence axioms between the structure of a monad and the structure of a comonad. Due to its complexity, we formalize the proof of the theorem in Coq Proof Assistant. In the proof, we introduce the concepts of a context and a generalized wreath product for Eilenberg-Moore algebras, which could be valuable tools for studying these algebras.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
