(Almost) Affine Higher-Order Tree Transducers
<|reference_start|>(Almost) Affine Higher-Order Tree Transducers: We investigate the tree-to-tree functions computed by \enquote{affine$\lambda$-transducers}: tree automata whose memory consists of an affine $\lambda$-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{\`a 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 \titocecilia on \enquote{implicit automata} in an affine $\lambda$-calculus. The key technical tool in our proofs is the Interaction Abstract Machine (IAM), an operational avatar of the \enquote{geometry of interaction} semantics of linear logic. We work with ad-hoc specializations to (almost) affine $\lambda$-terms of a tree-generating version of the IAM.<|reference_end|>
@article{nguyên2024(almost),
    title={(Almost) Affine Higher-Order Tree Transducers},
    author={L^e Th`anh D~ung Tito Nguy^en and Gabriele Vanoni},
    journal={arXiv preprint arXiv:2402.05854},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.05854},
    primaryClass={cs.FL cs.LO}
}