Slightly Non-Linear Higher-Order Tree Transducers

TL;DR

The paper establishes deep connections between affine $\lambda$-transducers and classical tree automata by using the Interaction Abstract Machine to simulate higher-order memory in tree-walking and invisible-pebble transducers. It shows that purely affine $\lambda$-transducers, when preprocessed with $MSO$ relabeling, capture $MSOT$, while almost purely affine ones capture $MSOT$-S; a new characterization of $MSOT$-S$^2$ is obtained via almost depth-1/! depth constructs and invisible pebbles. The work integrates GoI-inspired semantics with automata theory to provide a unified framework for higher-order tree transductions and their preprocessing, offering both reversibility results and a route to compositional expressiveness. It also outlines future hierarchies and questions about the boundaries between these models and their practical implications for implicit automata theory.

Abstract

We investigate the tree-to-tree functions computed by "affine $λ$-transducers": tree automata whose memory consists of an affine $λ$-term instead of a finite state. They can be seen as variations on Gallot, Lemay and Salvati's Linear High-Order Deterministic Tree Transducers. When the memory is almost purely affine ($\textit{à la}$ Kanazawa), we show that these machines can be translated to tree-walking transducers (and with a purely affine memory, we get a reversible tree-walking transducer). This leads to a proof of an inexpressivity conjecture of Nguyên and Pradic on "implicit automata" in an affine $λ$-calculus. We also prove that a more powerful variant, extended with preprocessing by an MSO relabeling and allowing a limited amount of non-linearity, is equivalent in expressive power to Engelfriet, Hoogeboom and Samwel's invisible pebble tree transducers. The key technical tool in our proofs is the Interaction Abstract Machine (IAM), an operational avatar of Girard's geometry of interaction, a semantics of linear logic. We work with ad-hoc specializations to $λ$-terms of low exponential depth of a tree-generating version of the IAM.

Theorems & Definitions (57)

• Example 1.1
• Corollary 1.2: of Theorem \ref{['thm:main-affine']} below
• Definition 1.3
• Theorem 1.4
• Theorem 1.5
• Definition 1.6
• Theorem 1.7
• Proposition 1.8: proved in §\ref{['sec:lambdatrans']}
• Claim 2.1: Affineness
• Proposition 2.2: Normalization & subject reduction