A transducer model for simply typed λ-definable functions

Among the natural ways to define functions ℕ^k -> ℕ in the simply typed λ-calculus, one of them allows hyperexponential growth (any tower of exponentials) but excludes many basic functions such as subtraction and equality, as was discovered by Statman in the 1980s. Until now, this function class did not have any characterization not mentioning the λ-calculus. We provide the first one, which more generally encompasses λ-definable tree-to-tree functions, using an automata model: "collapsible pushdown transducers". As the name of our machines suggests, we draw on the known connections between collapsible pushdown automata and simply typed λ-calculus with fixpoints; in fact, one might think of our results as being about recursion schemes parameterized by finite input trees. Other significant inspirations include: * Engelfriet et al.'s work on higher-order pushdown tree transducers, which are included in our model while already being to our knowledge the most expressive transducer model in the literature (polyregular functions, macro tree transducers, etc. define strict subclasses); * an old result of Plotkin, recently made available thanks to Urzyczyn ( https://arxiv.org/abs/2206.08413 ), showing that the presence of fixpoints does not affect what total functions can be expressed. This (unpublished) work is a sequel to my collaboration with Pierre Pradic on "implicit automata", see this previous session of the MIMUW automata seminar: https://www.mimuw.edu.pl/aktualnosci/seminaria/implicit-automata-l-calculi-joint-work-le-thanh-dung-aka-tito-nguyen