💻 computer science

Are Dependent Types in Set Theory Feasible?

Cet article présente une intégration mécanisée des types dépendants et d'une hiérarchie d'univers dans la logique du premier ordre via la théorie des ensembles de Tarski-Grothendieck, permettant une vérification complète des preuves de typage au sein de l'assistant de preuve Lisa.

Auteurs originaux : Yunsong Yang, Simon Guilloud, Viktor Kunčak

Publié 2026-03-16

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Yunsong Yang, Simon Guilloud, Viktor Kunčak

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 Tours de Lego avec des Briques de Mathématiques

Imaginez que vous avez deux façons de construire des choses très complexes (comme des logiciels ou des preuves mathématiques) :

La méthode "Type Theory" (Théorie des Types) : C'est comme utiliser un jeu de Lego spécial. Chaque pièce a une forme précise, une couleur spécifique et ne s'emboîte que si elle correspond parfaitement à son voisin. C'est très sûr, très rigoureux, et les ordinateurs adorent ça (c'est ce que utilisent des outils modernes comme Lean ou Rocq). Mais c'est aussi un système très complexe à fabriquer de zéro.
La méthode "Set Theory" (Théorie des Ensembles) : C'est comme utiliser des briques de construction classiques (des cubes, des planches) que tout le monde connaît depuis 100 ans (la théorie ZFC). C'est la fondation "classique" des mathématiques. C'est robuste, simple à comprendre, mais un peu "brut" : rien n'empêche une brique ronde de s'insérer dans un trou carré si vous forcez un peu.

Le problème ?
Les développeurs de logiciels modernes préfèrent le système "Lego spécial" (Types) pour sa sécurité. Mais les mathématiciens et les vérificateurs de preuves "classiques" préfèrent le système "briques classiques" (Ensembles) car c'est plus simple à vérifier.

La question du papier :
Peut-on construire les pièces de Lego complexes (les Types Dépendants) en utilisant uniquement les briques classiques (les Ensembles) ? Est-ce possible de faire fonctionner le système "Lego" à l'intérieur du système "Briques" sans que ça s'effondre ?

🧩 La Réponse : OUI, et voici comment ils l'ont fait

Les auteurs (Yunsong Yang, Simon Guilloud et Viktor Kunčak) disent : "Oui, c'est possible !" Ils ont réussi à créer un "traducteur" automatique qui prend les règles complexes du système Lego et les traduit en règles simples de briques classiques, tout en gardant la sécurité.

Voici les 3 étapes clés de leur recette, expliquées avec des métaphores :

1. Le Traducteur Magique (L'Encodage)

Imaginez que vous voulez écrire un poème en chinois (le langage complexe des Types Dépendants) sur un papier où vous ne pouvez écrire que des lettres latines (le langage simple des Ensembles).

Ce qu'ils ont fait : Ils ont créé un dictionnaire. Quand le système voit une pièce de Lego complexe (une fonction qui dépend d'une autre), il la transforme immédiatement en une règle mathématique simple : "Ceci est un ensemble de paires de nombres qui obéissent à telle loi".
L'astuce : Ils utilisent une extension de la logique classique qui permet de manipuler des "boîtes" (des fonctions) comme si c'étaient des objets ordinaires.

2. Les Étagères Infinies (Les Univers)

Dans le monde des Types, il y a un problème : si vous avez une boîte qui contient des boîtes, dans quelle boîte mettez-vous cette boîte ? Si vous la mettez dans une boîte plus grande, et que cette boîte contient encore des boîtes... vous avez besoin d'une étagère infinie.

Le problème classique : En mathématiques classiques, il n'existe pas de "boîte" assez grande pour contenir toutes les autres boîtes.
La solution des auteurs : Ils ont utilisé une règle mathématique spéciale appelée l'axiome de Tarski. Imaginez que cet axiome vous donne un magicien capable de créer instantanément une nouvelle étagère plus grande que n'importe quelle étagère existante.
Résultat : Ils peuvent empiler leurs boîtes (Types) à l'infini sans jamais manquer d'espace, tout en restant dans le monde des mathématiques classiques.

3. Le Robot Vérificateur (La Preuve Automatique)

Le plus grand défi n'est pas seulement de construire, mais de vérifier que tout est bien rangé.

