# Lambdas, Transducers and MSO (Invited Talk)

Thomas Colcombet

► To cite this version:

Thomas Colcombet. Lambdas, Transducers and MSO (Invited Talk). Mathematical Foundations of Computer Science (MFCS), Aug 2025, Varsovie, Poland. 10.4230/LIPIcs.MFCS.2025.1. hal-05413478

HAL Id: hal-05413478

https://hal.science/hal-05413478v1

Submitted on 12 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Lambdas, Transducers and MSO

Thomas Colcombet

CNRS, IRIF, Université Paris Diderot, France

## 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.

**2012 ACM Subject Classification** Theory of computation → Finite Model Theory; Theory of computation → Regular languages

**Keywords and phrases** Lambda-calculus, automata theory, finite model theory, MSO

**Digital Object Identifier** 10.4230/LIPIcs.MFCS.2025.1

**Category** Invited Talk

<figure><img src="image_2.png" /></figure>

© Thomas Colcombet;

licensed under Creative Commons License CC-BY 4.0

50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025).

Editors: Pawel Gawrychowski, Filip Mazowiecki, and Michał Skrzypczak; Article No. 1; pp. 1:1–1:1

Leibniz International Proceedings in Informatics

<figure><img src="image_3.png" /></figure>

LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany