Lambdas, Transducers and MSO (Invited Talk)

Abstract

This talk will revolve around the classical question: 
What kind of maps from words to words or trees to trees can be considered as "well behaved" from an automata theoretic point of view? 
What means to be well-behaved is left unspecified on purpose, but one thing is sure is that one would expect as minimal requirement that the inverse image of a regular language under such a map be effectively regular. One would also expect to have nice closure properties for these maps, in particular under composition. Ideally, we would also like to have several different equivalent computation models for representing them.
This talk advertises the use of simply-typed lambda calculus as a good way to approach this question, and presents newer results concerning translations from and to exponential growth maps.
This line of research is rooted in a long literature, starting from the works of Damm on higher order grammars, and the works of Engelfriet and Vogler on macro-tree transducers, and more generally from works on higher-order tree transducers, as well as the results of Ong et al. on decidability of MSO over higher-order recursion schemes (a model that produces infinite trees). These works show in a broad sense that models of computation defined in simply typed lambda-calculus do preserve regularity under taking the inverse image.
Another connection is the recent implicit automata research programme initiated by Nguy~ên and Pradic, that was inspired by the seminal work of Hillebrand and Kanellakis. Here, automata models a directly viewed as programs written in some form of typed lambda-calculus, using Church encoding for representing inputs and outputs. When appropriately controlling the type system various it is possible to characterize various classes of finite state transducers studied in the literature.
A last approach comes from finite model-theory. In this context, Monadic Second-Order Logic (MSO for short, the extension of first-order in which one can further quantify over sets) is the prime logic for describing regular languages over words or trees. This logic can also be used for defining transformations from words/trees to words/trees. These are the notions of MSO-interpretations or MSO-transducers. A major contribution here is the study of the expressive power of MSO-interpretations of polynomial growth from words to words that was undertaken by Bojańczyk, Kiefer and Lhote, and shown equivalent to other formalisms of transducers and programming languages. This is the class of polyregular functions, and it satisfies all the expectation of the question. Yet it is limited to finite words as inputs and outputs, and to polynomial growth.
In a first part of the talk, we shall see how to use simply-typed lambda-calculus as a general mechanism for transforming trees into trees, and how it gives a positive answer to the original question. This description essentially repackages many ideas existing from the literature, in a way similar Gallot’s thesis. It also introduces a few new ones. In particular, we shall see generic results that some clearly identified classes of functional programs describing transformations from trees to trees can be effectively compiled into transducer-like models which perform only one pass on the input (i.e. higher-order tree transducers). This class of programs is also closed under composition. We shall also see how the logic MSO itself can be natively embedded in such models of computation. 
In a second part, we will see how this presentation relates to recent works with Lhote, Nguy~ên and Ohlmann in which extensions of polyregular functions to maps from words to words of exponential growth are studied. This work has the particularity to be the first one in the model-theoretic side of this theory in which it is key to allow lambda-terms to be unsafe.