2026-09-13T16:03:18Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22893 2026-09-05T18:00:04Z ddc:004 open_access

Slightly Non-Linear Higher-Order Tree Transducers Nguyễn, Lê Thành Dũng (Tito) Vanoni, Gabriele Almost affine lambda-calculus geometry of interaction reversibility tree transducers tree-walking automata 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 (à 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lê Thành Dũng (Tito) Nguyễn and Gabriele Vanoni 2025 Is Part Of LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2025.68 urn:nbn:de:0030-drops-228934 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.68 eng https://creativecommons.org/licenses/by/4.0/legalcode