Implicit automata in λ-calculi III: affine planar string-to-string functions

TL;DR

This work characterizes first-order string-to-string transductions via the planar affine λ-calculus $\lambda\wp$ with Church encodings, proving that FO transductions coincide with $\lambda\wp$-definable functions and that $\lambda\wp$-transducers can be compiled into two-way planar reversible transducers (2PRFTs). The authors develop a poset-enriched, monoidal-closed semantic framework using planar diagrams (TransDiag_Γ) to interpret $β$-reductions as inequalities, enabling a bridge between typed lambda terms and automata-theoretic transductions. The Krohn–Rhodes decomposition plays a central role in showing the FO side can be captured by $\lambda\wp$, with a constructive translation in both directions between $\lambda\wp$ constructs and 2PRFTs. This extends previous star-free characterizations and clarifies the exact boundary between affine lambda-calculus expressiveness and first-order string transductions, while also outlining variants without planarity and potential extensions to tree languages. The results provide a low-complexity, diagrammatic route from higher-order term calculi to automata that can inform both theory and SEO-friendly metadata generation for related topics.

Abstract

We prove a characterization of first-order string-to-string transduction via $λ$-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 $λ$-term using a known Krohn-Rhodes-style decomposition lemma. The converse direction is given by compiling $λ$-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 $λ$-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 $β$-equivalent terms, but it does turn $β$-reductions into inequalities in a poset-enrichment of the category of diagrams.

Figures (7)

• Figure 1: Syntax and typing rules for $\lambda\wp$. The contexts $\Psi$ and $\Delta$ are lists of pairs $x : \tau$ containing a variable name $x$ and some type $\tau$. We assume that all variables appearing in a context and under binders are pairwise distinct and that terms and derivations are defined up to $\alpha$-renaming.
• Figure 2: A geometric realization of a morphism from $+-+--$ to $+-+-+$. The edge directions are not part of the definition, but inferred from the polarity labels of the source and targets. When the label is $\epsilon$, we omit it from the picture.
• Figure 3: How morphisms compose
• Figure 4: The monoidal product of two morphisms
• Figure 5: Identity, cup and cap for the object $-+$

Theorems & Definitions (42)

• definition 1
• definition 2
• definition 3
• definition 4
• definition 5
• definition 6
• lemma 1
• proof
• proposition 1: standard argument, see also aperiodic
• definition 7