🔬 Publications

This page is mostly in English. You will find published and unpublished documents, that are related to my research. Some of the documents are in french, and are marked as such. You will find a complete bibtex file with all the information displayed on this page. Furthermore, you can quickly cite a document using the dedicated links, that copies the appropriate LaTeX command to your clipboard.

Preprints

• \(\mathbb{N}\)-polyregular functions arise from well-quasi-orderings

  Aliaume Lopez

  Preprint for Nowhere… yet (2024)

  [arxiv] [bib]

  Abstract

  A fundamental construction in formal language theory is the Myhill-Nerode congruence on words, whose finiteness characterizes regular language. This construction was generalized to functions from finite words to ℤ by Colcombet, Douéneau-Tabot, and Lopez to characterize the class of so-called ℤ-polyregular functions. In this paper, we relax the notion of equivalence relation to quasi-ordering in order to study the class of ℕ-polyregular functions, that plays the role of ℤ-polyregular functions among functions from finite words to ℕ. The analogue of having a finite index is then being a well-quasi-ordering. This provides a canonical object to describe ℕ-polyregular functions, together with a powerful new characterization of this class.

• Labelled Well Quasi Ordered Classes of Bounded Linear Clique Width

  Aliaume Lopez

  Preprint for CSL’25 (2024)

  [arxiv] [bib]

  Abstract

  We provide an algorithm to decide whether a class of finite graphs that has bounded linear clique width is well-quasi-ordered by the induced subgraph relation in the presence of a labelling of the vertices, where the class is given by an MSO-transduction from finite words. This study leverages tools from automata theory, and the proof scheme allows to derive a weak version of the Pouzet conjecture for classes of bounded linear clique-width. We also provide an automata based characterization of which classes of NLC graphs are labelled-well-quasi-ordered by the induced subgraph relation, where we recover the results of Daligault Rao and Thomassé by encoding the models into trees with the gap embedding relation of Dershowitz and Tzameret.

• Commutative N-polyregular functions

  Aliaume Lopez

  Preprint for CSL’25 (2024)

  [arxiv] [bib]

  Abstract

  This paper addresses two questions regarding N-polyregular functions, that forms a proper subset of N-rational series. We show that given a Z-rational series, it is decidable whether it is computable via a commutative N-polyregular function, and provide a counter-example to the theorem of Karhumäki that studied the same question in the case of polynomials. We also prove that it is decidable whether a commutative N-polyregular function is star-free, by proving the stronger statement that star-free Z-polyregular functions that are N-polyregular are in fact computable using a star-free N-polyregular function. Building towards answering the same questions in the non-commutative case, we present a canonical model of computation of N-polyregular functions by generalizing the notion of residual transducers previously introduced in Z-polyregular functions.

• Measuring well quasi-ordered finitary powersets

  Sergio AbriolaSimon HalfonAliaume LopezSylvain SchmitzPhilippe SchnoebelenIsa Vialard

  Preprint for MSCS (2023)

  [arxiv] [bib]

  Abstract

  The complexity of a well-quasi-order (wqo) can be measured through three classical ordinal invariants: the width as a measure of antichains, the height as a measure of chains, and the maximal order type as a measure of bad sequences. This article considers the “finitary powerset” construction: the collection Pf(X) of finite subsets of a wqo X ordered with the Hoare embedding relation remains a wqo. The width, height and maximal order type of Pf(X) cannot be expressed as a function of the invariants of X, and we provide tight upper and lower bounds for the three invariants. The article also identifies an algebra of well-behaved wqos, that include finitary powersets as well as other more classical constructions, and for which the ordinal invariants can be computed compositionnally. This relies on a new ordinal invariant called the approximated maximal order type.

• Infinitary Noetherian Constructions II. Transfinite Words and the Regular Subword Topology

  Jean Goubault-LarrecqSimon HalfonAliaume Lopez

  Preprint for Colloquium Mathematicum (2022)

  [arxiv] [bib]

  Abstract

  We show that the spaces of transfinite words, namely ordinal-indexed words, over a Noetherian space, is also Noetherian, under a natural topology which we call the regular subword topology. We characterize its sobrification and its specialization ordering, and we give an upper bound on its dimension and on its stature.

Talks