Leur innovation : Ils ont programmé un robot (un "tactique" dans leur logiciel Lisa).
Comment il travaille :
- Si vous lui donnez une fonction, il regarde : "Est-ce que cette fonction rentre bien dans la boîte prévue ?"
- Si oui, il ne se contente pas de dire "Oui". Il écrit le rapport de contrôle (la preuve mathématique) étape par étape, en utilisant uniquement les règles de base des briques classiques.
- Il gère même les cas où une boîte est un peu plus petite ou plus grande qu'une autre (ce qu'on appelle le sous-typage), en vérifiant que ça ne casse rien.

🌟 Pourquoi c'est important ? (L'Analogie Finale)

Imaginez que vous avez deux pays :

Pays A (Types) : Très avancé, avec des autoroutes à 10 voies, mais très cher à construire et à entretenir.
Pays B (Ensembles) : Un pays avec des routes de terre simples, mais très solides et connues de tous depuis des siècles.

Ce papier est comme la construction d'un pont automatique.
Grâce à ce pont, un ingénieur du Pays A peut envoyer ses plans complexes (ses preuves de logiciels) vers le Pays B. Le robot du Pays B les reçoit, les traduit en langage "route de terre", vérifie que tout est solide, et renvoie un certificat de sécurité officiel.

En résumé :
Les auteurs ont prouvé qu'on n'a pas besoin d'abandonner la simplicité des mathématiques classiques pour utiliser les outils puissants des types modernes. Ils ont montré qu'on peut avoir le meilleur des deux mondes : la puissance des "Types" avec la sécurité et la simplicité des "Ensembles".

C'est une étape majeure pour permettre aux mathématiciens et aux informaticiens de travailler ensemble, en partageant leurs preuves sans avoir à tout réécrire.

1. Problématique et Contexte

L'article s'attaque à la question de la faisabilité de l'intégration des types dépendants (au cœur de la théorie des types dépendants ou DTT, utilisée par des assistants de preuve comme Rocq/Coq et Lean 4) au sein d'une fondation basée sur la théorie des ensembles (ZFC ou Tarski-Grothendieck).

Le constat : La théorie des ensembles (ZFC) est la fondation standard des mathématiques depuis plus d'un siècle. En revanche, l'automatisation des preuves interactives est dominée par des systèmes basés sur la théorie des types dépendants. Ces systèmes, bien que pratiques (vérification de types prévisible, évaluation intégrée), possèdent des noyaux logiques complexes et coûteux à valider formellement par rapport à la logique du premier ordre avec ZFC.
L'objectif : Développer un système de types « doux » (soft type system) pour un assistant de preuve basé sur la théorie des ensembles. L'ambition est de permettre l'interopérabilité des preuves (par exemple, transférer des preuves de Lean 4 vers des assistants basés sur la théorie des ensembles comme Lisa) sans avoir à encoder lourdement la théorie des types dans la théorie des ensembles, tout en garantissant la correction formelle via les axiomes ensemblistes.

2. Méthodologie

Les auteurs ont implémenté leur approche dans Lisa, un assistant de preuve dont le noyau logique est basé sur la logique du premier ordre avec égalité et la théorie des ensembles.

A. Fondations Logiques (λFOL)

Pour surmonter la limitation de la logique du premier ordre (qui ne gère pas naturellement les abstractions $\lambda$ ), les auteurs utilisent λFOL (Lambda First-Order Logic), une extension de Lisa intégrant :

Des termes $\lambda$ -typés sur deux sorts primitifs : Prop (propositions) et Ind (individus).
L'opérateur $\varepsilon$ de Hilbert pour la sélection de valeurs.
La réduction $\beta$ et l'instanciation de symboles schématiques comme règles de base.
Cela permet de représenter les termes de la théorie des types comme des termes de logique du premier ordre, tout en conservant la simplicité du noyau logique.

B. Encodage des Types Dépendants

Les types dépendants sont encodés directement comme des ensembles :

Abstraction ( $\lambda x : T. u$ ) : Encodée comme un ensemble de paires $\{ \langle x, L(x) \rangle \mid x \in T \}$ .
Application ( $t\ u$ ) : Encodée via l'opérateur $\varepsilon$ pour extraire la valeur associée dans l'ensemble fonctionnel.
Produit Dépendant ( $\Pi x : T_1. T_2$ ) : Encodé comme l'ensemble des fonctions $f$ dont le domaine est $T_1$ et dont l'image de chaque $x$ appartient à $T_2(x)$ .
Les règles de réduction $\beta$ et les règles de typage (introduction et élimination) sont prouvées comme des théorèmes dérivés des axiomes de la théorie des ensembles et des définitions ci-dessus.

