💻 computer science

Proof Theory and Dependent Type Theory: Distinct Foundations for Designing Proof Assistants

Cet article soutient que la théorie moderne de la preuve structurelle, illustrée par le calcul des séquents et implémentée dans le prouveur de théorèmes Abella, offre une alternative convaincante à la théorie des types dépendants pour la conception d'assistants de preuve en séparant mieux la logique de la structure de preuve, en utilisant stratégiquement le non-déterminisme, en évitant les problèmes de typage complexes et en fournissant une approche élégante pour la gestion des liaisons.

Auteurs originaux : Dale Miller (Inria Saclay,LIX, Institut Polytechnique de Paris)

Publié 2026-07-15

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Dale Miller (Inria Saclay,LIX, Institut Polytechnique de Paris)

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

Imaginez que vous essayiez de construire le « Assistant de Preuve » ultime — un robot super intelligent qui aide les humains à vérifier leurs devoirs de mathématiques et de logique pour s'assurer qu'ils sont corrects à 100 %. Pendant des décennies, la plupart de ces robots ont été construits en utilisant un blueprint spécifique appelé Théorie des Types Dépendants (DTT). C'est comme construire un robot à partir d'un ensemble de Legos très complexes et de haute technologie où chaque brique possède une étiquette spécifique, et le robot vérifie si les étiquettes correspondent parfaitement avant de vous laisser les assembler.

Mais dans cet article, l'auteur Dale Miller suggère qu'il existe une autre façon, peut-être meilleure, de construire ces robots. Il soutient que nous devrions regarder la Théorie de la Preuve Structurelle, plus précisément un cadre appelé le Calcul des Séquents. Considérez cela non pas comme un ensemble de Legos rigide, mais comme un puzzle dynamique et mobile où les pièces peuvent glisser et changer de forme tant que la logique est respectée.

Voici la décomposition de pourquoi Miller pense que cette approche par « puzzle » pourrait être supérieure à l'approche « Lego », en utilisant six idées clés :

1. Séparer le « Quoi » du « Comment »

Dans le monde des Legos (DTT), le robot décide de deux choses à la fois : ce que votre logique utilise et comment la preuve est construite. C'est comme dire : « Nous n'avons le droit de construire des tours qu'avec des briques rouges, et la seule façon de les empiler est verticalement. »
Miller suggère de séparer ces éléments. Nous pouvons décider de la logique (les règles du jeu) puis choisir n'importe quelle structure de preuve pour la résoudre. C'est comme décider que vous voulez jouer au football, puis réaliser que vous pouvez marquer des buts en frappant, en jouant de la tête ou même en utilisant un canon à ballons si les règles le permettent. Le Calcul des Sents vous permet d'utiliser de nombreux différents « mouvements » (comme la déduction naturelle, les tableaux ou la résolution) sans vous contraindre à un seul style rigide.

2. Le problème des « Preuves comme Code »

L'approche Lego traite une preuve comme un programme informatique (un terme λ). Bien que les ordinateurs soient excellents pour exécuter des programmes, ils peuvent être pointilleux. Parfois, le programme prend un chemin étrange pour arriver à la réponse, ou il reste bloqué parce qu'il attend un type spécifique d'entrée.
Miller souligne que l'approche Lego doit gérer des problèmes complexes comme les « niveaux d'univers » (une façon complexe d'organiser les types pour qu'ils ne s'entrechoquent pas) et l'« irrelience de la preuve » (perdre du temps à vérifier des parties de la preuve qui n'ont pas réellement d'importance). L'approche du Calcul des Séquents est plus simple ; elle n'a pas besoin de se soucier de ces règles de typage lourdes car elle traite la structure de la preuve plus directement, comme un organigramme plutôt que comme un script de code complexe.

3. Gérer la logique « Classique » (Le problème du « Soit/Soit »)

Certaines logiques sont « intuitionnistes » (vous devez prouver que quelque chose existe en le construisant), et d'autres sont « classiques » (vous pouvez prouver que quelque chose existe simplement en montrant qu'il est impossible qu'il n'existe pas).
L'approche Lego peine à gérer le style « classique » de manière fluide. Elle doit souvent ajouter des règles supplémentaires et encombrantes pour que cela fonctionne. Miller soutient que le Calcul des Séquents a été conçu dès le départ pour gérer les deux styles de manière égale, comme un adaptateur universel qui s'adapte à n'importe quelle prise sans avoir besoin d'un convertisseur volumineux.

