Invisible pebbles and the geometry of affine higher-order tree transducers
summary
This work shows that affine λ-transducers with (almost) purely affine memory translate to tree-walking transducers, proving an inexpressivity conjecture of Nguyễn and Pradic on implicit automata; an extended variant with regular lookaround and a bounded amount of non-linearity is exactly equivalent to invisible pebble tree transducers. Proofs give explicit, implementable translations using a specialized Interaction Abstract Machine from geometry-of-interaction semantics; constructions yield reversible implementations for the purely affine case and nonreversible implementations when limited duplication is allowed.
AI-written summary · about
chapters (11)
- 0:00Higher-order tree transducers intro
- 3:37Automata to tree transducers
- 6:50Interaction ABS machines matter
- 9:39ABS machine explained
- 12:34First characterization theorem
- 13:59Quasifine Lambda calculus
- 15:46Full tree transducer characterization
- 16:49Geometry of interaction insights
- 17:31Invisible pebbles and XML parsing
- 18:56Future work and open questions
- 19:17Q&A