💻 computer science

What does it take to certify a conversion checker?

Cet article soutient que les propriétés d'injectivité, plutôt que la normalisation, constituent le fondement crucial et suffisant pour certifier les procédures de décision pour l'égalité définitionnelle dans la théorie des types dépendants, y compris pour les vérificateurs de conversion entièrement non typés.

Auteurs originaux : Meven Lennon-Bertrand

Publié 2026-07-17

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Meven Lennon-Bertrand

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 construisiez une forteresse numérique, un lieu où vous pouvez écrire des preuves mathématiques et être absolument certain qu'elles sont vraies. Pour garder cette forteresse en sécurité, vous avez besoin d'un minuscule garde, extrêmement strict, à la porte, appelé « assistant de preuve ». Son seul travail est de vérifier si les preuves que vous lui présentez sont valides. Si le garde commet une erreur, toute la forteresse pourrait s'effondrer ; nous devons donc être sûrs à 100 % que le garde fait son travail correctement. C'est le monde de la théorie des types dépendants, une branche de l'informatique et de la logique où les types (comme « nombre » ou « liste de nombres ») peuvent dépendre de valeurs spécifiques, ce qui les rend incroyablement puissants mais aussi incroyablement complexes à gérer.

Le problème central auquel le garde est confronté s'appelle la vérification de conversion. Imaginez que vous ayez deux phrases qui semblent différentes en surface, comme « 2 + 2 » et « 4 ». Pour le garde, elles doivent être reconnues comme étant exactement la même chose. Dans le monde complexe des types dépendants, déterminer si deux choses sont « les mêmes » revient à essayer de démêler un nœud de cordes infinies. Habituellement, pour prouver que le garde travaille correctement, les mathématiciens tentent de prouver que les cordes finiront par se démêler complètement (une propriété appelée normalisation). Cependant, il existe une règle célèbre en logique (le second théorème d'incomplétude de Gödel) qui stipule que vous ne pouvez pas prouver qu'un système est sûr de l'intérieur si cette preuve nécessite que le système soit parfait. C'est comme essayer de se soulever en tirant sur ses propres bottes. Ainsi, la grande question est la suivante : peut-on certifier le garde sans avoir besoin de prouver cet impossible « démêlage parfait » ?

Cet article, écrit par Meven Lennon-Bertrand de l'Université de Cambridge, répond à cette question par un « oui » retentissant, mais avec une nuance. Au lieu de s'appuyer sur la tâche lourde, et souvent impossible, de prouver que tout finit par se démêler, l'auteur montre que le garde a seulement besoin d'être très doué pour un tour spécifique : l'injectivité.

Considérez l'injectivité comme un maître détective capable de regarder un déguisement complexe et de connaître instantanément les ingrédients. Si le garde voit une « fonction » (une machine qui prend une entrée et donne une sortie) et que deux d'entre elles semblent identiques, l'injectivité garantit que leurs composants internes (les entrées et les règles) doivent également être les mêmes. C'est la différence entre voir deux robots d'apparence identique et savoir avec certitude qu'ils ont été construits avec les mêmes plans, et non pas simplement qu'ils se ressemblent par hasard. L'article prouve que si le garde est certifié pour être un détective parfait de ces composants (injectivité), cela suffit pour certifier que le garde est digne de confiance pour presque tout, même sans prouver l'impossible « démêlage parfait ».

L'auteur explore également une seconde version plus chaotique du garde : un garde qui ne regarde pas du tout les « types » (les étiquettes), mais seulement les formes brutes des termes. C'est comme un garde qui ignorerait les badges de nom pour ne vérifier que si les chaussures et les chapeaux correspondent. Étonnamment, l'article trouve que ce garde « non typé » peut également être certifié, à condition qu'il suive les mêmes règles de détective, bien que les règles pour les « chaussures et chapeaux » doivent être légèrement différentes selon que les objets sont simples ou complexes.