C. Gestion des Univers

La théorie ZFC standard ne possède pas d'univers internes fermés sous les constructions ensemblistes (notamment le produit $\Pi$ ). Pour modéliser la hiérarchie cumulative des univers ( $Type_i : Type_{i+1}$ ) requise par les types dépendants :

Les auteurs utilisent l'axiome de Tarski (ou axiome des univers de Grothendieck), qui postule l'existence d'un nombre infini d'univers fermés sous les opérations ensemblistes usuelles.
Ils définissent un prédicat isUniverse simplifié, suffisant pour la fermeture sous les produits dépendants.
Une hiérarchie d'univers est construite itérativement via un opérateur universeOf, permettant de gérer les niveaux d'univers nécessaires à la polymorphie.

D. Génération de Preuves Automatique

Pour éviter la vérification manuelle fastidieuse des jugements de typage, les auteurs ont implémenté une tactique de preuve bidirectionnelle (Typecheck.prove) :

Mode Inférence (Infer) : Déduit le type d'un terme.
Mode Vérification (Check) : Vérifie qu'un terme possède un type attendu.
Mode Sous-typage (Subset) : Gère les relations de sous-typage (notamment la covariance dans le codomaine des fonctions).
Cette tactique synthétise des objets de preuve vérifiables par le noyau de Lisa, prouvant que le terme appartient bien à l'ensemble correspondant au type.

3. Contributions Clés

Encodage Mécanisé : Première implémentation d'un système de types dépendants avec univers dans un assistant basé sur la théorie des ensembles (Lisa), utilisant une traduction syntaxique peu profonde (shallow translation).
Justification Formelle : Tous les aspects du typage (réduction $\beta$ , règles d'introduction/élimination, gestion des univers) sont dérivés et prouvés à partir des axiomes de Tarski-Grothendieck et de la logique du premier ordre.
Support du Sous-typage : Implémentation d'une forme de sous-typage (covariance du codomaine, invariance du domaine) qui fonctionne dans le cadre ensembliste, bien que la contravariance (courante en théorie des types) soit limitée par des considérations de taille d'ensembles (impredicativité).
Interopérabilité Potentielle : Démonstration qu'il est possible de traduire des jugements de typage complexes (comme la composition de fonctions polymorphes) en preuves ensemblistes vérifiables, ouvrant la voie au transfert de preuves depuis des systèmes comme Lean 4.

4. Résultats et Exemples

Les auteurs démontrent la viabilité de leur approche à travers plusieurs exemples :

Théorèmes de base : Preuve formelle des règles de réduction $\beta$ et des règles de formation des types ( $\Pi$ -formation).
Composition Polymorphe : Un exemple concret montre la composition d'une fonction $f: A \to B$ avec une fonction identité polymorphe. Le système infère automatiquement les niveaux d'univers et génère une preuve que le résultat est bien typé comme une fonction $A \to B$ .
Gestion des Univers : Le système gère correctement la hiérarchie cumulative, permettant d'instantier des opérateurs polymorphes définis à un niveau d'univers élevé sur des types situés à des niveaux inférieurs.

5. Signification et Impact

Ce travail est significatif pour plusieurs raisons :

Réduction de la complexité de vérification : En reposant sur un noyau logique basé sur la théorie des ensembles (plus simple et mieux compris que les noyaux de la théorie des types), il offre une alternative robuste pour la vérification de preuves complexes.
Pont entre paradigmes : Il comble le fossé entre la théorie des ensembles (fondation mathématique classique) et la théorie des types (fondation informatique moderne), facilitant potentiellement l'échange de preuves entre écosystèmes (ex: Lean vers Mizar ou Isabelle/ZF).
Faisabilité : Il répond positivement à la question de la faisabilité, montrant que les types dépendants ne nécessitent pas intrinsèquement une théorie des types pour être définis, mais peuvent être vus comme des constructions ensemblistes spécifiques, tant que l'on dispose d'axiomes d'univers adéquats (Tarski).

En conclusion, l'article établit que les types dépendants peuvent être intégrés de manière mécanisée et vérifiée dans un cadre ensembliste, offrant une base solide pour le développement futur d'assistants de preuve hybrides ou pour le transfert de preuves à grande échelle.