Implicit automata in typed $\lambda$-calculi II: streaming transducers vs categorical semantics

TL;DR

This paper establishes a deep connection between regular string and tree transductions and linear $alculus$, using categorical semantics to relate automata, transducers, and linear logic features.

Contribution

It introduces a categorical framework linking streaming transducers and linear $alculus$, generalizing results from strings to trees and highlighting the role of monoidal closure.

Findings

Encoding SSTs into linear alculus demonstrates equivalence with regular functions.

Categorical semantics relate register updates to monoidal closed categories.

Generalization from strings to trees connects transducer features with linear logic.

Abstract

We characterize regular string transductions as programs in a linear $\lambda$-calculus with additives. One direction of this equivalence is proved by encoding copyless streaming string transducers (SSTs), which compute regular functions, into our $\lambda$-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 $\lambda$-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