Confluences cubiques et formalisation des catégories cubiques

par M. Tanguy Massacrier

vendredi 12 déc. 2025, 14:00 → 16:00 Europe/Paris

Salle Fokko du Cloux - Bât. Braconnier

Le jury sera composé de :
- M. Xavier Urbain, Université Claude Bernard Lyon 1,
- Mme Fida El Chami, Université Libanaise,
- Mme Sophie Morel, ENS de Lyon,
- M. Femke van Raamsdonk, Vrije Universiteit Amsterdam,
- Mme Florence Fauquant-Millet, Université Jean Monnet,
- M. Jean Goubault-Larrecq, ENS Paris-Saclay, rapporteur,
- M. Nicolai Kraus, Nottingham University, rapporteur,
- M. Philippe Malbos, Université Claude Bernard Lyon 1, directeur de thèse,
- M. Georg Struth, Sheffield University, codirecteur de thèse.


Résumé :
Cette thèse s’inscrit dans un programme de recherche sur la formalisation de la réécriture. Nous étudions la propriété de confluence, qui garantit que deux réécritures sur une même expression peuvent être prolongées par d’autres chemins de réécriture conduisant à une expression commune. Cette propriété fondamentale de la réécriture a été exprimée dans différents langages : diagrammes, inclusions de relations, algèbres de Kleene, catégories globulaires et cubiques. Cette thèse étudie la formalisation de cette propriété d’un point de vue cubique. Les schémas de confluence de branchements de deux réécritures sont par définition carrés et ceux de k-branchements forment des k-cubes. Cela suggère une formulation naturelle des preuves de confluence dans le langage des catégories et polygraphes cubiques. Dans cette thèse, nous introduisons un cadre permettant d’étudier les preuves de confluence comme des constructions cubiques et d’en déduire des formalisations cubiques à un seul ensemble.
Nous explicitons la notion de contraction cubique permettant de démontrer l’acyclicité des (ω,0)-catégories cubiques. Nous montrons comment construire des contractions cubiques à partir de systèmes de réécriture abstraits confluents et terminants. Nous donnons ainsi une construction explicite de résolution polygraphique cubique constituée en toute dimension par les formes cubiques des confluences des multiples branchements. Nous formulons les schémas de preuves de confluence à la Newman et Church-Rosser dans ce langage polygraphique. Nous introduisons les catégories cubiques à un seul ensemble, dites single-set, qui axiomatisent les catégories cubiques en définissant la dimension des cellules par des équations de point fixe. L’axiomatisation à un seul ensemble est bien adaptée à une formalisation dans l’assistant de preuve Isabelle/HOL. Nous formalisons les ω-catégories cubiques à un seul ensemble dans Isabelle/HOL. Enfin, nous formalisons le concept de système de réécriture dans les ω-catégories globulaires polygraphiables à un seul ensemble, qui correspondent aux ω-catégories globulaires librement engendrées par des ω-polygraphes. Nous les caractérisons comme les objets cofibrants de la structure de modèle folk transférée et nous les formalisons dans Isabelle/HOL.