We prove a characterization of first-order string-to-string transduction via $\lambda$-terms typed in non-commutative affine logic that compute with Church encoding, extending the analogous known characterization of star-free languages. We show that every first-order transduction can be computed by a $\lambda$-term using a known Krohn-Rhodes-style decomposition lemma. The converse direction is given by compiling $\lambda$-terms into two-way reversible planar transducers. The soundness of this translation involves showing that the transition functions of those transducers live in a monoidal closed category of diagrams in which we can interpret purely affine $\lambda$-terms. One challenge is that the unit of the tensor of the category in question is not a terminal object. As a result, our interpretation does not identify $\beta$-equivalent terms, but it does turn $\beta$-reductions into inequalities in a poset-enrichment of the category of diagrams.

翻译：我们通过非交换仿射逻辑中带Church编码计算的λ-项，证明了一阶字符串到字符串转换的一个刻画，这扩展了已知的无星语言类似刻画。我们证明，每个一阶转换都可以利用已知的Krohn-Rhodes风格分解引理通过λ-项计算。反向方向通过将λ-项编译为双向可逆平面转换器给出。该翻译的可靠性涉及证明这些转换器的转移函数存在于一个图表的幺半闭合范畴中，在其中我们可以解释纯仿射λ-项。一个挑战是所考虑的范畴的张量单位不是终端对象。因此，我们的解释不识别β-等价项，但它确实将β-归约转化为图表范畴的偏序丰富中的不等式。