Tito Nguyễn (LIP, ENS de Lyon), 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:

(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 (Swansea University) on "implicit automata".

NDLR: the talk will be given on the blackboard, so it might be not so easy to follow at a distance, given the available technology