Automata theory starts with the well-known correspondence between regular languages and various kinds of finite-state automata. What happens if you consider automata-like devices that, instead of recognizing languages, compute string-to-string (or tree-to-tree) functions? Such devices are called transducers. Interestingly, there is a plethora of transducer models, sometimes but not always equally expressive.

The class of regular string functions has several equivalent definitions by machine models (two-way finite transducers, copyless streaming string transducers, …), and another one using logic (MSO transductions), attesting to its robustness/canonicity.

• Mikołaj Bojańczyk and I have proposed a concise algebraic characterization, analogous to recognizability by finite monoids for regular languages, but using a little bit of categories (slides; alternate slides+video for category theorists: SYCO 11).
• Cécilia Pradic and I have shown that two-way transducers with planar behaviors — an idea from Peter Hines — compute exactly the aperiodic regular functions i.e. FO transductions (slides).

Polyregular functions are a more recent trending topic in string transducers. They were given this name by Bojańczyk because their output has size polynomially bounded in the input size, and they extend the regular functions (which have linear output size).

• Pradic and I have introduced the subclass of comparison-free polyregular (or polyblind) functions (slides), studied further by Gaëtan Douéneau-Tabot in his PhD thesis.
• I have also looked into questions concerning the degree of polynomial growth of a polyregular function. They turn out to be closely connected to older works on tree transducer hierarchies (by Engelfriet, Vogler, Maneth, …), as shown in my work with Kiefer & Pradic (arXiv preprint) and with Gallot & Lhote (in preparation; slides 1, slides 2).

The field of implicit computational complexity seeks to characterize complexity classes by using constrained programming languages. Linear type systems are typically used for that purpose, since they enable static restrictions on duplication and iteration. Cécilia Pradic and I have been investigating a counterpart to implicit complexity for automata and transducers; it turns out “single-use” or “copyless” restrictions, that look a lot like linearity, already played an important role in automata theory. Our starting point was a theorem of Hillebrand & Kanellakis about characterizing regular languages in the simply typed λ-calculus.

This is the topic of my PhD dissertation (final revision: March 2023; defense (slides): December 2021). For a shorter read, you can look at the first paper in the series: Aperiodicity in a non-commutative logic (perhaps one of my favorite results in my entire career).

There is more to say about this ongoing research programme: it is closely related to earlier works concerning higher-order transducers (though our characterization of polyblind functions cannot be expressed in this framework) and abstract categorial grammars; ideas from higher-order model checking can be used to handle infinite trees; …

The study of linear logics has led to developing formal proof systems going beyond the limits of the traditional sequent calculus. Deep inference liberalizes the possible applications of deduction rules. Proof nets represent proofs as graph-like objects from which it is not obvious to reconstruct a sequence of deductions; subtle combinatorial conditions are needed to ensure that a proof net is correct.

The first logic to use deep inference, system BV, attempted to be an equivalent presentation of an existing logic based on proof nets, namely pomset logic. But in fact, these two logics are not equivalent; furthermore, provability is more computationally difficult in pomset logic (it is ${\mathrm{\Sigma }}_2^{\mathrm{P}}$-complete) than in BV (NP-complete). This is what Lutz Straßburger and I showed in a journal paper, which hope will also serve as a useful reference for BV and pomset logic. Indeed, while I don't work on this topic anymore, it is still active; for instance, connections between pomset logic and higher-order causal processes have been found recently.

One important aspect of the above work is to draw inspiration from the literature on graph algorithms to study the proof nets of pomset logic. In another arXiv note, I prove some anecdotal graph-theoretic results initially motivated by my early work on proof nets for Multiplicative Linear Logic with Mix (MLL+Mix). In particular, this concerns perfect matchings, edge-colored graphs and paths/trails avoiding forbidden transitions. My interest in these objects started with a recreational algorithmic puzzle given by Christoph Dürr during an internship supervised by him and by Nguyễn Kim Thắng (for a master's degree in operations research). The connection between perfect matchings and proof nets was first discovered by Christian Retoré, who is also the inventor of pomset logic.

Finally, with Thomas Seiller, we also built a semantics of MLL+Mix which gives a computational / interactive explanation of a correctness criterion for proof nets in MLL+Mix by Retoré (again!) based on cographs. We later realized that this could be extended to pomset logic (see the end of these slides). A throwaway sentence in the conclusion mentioning possible uses of prime graphs and modular decomposition in proof theory coincidentally anticipated a line of work that appeared soon afterwards by Matteo Acclavio and his collaborators.

I have worked with Bojańczyk and Stefański on using ideas from linear logic to relax the “single-use restriction” on functions between orbit-finite sets, leading to a category with function spaces (weak monoidal closure). This was inspired by an ongoing project with Eberhart and Pradic on extending implicit automata in linear logic to infinite alphabets.

The use of finitary semantics to study λ-terms, which plays an important role in my work on “implicit automata”, had also led Sylvain Salvati to define regular languages of simply typed λ-terms at arbitrary types. Vincent Moreau have a paper about their various equivalent definitions, using logical relation arguments. (We also have a cute example: among the third-order encodings of untyped λ-terms (as syntax trees with binders modulo α-renaming), the subset of linear terms is regular.)

Consider the following decision problem, for some fixed variant of the λ-calculus: given two terms as input, are they convertible? Equivalently, if we work in a normalizing system, do they reduce to the same normal form?

I showed that this problem is P-complete for planar λ-terms (also known as “ordered” or “non-commutative” λ-terms; joint work with Das, Mazza and Zeilberger) and TOWER-complete for safe λ-terms. In other words, the planarity (resp. safety) condition does not decrease the computational complexity of the convertibility problem in the linear (resp. simply typed) λ-calculus. The proof techniques for both results are inspired by my work on implicit automata.

What led me to implicit automata (cf. above) was finding out that regular languages occur in a language with linear types designed for implicit complexity, giving an unexpected answer to a question by Patrick Baillot. It turns out that the proof for this relies on old ideas on the denotational semantics of second-order linear logic. Another direction was to understand how to go beyond regular languages using the same ideas.

The result was an implicit characterization of something between L and NL (probably L…), whose proof uses a bit of semantics and of category theory (in particular normal functors). The implicit complexity side of the story — a joint work with Cécilia Pradic — was published. The semantics side is far from being as rigorous as I would like and is projected to be rewritten at some point (I don't have the excuse of having to write my PhD dissertation anymore…); in the meantime, you can take a look at this old preprint.