💻 computer science

A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism

Cet article présente une caractérisation algébrique généralisée de deux variantes de la théorie des types avec polymorphisme universel explicite en les définissant comme des modèles initiaux de théories algébriques généralisées, offrant ainsi une abstraction structurelle qui éclaire la conjecture d'initialité de Voevodsky.

Auteurs originaux : Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó

Publié 2026-03-05

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Le Grand Projet : Construire des Univers de Logique

Imaginez que les mathématiques et l'informatique sont comme des villes immenses construites avec des règles très strictes. Ces villes, on les appelle des "théories des types". Elles servent à vérifier que nos programmes informatiques ne font pas d'erreurs et que nos preuves mathématiques sont solides.

Mais construire ces villes est difficile. Souvent, les architectes (les chercheurs) se perdent dans les détails : la forme exacte des briques, la couleur du mortier, les règles de grammaire pour écrire les plans. Parfois, on oublie l'essentiel : comment la ville est structurée dans son ensemble.

C'est le but de ce papier : au lieu de regarder chaque brique individuellement, les auteurs (Marc Bezem, Thierry Coquand et leurs collègues) veulent nous donner une vue d'ensemble, une "carte maîtresse" qui décrit la structure fondamentale de ces villes logiques.

Les Deux Outils Magiques

Pour y parvenir, ils utilisent deux outils spéciaux qu'ils ont développés ensemble :

Les "GATs" (Théories Algébriques Généralisées) :
Imaginez que vous voulez décrire comment construire un meuble. Au lieu de donner une liste interminable de vis, de clous et de planches, vous donnez un plan de montage abstrait. Ce plan dit : "Il faut un pied, une assise, et un dossier, et ils doivent s'assembler ainsi". Peu importe si le meuble est en chêne ou en plastique, la structure reste la même. Les GATs sont ces plans de montage pour la logique. Ils ignorent les détails de grammaire pour se concentrer sur la forme pure.
Les "CWFs" (Catégories avec Familles) :
C'est le terrain de jeu où ces meubles sont construits. C'est un espace mathématique qui permet de gérer les contextes (par exemple : "si je sais que X est un nombre, alors Y est une liste"). C'est le sol sur lequel on pose les règles.

Le Défi des "Univers" (Les Étagères Infinies)

Le problème principal que le papier aborde concerne les univers.
Imaginez une bibliothèque.

