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 et al.’s Linear High-Order Deterministic Tree Transducers.

When the memory is (almost) purely affine, we show that these machines can be translated to tree-walking transducers; 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 regular lookaround and allowing a limited amount of non-linearity, is equivalent in expressive power to Engelfriet et al.’s invisible pebble tree transducers.

The key technical tool in our proofs is the Interaction Abstract Machine, an operational avatar of the “geometry of interaction” semantics of linear logic. We work with ad-hoc specializations to λ-terms of low exponential depth of a tree-generating version of the IAM.