Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: our work

Topic: Vincent Moreau

Vincent Moreau (Jul 02 2025 at 15:22):

Hi everyone! We may have already interacted here or in real life, I am a PhD student working under the supervision of Paul-André Melliès and Sam van Gool at IRIF, in Paris. Today, I am delighted to announce my upcoming PhD defence! The title of my PhD is:

A topological and fibrational approach to higher-order automata

The topic lies at the intersection of automata theory, semantics in cartesian closed categories, and Stone duality. The defence will take place on 2025-07-11T14:00:00+02:00 in Paris, and will be streamed for online attendance. All the relevant information is available on the dedicated webpage, as well as the PhD manuscript: https://www.irif.fr/users/moreau/defence

Vincent Moreau (Jul 02 2025 at 15:23):

The starting point of my thesis is the algebraic approach to automata theory, focused on recognition. Its fundamental observation is that the Boolean algebra of regular languages associated with some alphabet can be recovered by considering the monoid homomorphisms from the free monoid on that alphabet to finite monoids. On the topological side, the associated free profinite monoid, whose underlying space is the Stone dual of that Boolean algebra, can be computed using the codensity monad induced by the full subcategory of finite monoids.

Following the work of Sylvain Salvati, we move from algebraic language theory to denotational semantics by replacing monoids by cartesian closed categories. In that case, free cartesian closed categories have $\lambda$-terms as morphisms. By considering locally finite cartesian closed categories as the higher-order analogs of finite monoids, we thus obtain a notion of recognition for languages of $\lambda$-term. This situation amounts to an extension of automata theory, where new letters of the alphabet can be declared on the fly at higher-order types through currying.

Vincent Moreau (Jul 02 2025 at 15:23):

Here are the main contributions of my PhD thesis:

• We prove that all the locally finite, well-pointed, cartesian closed categories (that are not posetal) recognize the same languages as $\mathbf{FinSet}$, our prototypical example. We call these higher-order regular languages.
• In turn, we prove that this class of languages coincides with the one given by a natural extension of the syntactic approach of Hillebrand and Kanellakis to regular languages, in relation to the implicit automata research programme of Nguyễn and Pradic. To achieve that, we introduce a construction on cartesian closed categories called squeezing, inspired by glueing and Normalization by Evaluation. Taken together, these two first results demonstrate the robustness of the notion of higher-order regular languages.
• We build a cartesian closed fibration of regular languages of $\lambda$-terms, use that structure to give a higher-order version of Brzozowski derivatives, and explore the question of which $\lambda$-terms admit cocartesian lifts i.e. existential quantifiers in the style of Monadic Second Order logic.
• We introduce the profinite $\lambda$-calculus, an extension of the notion of profinite word to the higher order, and give equivalent descriptions of it through a metric completion, Stone duality and Reynolds parametricity.
• We show that profinite $\lambda$-terms are the morphisms of a Stone-enriched cartesian closed category, which we show has a universal property amounting to a semantic interpretation of the profinite $\lambda$-calculus.
• We introduce the profinite completion of abstract clones. By exhibiting the embedding functors of sets and monoids into clones as parametric right adjoints, we prove that the profinite completion of clone generalizes the profinite completion of monoids and the ultrafilter monad on sets. When applied to a free clone, this completion induces a notion of profinite tree, which we show to coincide with low-order profinite $\lambda$-terms.

The thesis contains work that is joint with my two advisors and Tito Nguyễn.

Vincent Moreau (Jul 02 2025 at 15:23):

Don't hesitate to attend the defence, either online or in person, if you turn out to be in Paris! By the way, I will present at CT2025 parts of the thesis' last chapter about profinite completions of clones.