Il y a des livres (les types).
Il y a des étagères pour ranger les livres (les univers).
Mais une étagère ne peut pas contenir une autre étagère identique à elle-même (sinon, on tombe dans un paradoxe, comme un miroir qui reflète un miroir à l'infini).

Dans les théories classiques, on a souvent une tour d'étagères fixe : Étagère 1, Étagère 2, Étagère 3... C'est ce qu'on appelle une "tour externe". C'est simple, mais un peu rigide.

Les auteurs proposent une version plus flexible : la polymorphie explicite des univers.
Imaginez que chaque étagère a un numéro de niveau (comme un étage dans un gratte-ciel).

Au lieu de dire "C'est l'étagère 5", on dit "C'est l'étagère de niveau l".
Et le génie de ce papier, c'est qu'on peut maintenant construire des étagères qui s'adaptent dynamiquement. Si vous avez une étagère de niveau l, vous pouvez créer une nouvelle étagère qui contient toutes les étagères de niveau inférieur à l. C'est comme si l'architecture du bâtiment pouvait se réorganiser elle-même selon les besoins.

L'Analogie de la "Boîte à Outils Universelle"

Pour expliquer leur méthode, les auteurs disent :

"Au lieu de construire une maison brique par brique (règle par règle), nous allons définir une boîte à outils universelle (le GAT) qui contient les instructions pour construire n'importe quelle maison de ce type."

L'Approche "Tour Externe" (Section 2) :
Ils montrent d'abord comment décrire une ville avec une tour d'étagères fixe. C'est comme un plan d'architecte pour un immeuble où chaque étage est prédéfini. C'est solide, mais un peu rigide.
L'Approche "Polymorphie Explicite" (Section 3) :
Ensuite, ils montrent comment décrire une ville où les étages sont dynamiques. Ils ajoutent une nouvelle règle : "Si vous avez un niveau l, vous pouvez créer un niveau l+1 ou fusionner deux niveaux".
C'est comme si les architectes avaient inventé un nouveau type de brique qui peut changer de taille selon l'endroit où on la pose.

Pourquoi est-ce important ? (Le Projet de Voevodsky)

Le papier mentionne un grand rêve du mathématicien Vladimir Voevodsky : La Conjecture d'Initialité.
Imaginez que vous voulez prouver que deux architectes différents, qui ont construit deux villes différentes avec des règles légèrement différentes, ont en fait construit la même ville au fond.

Si on regarde les briques (la syntaxe), les villes semblent différentes.
Mais si on regarde la structure fondamentale (le GAT), on peut prouver qu'elles sont identiques.

Ce papier est une étape cruciale pour prouver cela. Il dit : "Regardez, peu importe comment vous écrivez les règles (la grammaire), si vous utilisez notre 'plan de montage' (le GAT), vous obtiendrez toujours la même structure mathématique fondamentale."

En Résumé

Ce papier est une boîte à outils de haute précision pour les architectes de la logique.

Il remplace les listes interminables de règles par des plans abstraits (GATs).
Il gère la complexité des niveaux d'étagères (univers) de manière flexible.
Il permet de prouver que différentes façons de construire la logique mènent au même résultat fondamental.

C'est une façon de dire : "Ne vous perdez pas dans les détails de la peinture des murs. Concentrez-vous sur la structure de l'immeuble, car c'est là que réside la vérité mathématique."

C'est une contribution majeure pour rendre les mathématiques et l'informatique plus robustes, plus claires et plus faciles à vérifier par des machines.

1. Problématique

Le papier aborde la difficulté de donner une caractérisation mathématique abstraite et uniforme des systèmes de types dépendants, en particulier ceux dotés de polymorphisme universel explicite.

Le défi de la syntaxe : Les présentations traditionnelles des théories des types reposent sur des grammaires et des règles d'inférence. Cette approche est lourde, dépendante de choix syntaxiques arbitraires (gestion des substitutions, règles d'égalité, etc.) et rend difficile la preuve de l'équivalence entre différentes formulations ou la construction de modèles initiaux rigoureux.
Le projet de Voevodsky : L'article s'inscrit dans le cadre du projet de l'« Initialité Conjecture » de Vladimir Voevodsky, qui vise à définir une classe générale de théories des types dépendants et à prouver que leur modèle de termes est un objet initial dans une catégorie de modèles appropriée.
Spécificité du polymorphisme : Les auteurs se concentrent sur deux variantes de la théorie des types de Martin-Löf :
1. Une théorie avec une tour externe d'univers ( $TT_{tower}$ ), où les niveaux d'univers sont des entiers naturels externes.
2. Une théorie avec polymorphisme universel explicite ( $TT_{up}$ ), où les niveaux d'univers sont des variables de niveau internes au système, permettant des produits indexés par les niveaux et des contraintes d'égalité entre niveaux.

2. Méthodologie

Les auteurs utilisent une approche basée sur la logique catégorique, en remplaçant les systèmes déductifs traditionnels par des notions algébriques plus régulières : les Théories Algébriques Généralisées (GATs) et les Catégories avec Familles (CwF).

Théories Algébriques Généralisées (GATs) : Introduites par Cartmell, les GATs généralisent les théories algébriques multi-sortes en permettant aux symboles d'opérateurs et de sorts d'avoir des types dépendants. Elles capturent la structure catégorique essentielle sans les détails syntaxiques superflus.
Catégories avec Familles (CwF) : Les CwF sont des modèles sémantiques des règles de base de la théorie des types (formation de contextes, morphismes de contextes, substitution, etc.).
Stratégie de construction :
1. Définir une GAT spécifique ( $\Sigma$ ) qui encode la structure de la théorie des types visée (types, termes, règles de substitution, formateurs de types, univers).
2. Prouver que la catégorie des modèles de cette GAT possède un objet initial (le modèle de termes $T_\Sigma$ ).
3. Montrer que ce modèle initial est isomorphe à la théorie des types syntaxique (avec substitution implicite ou explicite), validant ainsi la caractérisation abstraite.

3. Contributions Clés

L'article présente deux constructions principales de GATs :

A. La théorie avec une tour externe d'univers ( $\Sigma_{tower}$ )

Structure : Il s'agit d'une GAT infinitaire (car elle contient une infinité de symboles d'opérateurs pour une infinité d'univers $U_l$ indexés par $l \in \mathbb{N}$ ).
Composantes :
- Une CwF de base avec les formateurs de types standards ( $\Pi, \Sigma, N, W, Id$ , etc.).
- Une tour d'univers $U_l$ avec des opérateurs de décodage $T_l$ .
- Des codes pour les types dans les univers (ex: codes pour $\Pi$ ).
- Gestion de la cumulativité (optionnelle) via des opérateurs de levage.
Résultat : Bien que la présentation soit infinitaire, les auteurs montrent qu'elle peut être construite comme la limite d'une suite croissante de présentations finies, garantissant l'existence d'un modèle initial.