L'article ne se contente pas de suggérer cela ; il fournit une preuve formelle, vérifiée par ordinateur (en utilisant un outil appelé Rocq), que ces idées fonctionnent. Il montre qu'en se concentrant sur ces propriétés de « détective » (l'injectivité) plutôt que sur les propriétés de « démêlage » (la normalisation), nous pouvons construire un assistant de preuve certifié et digne de confiance. C'est une avancée majeure car cela signifie que nous n'avons pas besoin de résoudre le problème insoluble de prouver que le système est parfaitement cohérent pour avoir un assistant de preuve sûr. Nous devons simplement prouver que le garde est doué pour identifier les bons ingrédients. L'article note également que si cela fonctionne pour la plupart des types standards, il existe des types très étranges, de type « unité », où les choses deviennent confuses et où le garde pourrait avoir besoin d'une aide supplémentaire, mais pour la vaste majorité des cas, l'approche du détective est la clé pour déverrouiller les logiciels certifiés.

Résumé technique : Que faut-il pour certifier un vérificateur de conversion ?

Énoncé du problème
La certification des noyaux d'assistants de preuve (les composants centraux responsables de la vérification des preuves) est un défi critique dans la théorie des types dépendants. Bien que le « critère de de Bruijn » permette d'accorder une confiance à un petit noyau, la certification du noyau lui-même est difficile car les théories des types dépendants reposent sur des invariants complexes. Plus précisément, prouver la correction d'un vérificateur de conversion (qui décide l'égalité définitionnelle, $\sim=$ ) nécessite traditionnellement de prouver la normalisation du système (la terminaison de la réduction). Cependant, en raison du second théorème d'incomplétude de Gödel, un système ne peut prouver sa propre cohérence ou sa propre normalisation. Par conséquent, une certification complète d'un noyau à types dépendants au sein du système lui-même est irréalisable. L'article cherche à identifier les propriétés méta-théoriques minimales requises pour certifier les vérificateurs de conversion sans dépendre d'une preuve complète de normalisation, visant une « défaillance gracieuse » où le vérificateur est certifié sur la base de propriétés plus faibles et prouvables.

Méthodologie
Les auteurs adoptent une approche modulaire, séparant la méta-théorie (la « boîte à outils opaque » de propriétés telles que l'injectivité et la normalisation) de la certification algorithmique (l'implémentation du vérificateur).

Système formel : Le travail est formalisé dans l'assistant de preuve Rocq (anciennement Coq) pour une version de la théorie des types de Martin-Löf (MLTT) présentant des types fonctions ( $\Pi$ ) et paires ( $\Sigma$ ) dépendants, des types inductifs (vide, entiers naturels, identité), et un univers, le tout avec élimination large.
Algorithmes : Deux algorithmes de vérification de conversion sont implémentés et certifiés :
- Conversion typée : Un algorithme bidirectionnel dirigé par les types, similaire à ceux de Coq et Agda, qui maintient l'information de type tout au long de la vérification.
- Conversion non typée : Un algorithme dirigé par les termes, similaire à ceux de Rocq et Lean, qui ne maintient pas l'information de type pendant la réduction des termes mais repose sur une spécification typée pour sa correction.
Cadre de certification : Les algorithmes sont implémentés en utilisant le monade de récursion libre de McBride (via PartialFun) pour gérer la partialité. Les auteurs définissent des préconditions (invariants) et des postconditions pour les algorithmes. La correction est décomposée en :
- Correction positive (Positive Soundness) : Si l'algorithme retourne « oui », les termes sont convertibles.
- Correction négative (Negative Soundness) : Si l'algorithme retourne « non », les termes ne sont pas convertibles.
- Terminaison : L'algorithme s'arrête toujours.

Contributions clés
La contribution principale de l'article est l'identification et la démonstration que les propriétés d'injectivité des constructeurs de types et de termes sont les propriétés méta-théoriques cruciales et suffisantes pour certifier la correction des vérificateurs de conversion.

