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 ($\textit{à 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.
翻译:我们研究了由'仿射$λ$-转换器'计算的树到树函数:这类树状自动机的内存由仿射$λ$-项而非有限状态构成。它们可视为Gallot、Lemay与Salvati提出的线性高阶确定性树状转换器的变体。当内存几乎完全仿射(遵循Kanazawa方法)时,我们证明这些机器可转换为树遍历转换器(若内存完全仿射,则得到可逆树遍历转换器)。这为Nguyên与Pradic关于仿射$λ$-演算中'隐式自动机'的表达力猜想提供了不可行性证明。我们还证明了一种功能更强的变体——通过MSO重标记进行预处理并允许有限非线性的扩展版本——在表达力上等价于Engelfriet、Hoogeboom与Samwel提出的隐形卵石树状转换器。证明中的关键技术工具是交互抽象机(IAM),它是Girard交互几何(线性逻辑的一种语义)的操作化实例。我们采用专门针对低指数深度$λ$-项的树生成版本IAM进行定制化研究。