B. La théorie avec polymorphisme universel explicite ( $\Sigma_{up}$ )

Structure : Il s'agit d'une GAT finie (ou finiment présentée) qui internalise les niveaux d'univers.
Nouvelle structure de base : Les auteurs introduisent une CwF unitaire (ucwf) pour les niveaux.
- Les sorts sont : contextes de niveaux ($lctx$), morphismes de niveaux ($lhom$), termes de niveaux ($ltm$).
- Opérateurs pour le successeur de niveau ( $+$ ) et la borne supérieure ( $\vee$ ).
- Sort d'égalité de niveau ($leq$) : Une contribution majeure est l'introduction d'un sort explicite pour les égalités de niveaux ($leqn(l, l')$). Cela permet de formuler des contraintes comme $l < m$ (défini par $l^+ \vee m = m$ ) directement dans la GAT, sans utiliser d'hypothèses d'égalité interdites dans le formalisme standard des GATs.
CwF indexée par les niveaux : La théorie est modélisée comme un foncteur de la catégorie des niveaux vers la catégorie des CwF.
- Les types et termes sont indexés par un contexte de niveaux $n$ .
- Les opérateurs de substitution agissent à la fois sur les termes/typs et sur les niveaux.
Nouveaux formateurs :
- Univers indexés par des niveaux internes $U_l$ .
- Produits indexés par les niveaux ( $[\alpha]A$ ) : Permettent de quantifier universellement sur les niveaux, avec abstraction $\langle \alpha \rangle a$ et application $a l$ .
Résultat : Cette GAT finie capture toute la structure de la théorie $TT_{up}$ , y compris les contraintes d'ordre entre niveaux et le polymorphisme.

4. Résultats

Caractérisation par initialité : Les auteurs établissent que les théories de types $TT_{tower}$ et $TT_{up}$ sont isomorphes aux modèles initiaux de leurs GATs respectives ( $\Sigma_{tower}$ et $\Sigma_{up}$ ).
Construction de modèles :
- Ils décrivent une construction générique de modèles initiaux basée sur la substitution explicite (calculus de termes bruts quotientés).
- Ils esquissent également une construction basée sur la substitution implicite (la syntaxe usuelle), montrant comment organiser les termes bruts et les relations d'équivalence pour former un objet dans la catégorie des modèles.
Équivalence des approches : Le travail démontre que l'approche par GATs permet de prouver l'équivalence entre différentes présentations syntaxiques (choix de règles d'égalité, gestion des substitutions) en se concentrant sur la structure catégorique sous-jacente unique.
Gestion des contraintes d'égalité : L'introduction du sort $leq$ résout le problème de la formalisation des contraintes d'ordre sur les niveaux dans un cadre GAT, qui ne supporte pas nativement les hypothèses d'égalité dans les signatures.

5. Signification et Impact

Avancement de la conjecture d'initialité : Ce travail fournit une méthode robuste et uniforme pour aborder la conjecture d'initialité de Voevodsky. En caractérisant les théories des types comme des modèles initiaux de GATs, les auteurs contournent les pièges des détails syntaxiques qui ont historiquement rendu ces preuves difficiles.
Unification de la logique catégorique : L'article étend le cadre des GATs et des CwF au-delà des théories des types simples pour inclure des systèmes complexes avec polymorphisme d'univers et logique de prédicats (via des CwF indexées).
Fondement pour les outils de preuve : La clarté structurelle offerte par les GATs facilite l'implémentation et la vérification formelle (par exemple dans Agda, comme mentionné pour le travail de Brunerie et de Boer) de la sémantique des théories des types.
Perspectives futures : Les auteurs prévoient d'utiliser les sorts d'égalité de niveau pour formaliser des contraintes équationnelles plus complexes et d'explorer les liens avec les types inductifs-inductifs quotientés (QIITs) et les théories algébriques généralisées d'ordre supérieur (SOGATs).

En résumé, cet article propose une abstraction puissante des théories des types avec polymorphisme universel, transformant des problèmes syntaxiques complexes en questions de théorie des catégories et d'algèbre générale, offrant ainsi une voie prometteuse pour la métathéorie formelle.