• Which polynomials are computed by N-weighted automata?

  Aliaume Lopez

  Talk at INRIA Lille (2024)

  [slides] [bib]

  Abstract

  Given a semiring K, the notion of K-weighted automata generalizes regular languages to functions from Σ* to K. This model allows us to compute (multivariate) polynomial functions with coefficients in K. We provide a decidable characterization of polynomials with coefficients in Q that can be computed by K-weighted automata for K = (N,+,×) and for K = (Z+,×). As a consequence, we can decide which functions computed by Z-weighted automata are computed by N-weighted automata, under the assumption of commutativity (the order of the letters in the input does not matter) and polynomial growth (the output of the function is bounded by a polynomial in the size of the input). This surprisingly allows us to decide whether such functions are star-free, a notion borrowed from the theory of regular languages.

• Which polynomials are computed by N-weighted automata?

  Aliaume Lopez

  Talk at Marseille (2024)

  [slides] [bib]

  Abstract

  Given a semiring K, the notion of K-weighted automata generalises regular languages to functions from Σ* to K. This model allows us to compute (multivariate) polynomial functions with coefficients in K. We provide a decidable characterisation of polynomials with coefficients in Q that can be computed by K-weighted automata for K = (N,+,×) and for K = (Z+,×). As a consequence, we can decide which functions computed by Z-weighted automata are computed by N-weighted automata, under the assumption of commutativity (the order of the letters in the input does not matter) and polynomial growth (the output of the function is bounded by a polynomial in the size of the input). This surprisingly allows us to decide whether such functions are star-free, a notion borrowed from the theory of regular languages.

• Well-quasi-ordered classes of bounded (linear) clique-width: an automata based approach

  Aliaume Lopez

  Talk at Montpellier (2024)

  [slides] [bib]

  Abstract

  A class of graphs is (labelled) well-quasi-ordered (WQO) whenever any infinite subset of this class contains two (labelled) graphs G and H such that G is an induced subgraph of H respecting the labeling. We provide an algorithm to decide whether a class of finite graphs that has bounded linear clique width is labelled WQO, where the class is given by an MSO-transduction from finite words. This study leverages tools from automata theory, and as a byproduct we answer positively to a conjecture of Pouzet: for such classes of graphs, being WQO using finitely many labels is equivalent to being WQO with infinite sets of labels. We also provide an automata based characterization of earlier results of Daligault, Rao and Thomassé [10.1007/s11083-010-9174-0, Theorem 3] by encoding the models into trees ordered with the gap embedding relation of Dershowitz and Tzameret. This work is available on arxiv: https://arxiv.org/abs/2405.10894.

• Well-quasi-ordered classes of bounded (linear) clique-width: an automata based approach

  Aliaume Lopez

  Talk at Bordeaux (2024)

  [slides] [bib]

  Abstract

  A class of graphs is (labelled) well-quasi-ordered (WQO) whenever any infinite subset of this class contains two (labelled) graphs G and H such that G is an induced subgraph of H respecting the labeling. We provide an algorithm to decide whether a class of finite graphs that has bounded linear clique width is labelled WQO, where the class is given by an MSO-transduction from finite words. This study leverages tools from automata theory, and as a byproduct we answer positively to a conjecture of Pouzet: for such classes of graphs, being WQO using finitely many labels is equivalent to being WQO with infinite sets of labels. We also provide an automata based characterization of earlier results of Daligault, Rao and Thomassé [10.1007/s11083-010-9174-0, Theorem 3] by encoding the models into trees ordered with the gap embedding relation of Dershowitz and Tzameret. This work is available on arxiv: https://arxiv.org/abs/2405.10894.

• Labelled Well Quasi Ordered Classes of Bounded Linear Clique-Width

  Aliaume Lopez

  Talk at Highlights (2024)

  [slides] [bib]

  Abstract

  We provide an algorithm to decide whether a class of finite graphs that has bounded linear clique width is well-quasi-ordered by the induced subgraph relation in the presence of a labelling of the vertices, where the class is given by an MSO-transduction from finite words. This study leverages tools from automata theory, and the proof scheme allows to derive a weak version of the Pouzet conjecture for classes of bounded linear clique-width.

