A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

Résumé Technique : Une preuve de consistance mécanisée pour les systèmes de types purs imprédicatifs

Problème et Contexte
L'article traite des défis de la mécanisation de la théorie des types, en se concentrant spécifiquement sur les propriétés méta-théoriques des Systèmes de Types Purs (PTS). Une difficulté centrale de la formalisation de la substitution et de la réduction $\beta$ réside dans la gestion du renommage des variables pour éviter la capture de noms. Les définitions traditionnelles (par exemple, Curry-Feys) nécessitent une induction bien fondée sur la longueur des termes en raison des étapes de renommage non primitives récursives, ce qui rend la mécanisation difficile. Des approches alternatives telles que les indices de de Bruijn (dBI), la syntaxe localement sans nom (locally nameless), ou l'Abstraction de Syntaxe de Haut Rang (HOAS) offrent des solutions mais introduisent leurs propres inconvénients : le dBI est laborieux pour la lisibilité humaine ; la syntaxe localement sans nom nécessite des prédicats de bien-formalité qui « polluent » les résultats méta-théoriques ; et l'HOAS empêche souvent la génération de code exécutable ou la formulation de questions de décidabilité.

Les auteurs évaluent la faisabilité d'une approche qui conserve une syntaxe classique (utilisant des variables nommées) tout en utilisant les substitutions simultanées de Stoughton. Cette méthode effectue le renommage des variables liées simultanément à la substitution via une récursion structurelle unique, évitant ainsi le recours à l'induction bien fondée sur la longueur des termes pour la plupart des preuves.

Méthodologie
Le développement est entièrement mécanisé à l'aide d'Agda (v2.6.2.2) et de sa bibliothèque standard. La méthodologie repose sur les composants fondamentaux suivants :

1. Substitutions simultanées de Stoughton : Les substitutions sont définies comme des fonctions de variables vers des $\lambda$-termes ($Sub = V \to \Lambda$). L'opération $M \bullet \sigma$ est définie par récursion structurelle. Pour les abstractions $\lambda$ et les types $\Pi$, la variable liée est renommée en un nouveau nom $y$ choisi par une fonction $X$, et la substitution est mise à jour pour mapper l'ancienne variable liée vers ce nouveau nom. Cela garantit qu'un seul appel récursif est nécessaire par abstraction, maintenant la primitive récursivité.
2. Relations $\alpha$-commutatives : Les auteurs développent une théorie des relations qui commutent avec la conversion $\alpha$. Une relation $S$ est $\alpha$-commutative si $M \sim_\alpha N$ et que $N S P$ implique l'existence d'un $Q$ tel que $M S Q$ et $Q \sim_\alpha P$. Ce cadre permet aux auteurs de traiter la confluence à la conversion $\alpha$ de manière propre, évitant la duplication de lemmas souvent observée dans d'autres formalisations.
3. Révision de la preuve de confluence par Takahashi : Au lieu de la preuve originale de Tait et Martin-Löf, l'article emploie la révision de Takahashi utilisant la réduction parallèle ($\Rightarrow$). Les auteurs définissent la réduction parallèle sans règles explicites de conversion $\alpha$ dans les étapes de réduction, s'appuyant plutôt sur la propriété du pentagone (une généralisation de la propriété du diamant jusqu'à la conversion $\alpha$) pour prouver la confluence.
4. Hypothèse de Normalisation : La preuve de consistance suppose que le PTS spécifique considéré est normalisant (chaque terme bien typé est faiblement normalisant). Les auteurs notent que prouver la normalisation pour des systèmes imprédicatifs au sein d'Agda est probablement impossible en raison de l'absence d'imprédicativité de la méta-langue d'Agda.

Contributions Clés
L'article présente des preuves formelles pour trois propriétés méta-théoriques majeures :

1. Confluence de la réduction $\beta$ : Les auteurs prouvent le théorème de Church-Rosser pour la syntaxe sous-jacente du PTS. En utilisant la théorie des relations $\alpha$-commutatives et la réduction parallèle de Takahashi, ils établissent que la clôture étoile de la réduction parallèle coïncide avec la réduction $\beta$ à plusieurs étapes et satisfait la propriété du pentagone.
2. Réduction de Sujet (SR) : L'article formalise la préservation du typage sous la réduction. Suivant les idées de McKinna et Pollack, les auteurs étendent les réductions aux contextes et prouvent un théorème simultané concernant la validité des contextes et la préservation du typage pour les sujets. Cela inclut la preuve de l'injectivité du produit, un lemme crucial pour l'inversion.
3. Consistance pour le PTS Imprédicatif : Les auteurs prouvent que pour une sous-classe spécifique de PTS imprédicatifs (ceux satisfaisant des axiomes et des règles spécifiques, tels que $(\ast, \square) \in \mathcal{A}$ et $(\square, \ast, \ast) \in \mathcal{R}$), le type $\Pi[x : s]x$ (représentant la fausseté sous le principe de Curry-Howard) est inoccupé dans le contexte vide. La preuve étend la preuve de Coquand sur papier pour le Calcul des Constructions (CC). Elle repose sur la correction et la complétude des formes normales et neutres définies de manière inductive, les lemmas d'inversion et l'hypothèse de normalisation.

Résultats et Évaluation

• Taille de la formalisation : L'ensemble du développement comprend environ 4 300 lignes de code (LoC), dont 3 000 LoC sont attribuées au cadre sous-jacent des substitutions de Stoughton et de la syntaxe PTS provenant de travaux antérieurs.
• Comparaison : Les auteurs comparent leur travail à des formalisations utilisant les indices de de Bruijn (Barras et Werner, ~2 900 LoC) et la syntaxe localement sans nom (Aydemir et al., ~4 800 LoC). Ils soutiennent que leur approche est comparable en taille mais offre une transparence supérieure concernant la syntaxe utilisée, car elle reflète étroitement les présentations mathématiques informelles (par exemple, le lemme de faiblesse ressemble presque identiquement à la notation classique).
• Faisabilité : Les résultats suggèrent que l'approche utilisant la syntaxe classique et les substitutions simultanées est faisable pour les théories des types dépendants. Les auteurs notent que seuls quelques lemmas ont nécessité l'induction bien fondée, et que la taille du code n'a pas « explosé ».

Signification et Revendications
L'article affirme que l'approche utilisant les substitutions de Stoughton offre une « présentation et un traitement plus clairs » des problèmes méta-théoriques par rapport à des développements similaires, particulièrement concernant la gestion de la conversion $\alpha$. Les auteurs affirment que leur solution est plus transparente pour les lecteurs humains que les approches localement sans nom ou de Bruijn, car elle évite l'« encombrement notationnel » de l'ouverture des termes et la gestion manuelle des paramètres frais.

La signification du travail réside dans la démonstration qu'une preuve de consistance mécanisée pour des systèmes imprédicatifs est réalisable sans abandonner la syntaxe classique, à condition que la normalisation soit supposée. Les auteurs reconnaissent modestement qu'une mécanisation complète de la normalisation pour les théories imprédicatives est probablement impossible dans Agda en raison des limitations de la force de preuve (implications du théorème d'incomplétude de Gödel), mais la preuve de consistance elle-même reste une étape substantielle vers des algorithmes de typage correct-par-construction pour de tels systèmes. Ce travail sert de validation de l'utilité du cadre pour les formalisations futures des théories des types dépendants.