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.

翻译：我们研究了Hennie机（一种用于正则字符串函数的已知自动机模型）在树结构上的自然推广。树到树Hennie机通过改写输入树的节点标签（受有界访问次数的约束）进行树遍历变换。有趣的是，它们不仅计算正则树函数（即MSO转换），还计算一类具有线性尺寸-高度增长（LSHI）的更大函数类。我们证明该类介于LSHI宏树转换器（MTT）与MSO集合解释之间。为论证其鲁棒性，我们证明其在线性尺寸（或高度）增长的MTT预复合（或后复合）下封闭。由此可知，它包含线性高度增长的MTT的整个复合层次，并进一步证明该复合层次具有严格性。最后，我们基于带线性类型的λ-演算给出该函数类的另一种刻画。与MSO转换的类似刻画的关键区别在于输出树编码中使用加性元组。通过博弈语义/交互几何实现的等价性证明，深受高阶递归方案中类似结论的启发。