Tree transducers of linear size-to-height increase (and the additive conjunction of linear logic)

TL;DR

This paper introduces a new class of tree functions computed by tree transducers with linear size-to-height increase, situated between known classes, and characterizes it via lambda calculus and game semantics.

Contribution

It defines and analyzes a novel class of tree functions extending regular tree functions, with closure properties and a lambda calculus characterization.

Findings

The class includes more than MSO transductions but is contained within macro tree transducers.

It is closed under certain compositions, forming a strict hierarchy.

An alternative lambda calculus characterization using additive tuples is provided.

Abstract

We investigate a natural generalization to trees of Hennie machines, a known automaton model for regular string functions. Tree-to-tree Hennie machines are tree-walking tree transducers with the ability to rewrite the node labels of their input tree, subject to a bounded visit restriction. Interestingly, they do not merely compute regular tree functions (i.e. MSO transductions), but a larger class of functions with linear size-to-height increase (LSHI). We prove that this class sits between LSHI macro tree transducers (MTTs) and MSO set interpretations. To argue for its robustness, we show that it is closed under precomposition (resp. postcomposition) by MTTs of linear size (resp. height) increase. As a consequence, it contains the entire composition hierarchy of MTTs of linear height increase; we also prove that this composition hierarchy is strict. Finally, we give an alternative characterization of this function class based on a lambda-calculus with linear types. The key difference with similar characterizations of MSO transductions is the use of additive tuples in the encoding of output trees. Our equivalence proof, using game semantics / geometry of interaction, is heavily inspired by an analogous result on higher-order recursion schemes.