“Ma thèse s’intéresse aux théorèmes de préservation en logique du premier ordre sur des classes de modèles finis. Derrière ces mots clefs se cachent l’histoire d’un passage de l’infini mathématique au fini de l’informatique, plus précisément de la “Théorie des Modèles” (une branche de la logique) vers la “Théorie des Modèles Finis”. Le fait de ne pas considérer des modèles infinis intervient naturellement en informatique, par exemple lorsqu’on interprète des bases de données comme des structures mathématiques. Les théorèmes de préservation sont un exemple archétypique de la difficulté de ce passage de l’infini au fini. En effet, ce sont des résultats fondamentaux, simples, et bien compris de la théorie des modèles classiques, pour lesquels la transcription dans le cadre des modèles finis a posé et pose encore des questions profondes.” Aliaume Lopez, ancien doctorant.
Lien de sa thèse : Théorèmes de Préservation

Je m’appelle Aliaume Lopez. J’ai fait partie des générations de bacheliers qui pouvaient choisir l’informatique en option, et après une classe préparatoire à Montpellier, j’ai intégré l’ENS Paris-Saclay en 2015 (c’était alors l’ENS Cachan). En 2018 j’ai obtenu l’agrégation de mathématiques option informatique, option qui a disparu au profit de la nouvelle agrégation d’informatique. J’ai suivi le M2 du MPRI, le Master Parisien de Recherche en Informatique, durant lequel j’ai eu mon second contact avec la théorie des beaux préordres dans le cours éponyme, à l’époque donné par Jean Goubault-Larrecq et Philippe Schnoebelen. J’ai continué mon parcours en faisant une thèse en co-encadrement, avec Sylvain Schmitz à l’IRIF et Jean Goubault-Larrecq au LMF.

Je suis intéressé par l’informatique “pratique” depuis très jeune : j’ai commencé par mettre des thèmes sur Windows XP, puis j’ai installé une première fois Ubuntu afin de bénéficier de tous les “effets cools” que proposaient Compiz à l’époque. En effet, quoi de plus important pour un ordinateur que d’avoir des fenêtres qui prennent feu ? De fil en aiguille, j’ai migré de consommateur de programmes à assembleur de programmes, puis à développeur dans une moindre mesure (il faut remercier le site du zéro, qui faisait un travail remarquable à l’époque). Cependant, mon penchant pour la recherche provient curieusement d’un autre domaine, à savoir, les mathématiques. Bien sûr, à l’IRIF, tout le monde sait que preuves et programmes sont deux facettes d’un même objet conceptuel, mais c’est probablement plus flou pour un lycéen. L’informatique était alors teintée d’une aura de “bidouille”, à l’opposé des mathématiques qui semblaient reposer sur une théorie solide.

Je suis entré à l’ENS Paris-Saclay dans le département d’informatique, et c’est lors de ma première année que j’ai vraiment découvert la recherche en informatique théorique. Le dernier coup de pouce en direction des théorèmes de préservation a été un stage de M2 sous la co-direction de Jean Goubault-Larrecq et Sylvain Schmitz, durant lequel j’ai tenté d’appliquer des méthodes provenant des beaux préordres à l’étude de systèmes possédant une base de donnée. Il se trouve que les beaux préordres ne trouvent pas (à ce jour) d’application probante, mais qu’une notion proche, celle de théorème de préservation semblait prometteuse. Sans le savoir, j’étais tombé dans la théorie des modèles finis, à vouloir “remplacer” le théorème de compacité par des arguments combinatoires, garantissant la terminaison de certains processus. L’objet d’étude a donc évolué, passant de la vérification des systèmes avec une base de données à l’étude des théorèmes de préservation, qui une question reste assez riche et intéressante pour y passer trois années bien remplies.

Un théorème de préservation, c’est un théorème qui fait le lien entre une propriété syntaxique de certaines questions (comment la question est écrite, sa grammaire, les mots utilisés) et une propriété sémantique de certaines questions (le sens de la question).

Par exemple, certaines questions ne contiennent pas le quantificateur universel “pour tout” : c’est une propriété syntaxique. Ainsi, la question “Est-ce que toutes les voitures sont vertes ?” contient un quantificateur universel, alors que la question “Est-ce qu’il existe une voiture verte ?” n’en contient pas.

Certaines questions sont intéressantes d’un point de vue informatique parce qu’on peut y répondre dès qu’un exemple positif est trouvé. Ainsi, on peut répondre à la question “est-ce qu’il existe une voiture verte ?” dès lors qu’on a trouvé une voiture verte, sans avoir à regarder toutes les voitures du monde. Reformulé autrement, cela veut dire que lorsqu’on a découvert une sous partie du monde où la réponse à la question est positive, alors la réponse est positive “partout” : si on a trouvé une voiture verte au sein des voitures que l’on a observées, alors il existe une voiture verte au sein de l’ensemble des voitures du monde.

Le théorème de Los-Tarski est un théorème de préservation qui énonce l’équivalence entre les deux propriétés ci-dessus. C’est-à-dire, pour une question q, les deux propriétés suivantes sont équivalentes :

• Si l’on sait que q est vraie sur une partie de notre monde, alors q est vraie “partout” (q est croissante).
• On peut écrire la question q sans utiliser le quantificateur universel “pour tout”.

C’est ce théorème qui explique pourquoi les deux exemples ci-dessus étaient les mêmes : il n’est en réalité pas possible de trouver un exemple de question “croissante” qui ne peut pas s’écrire sans utiliser “pour tout”. Il existe plusieurs théorèmes de préservation, tout simplement parce que l’on peut imaginer d’autres fragments (par exemple, interdire d’utiliser la négation dans nos questions).

Dans le dessin ci-contre, on représente les structures relationnelles (mondes possibles) par des points, et la relation d’extension par des flèches. En fixant une formule close q (une question), on peut vérifier sur chaque structure si la formule est satisfaite (en vert) ou non-satisfaite (en rouge). Une formule est préservée par extensions (croissante) si, pour tout point coché en vert, le cône bleuté de ses extensions est lui aussi composé de points cochés en vert. Sur cet exemple, la formule n’est pas préservée par extensions.

Une des questions principales de ma thèse vient du problème suivant : le théorème de Los-Tarski a été originellement démontré d’un point de vue de mathématicien. Or, en informatique (par exemple pour modéliser des bases de données), il y a souvent une hypothèse naturelle sur les données traitées : elles sont de taille finie (c’est-à-dire, représentables sur une machine). Là où le bât blesse, c’est que, contrairement à ce que l’on pourrait penser, se limiter à l’étude des structures finies n’est pas un simple cas particulier, et fait apparaître des phénomènes nouveaux. Ainsi, on distingue la théorie des modèles (le cadre classique, étudié par les mathématiciens) de la théorie des modèles finis, qui est plus adaptée à l’informatique. Les différences entre ces deux domaines sont profondes, et un exemple est précisément le statut des théorèmes de préservation : une majorité de ces théorèmes ne sont pas transposables dans le cadre fini, à l’exception notable du théorème de préservation par homomorphisme, dont le statut était resté ouvert pendant plus de 20 ans.

On peut croire que l’étude de ces théorèmes est donc close. Cependant, lorsqu’on travaille sur des modèles en informatique, on peut souvent présupposer qu’ils possèdent une certaine structure (en plus d’être finis). Par exemple, si nos structures doivent représenter un réseau routier, on peut raisonnablement poser une limite sur le nombre de routes qui se croisent à une intersection donnée (par exemple, 10 semble plus que suffisant dans notre exemple). Cette restriction supplémentaire (et en réalité, chaque nouvelle hypothèse) remet en jeu le statut des théorèmes de préservation. 1 Le cœur de ma thèse est l’étude des classes de structures finies sur lesquelles certains théorèmes de préservation peuvent se transposer. C’est un problème non trivial, qui porte le double intérêt suivant :

1. Cela fournit, d’un point de vue théorique, une manière de mieux comprendre les classes de structures qui sont “agréables” d’un point de vue de la théorie des modèles finis, en développant des outils pour comprendre la manière dont la logique se comporte sur ces classes de structures.
2. Cela fournit, d’un point de vue plus pratique, une boite à outil qui systématise l’étude des théorèmes de préservation. En particulier, l’objectif a été de comprendre comment permettre de composer des théorèmes de préservation.

Sur cette image, on observe un graphe (au dessus) qui semble complexe car très dense. Cependant, il est en réalité obtenu comme la composition d’un ordre total (en dessous) avec des chemins finis. Ainsi, les théorèmes de préservation sur la classe de ces graphes se réduisent à l’étude de la classe des chemins finis et des ordres totaux, qui sont beaucoup plus simples.

Mon sujet de thèse est particulièrement théorique et ne possède aucune application en informatique “concrète”. Cependant, les théorèmes développés parlent de structures et de problèmes qui sont récurrent en théorie des bases de données. Il est possible que ces résultats (ou leurs preuves) puissent s’adapter à des questions plus pratiques dans un futur proche.

À l’ASN, j’ai travaillé en tant que développeur fullstack sur une application visant à consolider les données de cette autorité de contrôle pour permettre la recherche, la création de statistiques, et la préparation des inspections de l’Autorité de Sûreté Nucléaire. Cela n’a pas eu un impact particulier sur ma recherche, mais cela m’a convaincu de la nécessité de l’étude théorique des systèmes faisant évoluer une base de données.

Je commence un postdoc à l’Université de Varsovie sous la direction de Mikołaj Bojańczyk en octobre. Après ce postdoc, je voudrais obtenir un poste permanent en France.