• Z-Polyregular functions

  Aliaume Lopez

  Talk at the MOVE seminar of LIS (2023)

  [slides] [bib]

  Abstract

  Regular languages over finite words are defined equivalently in terms of restrictions of Turing Machines (finite deterministic automata, and the numerous equivalent automata models that are equi-expressive in this context), syntactic presentations (regular expressions), algebraic descriptions (recognisability by finite monoids), and logical specifications (via sentences in monadic second order logic). In this talk, we propose a generalisation of regular languages, i.e. functions from Σ* to Booleans, to functions from Σ* to integers, which we call Z-polyregular functions. This class shares many similarities with regular languages, both in terms of definitions, and in terms of decidability properties. We identify Z-polyregular functions as a subclass of other existing computational models, each time with appealing characterisations. Our main result is that one can decide whether Z-polyregular functions are star-free (aperiodic), whose proof relies on two beautiful ingredients: the construction of a residual transducer, and a semantic characterisation of aperiodicity for functions that is based on multivariate polynomials. This is a joint work with Gaëtan Douéneau-Tabot and Thomas Colcombet.

• Compositional Techniques for Preservation Theorems over Classes of Finite Structures

  Aliaume Lopez

  Talk at the BOREAL seminar of LIRMM (2023)

  [url] [slides] [bib]

  Abstract

  Preservation theorems connect syntactic fragments of first-order logic to corresponding “semantic” properties. For instance, the fragment of unions of conjunctive queries is characterized as the fragment of (first-order) queries that are “preserved under homomorphisms”, that is, if A is satisfies the query, and there is a homomorphism from A to B, then B also satisfies the query: this is known as the Homomorphism Presrevation Theorem. As an example of application of such theorems, the homomorphism preservation theorem has been used to characterize the termination of the “Core Chase Algorithm” by Deutsch, Nash and Remmel in 2008. Preservation theorems date back to the 1950s, but the classical proofs of these result are done in the framing of Model Theory and rely heavily on the compactness theorem of first order logic. When restricting our attention to classes of finite structures (which model finite databases), the status of the preservation theorems have been investigated in the past years, with positive and negative results on different classes of finite structures, often with carefully built ad-hoc proofs. The goal of this talk is to recall the landscape of preservation theorems in the finite, and propose a compositional approach to constructing classes of structures over which preservation theorems can be guaranteed.

• The Łos-Tarski theorem and locality

  Aliaume Lopez

  Talk at the automata seminar of MIMUW (2023)

  [bib]

  Abstract

  We consider first order sentences over a finite relational signature σ. Classical preservation theorems, dating back to the 1950s, state the correspondence between syntactic fragments of FO[σ], and semantic ones. The archetypal example of such preservation theorem is the Łoś–Tarski Theorem, that states the correspondence between the syntactic fragment of existential sentences, and the semantic fragment of sentences preserved under extensions. As its proof heavily relies on the compactness of first order logic, it is a priori unclear whether Łoś–Tarski Theorem relativizes to classes of finite structures. Tait has proven in 1959 that the theorem does not relativize to the class Fin[σ] of all finite structures, but it was proven by Atserias, Dawar, and Grohe that the Łoś–Tarski Theorem relativizes to hereditary classes of finite structures that have bounded degree, and are closed under disjoint unions. In this talk, we provide a full characterization of classes of hereditary classes finite structures that are closed under disjoint unions for which the Łoś–Tarski Theorem relativizes. This result follows form the study of the existential-local fragment of first order logic, that corresponds to a positive variant of the Gaifman normal form, and is itself subject to a preservation theorem.

• Preservation theorems and locality of first order logic

  Aliaume Lopez

  Talk at the M2F seminar of LaBRI (2023)

  [slides] [bib]

  Abstract

  In this talk, we will investigate the tight connection between the locality properties of first-order logic, and the relativisation (or lack thereof) of the Łós-Tarski Theorem to classes of structures. Starting with a gentle introduction to preservation theorems, we will then focus on two particular classes of sentences: existential formulas, and existential local formulas. We prove that existential local sentences are exactly those that can be rewritten in a positive variant of the Gaifman normal form, and can be characterized semantically as sentences that are preserved under local elementary embeddings. As expected, this semantic characterization fails in the finite. Quite surprisingly though, we can leverage this class of sentences to prove the following locality property for classes of finite structures: the Łós-Tarski Theorem relativises to a class C of finite structures if and only if the Łós-Tarski Theorem locally relativises to the class C, provided that the class C is hereditary and closed under disjoint unions. As a consequence of this result, we not only obtain new proofs of relativisation of Łós-Tarski Theorem, but also provide new classes where this relativisation holds.