4. Embrasser le « Peut-être » (Non-déterminisme)

C'est un point majeur. Les robots Lego sont construits pour être « déterministes », ce qui signifie qu'ils doivent suivre un chemin unique et droit pour vérifier une preuve. S'ils rencontrent une impasse, ils s'arrêtent.
Miller suggère que permettre un peu de « non-déterminisme » (deviner et revenir en arrière) est en fait un super-pouvoir. Imaginez un labyrinthe. Un robot déterministe parcourt un chemin et s'arrête s'il rencontre un mur. Un robot non-déterministe peut essayer un chemin, heurter un mur, dire « oups », et instantanément essayer un autre chemin.
Miller soutient qu'en laissant le vérificateur de preuve « deviner » et revenir en arrière, nous pouvons rendre les « certificats de preuve » (les devoirs que vous rendez) beaucoup plus petits. Le robot fait le gros du travail de recherche, de sorte que vous n'avez pas à noter chaque étape. C'est un compromis : une feuille de devoirs plus petite pour un robot qui doit réfléchir un peu plus intensément.

5. La magie des « Liants Mobiles »

C'est le tour de magie le plus excitant de l'article. En logique, nous traitons souvent des variables qui sont « liées » (comme le « x » dans « pour tout x... »). Dans le monde des Legos, ces variables sont souvent figées en place, et gérer cela est un cauchemar de problèmes techniques (comme le célèbre défi du POPLMark).
Miller propose une vision où ces variables sont mobiles. Il appelle cela la syntaxe λ-arbre.
Imaginez qu'une variable est un badge nominatif sur une personne. Dans le monde des Legos, si vous déplacez la personne, le badge pourrait tomber ou devenir confus. Dans le monde de Miller, le badge est collé à la personne. Peu importe comment vous déplacez la personne dans la pièce (ou la preuve), le badge reste avec elle.
Il introduit un outil spécial appelé le quantificateur ∇ (prononcé « nabla »). Considérez cela comme un bouton de « portée locale ». Quand vous appuyez dessus, cela dit : « Cette variable appartient uniquement à cette partie spécifique de la preuve, et elle ne pourra jamais s'échapper. » Cela rend extrêmement facile le raisonnement sur des langages qui ont des règles complexes, comme les langages de programmation ou le π-calcul (une façon de modéliser la communication entre les ordinateurs).

6. Le Robot Abella

Miller ne se contente pas d'en parler ; il a construit un robot pour prouver que cela fonctionne. Il s'appelle Abella.
Abella est un prouveur de théorèmes entièrement construit sur ces principes de Calcul des Séquents. Il utilise les « liants mobiles » et le quantificateur ∇ pour gérer la logique complexe des langages et des liaisons avec aisance. Bien que les robots basés sur les Legos (comme Coq ou Lean) soient très populaires et possèdent d'immenses bibliothèques de preuves pré-construites, Abella suggère que pour certains problèmes délicats — particulièrement ceux impliquant la façon dont les variables sont nommées et déplacées — cette nouvelle approche est plus naturelle et élégante.

L'essentiel

Miller ne dit pas que les robots Lego (Théorie des Types Dépendants) sont mauvais ou qu'il faut les jeter. Il reconnaît qu'ils sont matures, largement utilisés et excellents pour beaucoup de choses.
Cependant, il suggère que pour les fondations de la conception de ces assistants de preuve, le Calcul des Séquents offre un ensemble d'outils plus flexible, plus simple et plus puissant. Il sépare la logique de la structure, embrasse l'intelligence de la conjecture et gère la question complexe des « variables mobiles » avec une élégance que le standard actuel peine à égaler. C'est une invitation à regarder le problème sous un autre angle, en utilisant un cadre qui a connu du succès dans de nombreux autres domaines de la logique mais qui n'a pas encore pris la vedette dans le monde des assistants de preuve interactifs.

