论文标题
类型$λ$ -CALCULI II中的隐式自动机II：流传感器与分类语义
Implicit automata in typed $λ$-calculi II: streaming transducers vs categorical semantics
论文作者
论文摘要
我们将常规的字符串转换表征为带有添加剂的线性$λ$ -calculus中的程序。通过编码将常规函数计算到我们的$λ$ -calculus中的无拷贝流式传感器（SSTS）来证明此等价的一个方向。对于相反，我们考虑了一个分类框架，用于定义单词上的自动机和换能器，这使我们能够将SST中的寄存器更新与合适的单体封闭类别中的线性$λ$ -calculus的语义相关联。为了说明单体闭合与自动机理论的相关性，我们还利用了这一概念来对参数进行抽象的概括，以表明可以确定无拷贝的SST，并且两个常规功能的组成可以由无拷贝的SST实现。然后，我们的主要结果是使用类似方法从字符串到树的概括。在此过程中，我们展示了流媒体传感器的特征与线性逻辑的乘法/加法区别之间的联系。 关键词：MSO转换，隐性复杂性，辩证神类别，教堂编码
We characterize regular string transductions as programs in a linear $λ$-calculus with additives. One direction of this equivalence is proved by encoding copyless streaming string transducers (SSTs), which compute regular functions, into our $λ$-calculus. For the converse, we consider a categorical framework for defining automata and transducers over words, which allows us to relate register updates in SSTs to the semantics of the linear $λ$-calculus in a suitable monoidal closed category. To illustrate the relevance of monoidal closure to automata theory, we also leverage this notion to give abstract generalizations of the arguments showing that copyless SSTs may be determinized and that the composition of two regular functions may be implemented by a copyless SST. Our main result is then generalized from strings to trees using a similar approach. In doing so, we exhibit a connection between a feature of streaming tree transducers and the multiplicative/additive distinction of linear logic. Keywords: MSO transductions, implicit complexity, Dialectica categories, Church encodings