• Generic Noetherian Theorems - Defining Noetherian Topologies Through Iterations

  Aliaume Lopez

  Talk at the BRAVAS team seminar (2022)

  [slides] [bib]

  Abstract

  The goal of this talk is to provide a canonical way to construct Noetherian topologies as least fixed points. This is done by proving a least fixed point theorem, that extends the work of Hasegawa on well-quasi-orderings to Noetherian spaces. This extension allows us to justify previously introduced Noetherian topologies, and construct new Noetherian spaces. Finally, note that we can apply our result to spaces that are not inductively defined, provided that the topology/ordering is inductively defined, which is a limitation in Hasegawa’s approach.

• Locality and Preservation Theorems

  Aliaume Lopez

  Talk at the GT DAAL (2022)

  [slides] [see] [bib]

  Abstract

  This talk is a brief introduction to the relationship between locality based techniques and preservation theorems in finite model theory.

• Rejoindre l’administration publique avec un doctorat - Comment et pourquoi ?

  Aliaume LopezGaëtan Douéneau-Tabot

  Talk at the ENS Paris-Saclay student seminar (2022)

  [slides] [bib]

  Abstract

  Les présentations de l’ENS décrivent souvent une formation « par la recherche, pour la recherche », selon la formule consacrée. Ainsi, une grande majorité des normaliens commencent leur parcours professionnel par un doctorat (c’est le cas d’environ 80% des élèves du département informatique). Néanmoins, seuls 50% des docteurs diplômés en France rejoignent finalement les métiers de la recherche et de l’enseignement publics. Cela contraste avec les débouchés usuellement présentés aux normaliens, centrés sur les postes permanents de maîtres de conférences, chargés de recherche ou professeurs agrégés. Parmi les docteurs, on compte également 30% de débouchés dans le secteur privé ou l’entreprenariat. Notre objectif est de discuter des 20% restants, qui choisissent de rejoindre le secteur public hors du monde académique, autrement dit les administrations publiques. Les voies d’accès de la fonction publique aux jeunes docteurs sont nombreuses,qu’il s’agisse de recrutements sur concours ou en tant que contractuels (CDD ou CDI), à des postes de managers ou d’experts techniques. L’objectif de ce séminaire est de présenter les postes et les recrutements dans l’administration, ainsi que quelques parcours de normaliens l’ayant rejointe.

• Basic Operational Preorders for Algebraic Effects - With a pinch of non-determinism and probabilities

  Aliaume Lopez

  Talk at the PPS Seminar at IRIF (2021)

  [slides] [bib]

  Abstract

  The “generic operational metatheory” of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.

• Preservation theorems - At the crossroads of topology and logics

  Aliaume Lopez

  Talk at the ASV Seminar of IRIF (2021)

  [slides] [see] [bib]

  Abstract

  In this talk, we introduce a family of topological spaces that captures the existence of preservation theorems. The structure of those spaces allows us to study the relativisation of preservation theorems under suitable definitions of surjective morphisms, subclasses, sums, products, topological closures, and projective limits. Throughout the talk, we also integrate already known results into this new framework and show how it captures the essence of their proofs.

Conference Publications

• \(\mathbb{Z}\)-polyregular functions

  Thomas ColcombetGaëtan Douéneau-TabotAliaume Lopez

  Published at LICS’23 (2023)

  [doi] [url] [arxiv] [pdf] [slides] [video] [bib]

  Abstract

  This paper studies a robust class of functions from finite words to integers that we call ℤ-polyregular functions. We show that it admits natural characterizations in terms of logics, ℤ-rational expressions, ℤ-rational series and transducers.We then study two subclass membership problems. First, we show that the asymptotic growth rate of a function is computable, and corresponds to the minimal number of variables required to represent it using logical formulas. Second, we show that first-order definability of ℤ-polyregular functions is decidable. To show the latter, we introduce an original notion of residual transducer, and provide a semantic characterization based on aperiodicity.

• Fixed Points and Noetherian Topologies

  Aliaume Lopez

  Published at FoSSACS’23 (2023)

  [doi] [url] [arxiv] [pdf] [slides] [bib]

  Abstract

  Noetherian spaces are a generalisation of well-quasi-orderings to topologies, that can be used to prove termination of programs. They find applications in the verification of transition systems, some of which are better described using topology. The goal of this paper is to allow the systematic description of computations using inductively defined datatypes via Noetherian spaces. This is achieved through a fixed point theorem based on a topological minimal bad sequence argument.