Problème
L'article traite des choix de conception fondamentaux sous-jacents aux prouveurs de théorèmes interactifs. Alors que le paradigme dominant dans les systèmes majeurs (par exemple, Coq, Lean, Agda) repose sur la Théorie des Types Dépendants (DTT) et le paradigme « les preuves comme termes » — où les preuves sont représentées comme des $\lambda$ -termes à types dépendants — l'auteur soutient que la théorie de la preuve structurelle moderne, spécifiquement le calcul des séquents, offre une alternative convaincante, bien que sous-utilisée. L'article pose que l'approche DTT confond la logique formalisée avec la structure de la preuve, ce qui entraîne des complexités pour gérer la logique classique, le non-déterminisme et les liaisons syntaxiques qu'une perspective de la théorie de la preuve pourrait résoudre plus élégamment.

Méthodologie
L'auteur emploie une analyse théorique comparative, contrastant les récits de conception des systèmes basés sur la DTT avec ceux dérivés de la théorie de la preuve structurelle. La méthodologie comprend :

Enquête historique et théorique : Tracer les origages de la déduction naturelle et du calcul des séquents (Gentzen) ainsi que leurs applications ultérieures dans les preuves de cohérence, les preuves d'indépendance et la programmation logique.
Décomposition conceptuelle : Séparer la question de « quelle logique est formalisée » de « ce qui constitue une preuve », en soutenant que la DTT fixe souvent la structure de la preuve (déduction naturelle encodée comme $\lambda$ -termes) parallèlement à la logique, alors que la théorie de la preuve permet diverses structures de preuve (calcul des séquents, tableaux, résolution) pour une même logique.
Analyse critique des limites de la DTT : Examiner des obstacles techniques spécifiques à la DTT, tels que la confusion entre l'irrélevance de la preuve, les niveaux d'univers et les arguments implicites, ainsi que les difficultés de gestion uniforme de la logique classique (par exemple, l'exclusion des séquents à conclusions multiples).
Proposition de mécanismes de la théorie de la preuve : Introduire des concepts spécifiques de la théorie de la preuve — la polarité, le focus et, notamment, la mobilité des lieurs via la syntaxe $\lambda$ -arbre et le quantificateur $\nabla$ — comme des mécanismes supérieurs pour gérer les liaisons syntaxiques et le raisonnement méta-théorique.
Illustration par l'implémentation : Utiliser le prouveur de théorèmes Abella comme réalisation concrète de ces principes pour démontrer comment le cadre théorique fonctionne en pratique.

Contributions clés
L'article identifie six sujets spécifiques où la perspective de la théorie de la preuve offre des avantages distincts par rapport à la DTT :

Séparation de la logique et de la structure de la preuve : Contrairement à la DTT, qui lie souvent une logique spécifique à un encodage de preuve particulier (déduction naturelle comme $\lambda$ -termes), la théorie de la preuve permet plusieurs structures de preuve (calcul des séquents, tableaux, etc.) pour la même logique, facilitant diverses stratégies d'inférence (chaînage avant/arrière).
Évitement des complications de la DTT : L'approche de la théorie de la preuve contourne les disciplines de typage complexes inhérentes à la DTT, telles que la gestion des niveaux d'univers, la gestion de l'irrélevance de la preuve et le traitement de la redondance entre typage explicite et implicite.
Gestion de la logique classique : Alors que la DTT peine à représenter uniformément la logique classique (nécessitant souvent des axiomes comme le principe du tiers exclu), le calcul des séquents (spécifiquement à conclusions multiples) fournit un cadre naturel et uniforme pour les logiques classique et intuitionniste, supportant des structures comme les disjonctions de Herbrand et les réfutations par résolution.
Utilisation stratégique du non-déterminisme : L'article soutient que les vérificateurs de preuves n'ont pas besoin d'être strictement déterministes. Autoriser le non-déterminisme (par exemple, via la recherche avec retour en arrière) dans le noyau permet des compromis précieux entre la taille des certificats de preuve et le temps requis pour la vérification, une ressource souvent ignorée dans les noyaux fonctionnels et déterministes de la DTT.
Traitement des liaisons (Mobilité des lieurs) : Ceci est présenté comme la contribution la plus significative. L'article préconise de traiter les lieurs non pas comme des espaces de fonctions (vue extensionnelle) mais comme des abstractions mobiles sur la syntaxe (vue intentionnelle). Ceci est réalisé grâce à la syntaxe $\lambda$ -arbre, où les lieurs peuvent passer du niveau terme au niveau formule au niveau preuve (variables propres) sans jamais devenir libres.
Le quantificateur $\nabla$ : L'introduction du quantificateur $\nabla$ (un nouveau lieur au niveau formule) permet de spécifier des jugements génériques et de gérer des signatures de liaison locales. Il est auto-dual et interagit naturellement avec l'égalité, fournissant un mécanisme robuste pour raisonner sur la syntaxe avec des liaisons.

Résultats
L'article ne présente pas de nouveaux tests de performance expérimentaux ou de données empiriques, mais plutôt une synthèse théorique et une démonstration de faisabilité à travers le prouveur Abella.

Capacités d'Abella : Il est démontré qu'Abella exploite avec succès la syntaxe $\lambda$ -arbre et le quantificateur $\nabla$ pour raisonner sur la méta-théorie de langages et de logiques impliquant des liaisons complexes.
Applications spécifiques : L'article cite des spécifications réussies dans Abella, incluant :
- Des formulations du $\lambda$ -cube et de l'inférence de types polymorphes de rang supérieur.
- Des formalisations de la théorie du $\lambda$ -calcul de Barendregt.
- La sémantique opérationnelle et la méta-théorie du $\pi$ -calculus, incluant les distinctions entre bisimulation ouverte et fermée et la capture des opérateurs modaux.
Équivalence théorique : L'article démontre que la formule $\forall w. \lambda x.x \neq \lambda x.w$ est prouvable dans ce cadre car le problème d'unification d'ordre supérieur $(\lambda x.x = \lambda x.w)$ n'a pas d'unificateurs, illustuant la puissance de la vue intentionnelle des lieurs.

Signification
L'article affirme que la théorie de la preuve structurelle moderne offre une « alternative fondamentale robuste et convaincante » au paradigme de la DTT pour la conception de prouveurs de théorèmes interactifs. Sa signification réside dans :

Recadrage du récit de conception : Il conteste l'hypothèse selon laquelle le $\lambda$ -calcul à types dépendants est la seule ou la meilleure façon de représenter les preuves, suggérant que le calcul des séquents fournit un cadre plus flexible et naturel, particulièrement pour le raisonnement méta-théorique.
Résolution des problèmes de liaison : Il propose que l'approche de la « mobilité des lieurs » résout les défis de longue date concernant l'encodage des liaisons syntaxiques (référencés comme le défi POPLMark), offrant un traitement canonique qui évite le besoin d'encodages complexes comme les indices de de Bruijn ou les variables nommées dans la spécification logique de l'utilisateur.
Clartité fondamentale : En séparant la logique de la structure de la preuve et en embrassant le non-déterminisme, l'approche permet des spécifications plus directes et élégantes de systèmes complexes, comme en témoigne les capacités du prouveur Abella.

L'auteur conclut que bien que la DTT possède des implémentations matures et une adoption large, la perspective de la théorie de la preuve offre une fondation de conception plus profonde et plus flexible, particulièrement pour les systèmes nécessitant un raisonnement sophistiqué sur les liaisons et la méta-théorie.