L'injectivité comme exigence centrale : Les auteurs montrent que l'injectivité des constructeurs de types (par exemple, si $\Pi x:A.B \sim= \Pi x:A'.B'$ , alors $A \sim= A'$ et $B \sim= B'$ ) et l'absence de confusion (par exemple, $\Pi x:A.B$ ne peut pas être convertible à $N$ ) sont suffisantes pour prouver la correction positive.
Injectivité au niveau des termes : Pour prouver la correction négative, les auteurs démontrent que les propriétés d'injectivité des constructeurs de termes (spécifiquement pour les entiers naturels et les types $\Pi$ ) et la complétude de la comparaison des neutres (garantissant que les neutres convertibles peuvent être comparés structurellement) sont nécessaires.
Équivalence Typée vs Non Typée : L'article présente une certification inédite d'un vérificateur de conversion non typé par rapport à une spécification typée. Il clarifie que la conversion « non typée » est en fait une « conversion typée dirigée par les termes », où l'information de type est implicite dans les invariants plutôt qu'explicite dans les étapes de réduction.
Analyse de dépendance : En utilisant les classes de types de Rocq, les auteurs fournissent une carte de dépendance fine (Figure 1 de l'article) montrant exactement quelles propriétés méta-théoriques (Injectivité, Normalisation, etc.) sont nécessaires pour chaque propriété algorithmique (Correction, Terminaison).

Résultats
La formalisation (ajoutant environ 10 000 lignes de code à la base existante de Rocq) produit les résultats spécifiques suivants :

Correction positive : Prouvée pour les algorithmes typés et non typés en utilisant uniquement l'injectivité des constructeurs de types. Cette propriété n'implique pas la cohérence logique et peut être prouvée dans une méta-théorie plus faible que la théorie objet.
Correction négative : Prouvée en utilisant l'injectivité des constructeurs de types et de termes ainsi que la complétude de la comparaison des neutres.
- Pour l'algorithme typé, la complétude de la comparaison des neutres n'est requise qu'au niveau des types positifs (Propriété 9).
- Pour l'algorithme non typé, la complétude est requise pour tous les types (Propriété 7), en raison de l'absence d'information de type guidant l' $\eta$ -expansion des types négatifs.
Terminaison : Prouvée pour les deux algorithmes en supposant une normalisation profonde (Propriété 11). Cette propriété est la seule qui implique la cohérence logique et nécessite une méta-théorie plus forte que la théorie objet.
Équivalence : Les auteurs prouvent que les algorithmes typés et non typés sont équivalents (Propositions 22 et 24). La preuve repose sur le renforcement (suppression des variables non pertinentes du contexte) et la normalisation. L'algorithme non typé est montré comme étant une implémentation valide de la spécification typée.

Signification et Revendications
L'article affirme que la « clé de voûte » de la certification d'un vérificateur de types n'est pas la preuve complète de normalisation, mais plutôt les propriétés d'injectivité du système de types.

Défaillance gracieuse : Les auteurs soutiennent que même si la normalisation ne peut être prouvée (en raison des limitations de Gödel), on peut toujours certifier la correction d'un vérificateur. Cela permet la certification d'implémentations complexes et optimisées (comme celles de Rocq ou Lean) en supposant l'injectivité comme un axiome ou en la prouvant dans une méta-théorie plus faible.
Modularité : Ce travail préconise une approche de la « méta-théorie comme boîte noire ». La certification de l'algorithme doit dépendre uniquement d'un petit ensemble de propriétés axiomatisées (injectivité, complétude des neutres) plutôt que d'une preuve monolithique de toute la théorie des types.
Certification non typée : L'article démontre que la certification de vérificateurs dirigés par les termes (non typés) est réalisable et que la distinction entre conversion typée et non typée concerne moins l'absence de types que la direction de l'algorithme (dirigé par les termes vs dirigé par les types).
Limites : Les auteurs notent modestement que leur travail couvre une version simplifiée de MLTT. Ils reconnaissent que des fonctionnalités comme les types unités définitionnels (où tous les habitants sont convertibles) ou les propositions strictes (irrélevance de la preuve) compliquent la complétude de la comparaison des neutres, nécessissant des stratégies spécifiques (comme le ré-inférence de types ou le suivi des univers) dans les noyaux réels. Ils notent également que les théories des types extensives et cubiques présentent des défis supplémentaires concernant le renforcement et la complétude des neutres.

En résumé, l'article fournit une feuille de route pour certifier les vérificateurs de conversion en isolant l'injectivité comme la condition suffisante pour la correction, permettant ainsi de découpler la certification de l'algorithme de la tâche difficile de prouver la normalisation complète.

Résumé technique : Que faut-il pour certifier un vérificateur de conversion ?

Articles similaires