• When Locality Meets Preservation

  Aliaume Lopez

  Published at LICS’22 (2022)

  [doi] [url] [arxiv] [pdf] [slides] [bib]

  Abstract

  This paper investigates the expressiveness of a fragment of first-order sentences in Gaifman normal form, namely the positive Boolean combinations of basic local sentences. We show that they match exactly the first-order sentences preserved under local elementary embeddings, thus providing a new general preservation theorem and extending the Łós-Tarski Theorem. This full preservation result fails as usual in the finite, and we show furthermore that the naturally related decision problems are undecidable. In the more restricted case of preservation under extensions, it nevertheless yields new well-behaved classes of finite structures: we show that preservation under extensions holds if and only if it holds locally.

• Preservation Theorems Through the Lens of Topology

  Aliaume Lopez

  Published at CSL’21 (2021)

  [doi] [arxiv] [pdf] [slides] [bib]

  Abstract

  In this paper, we introduce a family of topological spaces that captures the existence of preservation theorems. The structure of those spaces allows us to study the relativisation of preservation theorems under suitable definitions of surjective morphisms, subclasses, sums, products, topological closures, and projective limits. Throughout the paper, we also integrate already known results into this new framework and show how it captures the essence of their proofs.

• Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular

  Aliaume LopezAlex Simpson

  Published at CSL’18 (2018)

  [doi] [url] [pdf] [slides] [bib]

  Abstract

  The “generic operational metatheory” of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.

• Diagrammatic Semantics for Digital Circuits

  Dan R. GhicaAchim JungAliaume Lopez

  Published at CSL’17 (2017)

  [doi] [url] [arxiv] [bib]

  Abstract

  We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about parametrised circuits, with a potentially interesting new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is producing a general yet simple graph-rewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications.

• A structural and nominal syntax for diagrams

  Dan R. GhicaAliaume Lopez

  Published at QPL (2017)

  [doi] [url] [arxiv] [bib]

  Abstract

  The correspondence between monoidal categories and graphical languages of diagrams has been studied extensively, leading to applications in quantum computing and communication, systems theory, circuit design and more. From the categorical perspective, diagrams can be specified using (name-free) combinators which enjoy elegant equational properties. However, conventional notations for diagrammatic structures, such as hardware description languages (VHDL, Verilog) or graph languages (Dot), use a different style, which is flat, relational, and reliant on extensive use of names (labels). Such languages are not known to enjoy nice syntactic equational properties. However, since they make it relatively easy to specify (and modify) arbitrary diagrammatic structures they are more popular than the combinator style. In this paper we show how the two approaches to diagram syntax can be reconciled and unified in a way that does not change the semantics and the existing equational theory. Additionally, we give sound and complete equational theories for the combined syntax.

Journal Publications

Reports

• Generic Operational Metatheory

  Aliaume Lopez

  Report for ENS Cachan (2017)

  [url] [pdf] [slides] [bib]

  Abstract

  The goal of this internship was to give a systematic study of contextual equivalence in the presence of algebraic effects in a uniform, compact and syntactic way, in the continuation of preexisting work. To reach this objective, we extended a call-by-value PCF with a signature of algebraic effects, and gave an abstract equality between the contextual equivalence for this language and a usable logical relation, independently of the signature itself. Generic meta theorems were then proven using this abstract equivalence. To justify the usefulness of this approach, a direct link with denotational semantics and the work of Plotkin and Power was developed, and signature of mixed non-determinism and probabilities was studied in-depth.

• Une syntaxe améliorée pour la description de circuits digitaux

  Aliaume Lopez

  Report for ENS Cachan (2016)

  [url] [pdf] [slides] [bib]

  Abstract

  \(\emptyset\)

Blog Posts

• On the word topology, and beyond

  Jean Goubault-LarrecqAliaume Lopez

  BlogPost in Jean Goubault-Larrecq’s blog (2020)

  [url] [bib]

  Abstract

  Given a quasi-ordered set \((X, ≤)\), the set of finite words over \(X\) is built as \(X^* = ⋃_{0 \leq k < \infty} X_k\). This set can be equipped with many different quasi-orders, but it appears that often the right notion is the one relying on subwords, that is, a word \(w\) is smaller than a word \(w'\) if there exists a map \(h\colon |w|\to|w'|\) such that \(\forall 1 \leq k \leq |w|, w_k \leq w_{h(k)}'\). This order is called the subword ordering. This blog posts explores how one can recover this ordering by looking at functions that decompose words (\(\operatorname{split} \colon X^* \to \mathcal{P}(X^* \times X^*)\)), rather than considering their inductive constructors (\(\operatorname{concat} \colon X^* \times X^* \to X^*\)).