💻 computer science

Definitional Inversion, Without Normalisation

Cet article introduit une nouvelle technique de preuve de théorie des domaines qui établit des propriétés d'inversion définitionnelle pour les systèmes de types dépendants sans recourir à la normalisation, permettant ainsi l'analyse méta-théorique de systèmes non normalisants comme Idris et Lean ainsi que de ceux possédant le type-dans-le-type.

Auteurs originaux : Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich

Publié 2026-07-16

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich

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 construisez une bibliothèque magique et immense où chaque livre est une preuve mathématique, et où les étagères elles-mêmes sont faites de logique. C'est le monde des systèmes de types dépendants, le moteur secret derrière les assistants de preuve modernes comme Lean et les langages de programmation comme Idris. Dans ce monde, les règles sont incroyablement strictes : si vous essayez de poser un « chat » sur une étagère étiquetée « nombres », le système de sécurité de la bibliothèque (le vérificateur de types) doit immédiatement hurler « Erreur ! » et vous arrêter. Cette sécurité repose sur un concept appelé égalité définitionnelle, qui est la façon dont la bibliothèque décide si deux choses sont essentiellement les mêmes. Par exemple, est-ce qu'un « carré » est simplement un « rectangle avec des côtés égaux » ? Si le système dit oui, il les traite comme identiques.

Cependant, vérifier ces règles est délicat. Traditionnellement, pour prouver que la bibliothèque est sûre, les mathématiciens devaient montrer que chaque livre pouvait être simplifié jusqu'à sa forme la plus simple et la plus basique (un processus appelé normalisation). Mais de nombreuses bibliothèques modernes et puissantes sont conçues pour être infinies ou autoréférentielles, ce qui signifie qu'elles ne peuvent pas être simplifiées jusqu'à un arrêt final. C'est comme essayer d'aplatir une fractale ; on continue de trouver plus de détails. Pendant longtemps, si un système ne pouvait pas être simplifié, nous ne pouvions pas prouver qu'il était sûr. Ce papier introduit une nouvelle façon de vérifier la sécurité de la bibliothèque sans avoir besoin d'aplatir la fractale d'abord.

Le Puzzle Infini et le Miroir Magique

Considérez un système de types dépendants comme un puzzle géant qui s'auto-vérifie. Les pièces sont des types (comme « nombres » ou « fonctions »), et l'objectif est de s'assurer que lorsque l'on emboîte deux pièces, elles s'ajustent parfaitement. La règle la plus critique dans ce puzzle est l'inversion définitionnelle. C'est la logique qui dit : « Si deux structures complexes se ressemblent, leurs parties doivent aussi être les mêmes. » Par exemple, si vous avez deux types de fonctions qui sont identiques, le papier prouve que leurs types d'entrée et de sortie doivent également être identiques. Ceci est crucial car cela permet à l'ordinateur de décomposer en toute sécurité des codes complexes en morceaux plus petits sans s'embrouiller.

Pendant des décennies, la seule façon de prouver que ces pièces s'emboîtaient était d'utiliser une méthode appelée confluence (vérifier si différents chemins de simplification mènent au même résultat) ou les relations logiques (une façon complexe de comparer comment les termes se comportent). Mais ces anciens outils ont heurté un mur. La confluence s'effondre lorsqu'on ajoute certaines règles « extensives » (comme les lois $\eta$ , qui disent qu'une fonction est définie entièrement par ce qu'elle fait, et non par la façon dont elle est écrite). Les relations logiques nécessitent généralement que le système soit « normalisant » (capable de s'arrêter de simplifier), ce qui exclut de nombreux langages de programmation réels et puissants qui permettent des boucles infinies ou des types autoréférentiels.

La Nouvelle Approche : Une Carte des Possibilités

Les auteurs, une équipe de chercheurs en informatique et en mathématiques, proposent une nouvelle stratégie basée sur la théorie des domaines. Au lieu d'essayer de forcer les pièces du puzzle à se simplifier en une forme finale unique, ils construisent une carte de tous les comportements possibles.

Imaginez que vous essayiez d'identifier une créature mystérieuse dans une forêt obscure.

L'Ancienne Méthode : Vous attendez que la créature s'arrête de bouger pour révéler sa véritable forme finale. Si la créature ne s'arrête jamais de bouger (parce qu'elle est dans une boucle infinie), vous ne pouvez pas l'identifier, et la forêt est jugée dangereuse.
La Nouvelle Méthode : Vous n'attendez pas que la créature s'arrête. Au lieu de cela, vous observez ses empreintes. Vous notez qu'elle laisse une empreinte de « pied gauche », puis une emprement de « pied droit », puis un « pied gauche » à nouveau. Même si la créature ne s'arrête jamais de marcher, vous pouvez toujours déduire sa forme en observant le motif de ses pas.

Dans le langage du papier, ces « empreintes » sont appelées éléments compacts ou observations finies. Les auteurs construisent un « domaine » mathématique (un espace structuré) où chaque type est représenté non pas par une réponse finale, mais par l'ensemble de toutes les choses finies que l'on peut observer à son sujet. Ils utilisent une technique appelée projecteurs finitaires pour découper ce domaine en morceaux gérables.

Ce Qu'Ils Ont Trouvé

En utilisant cette méthode d'« empreintes », l'équipe a prouvé avec succès que l'inversion définitionnelle est vraie, même dans des systèmes qui :

Ne s'arrêtent jamais de se simplifier (non-normalisants), tels que ceux avec une règle de « type-dans-type » (où un type peut se contenir lui-même).
Incluent des lois $\eta$ , qui sont des règles complexes faisant en sorte que les fonctions et les paires se comportent de manière plus intuitive mais qui brisent les méthodes de preuve traditionnelles.

Ils ont démontré cela sur une petite version centrale d'une théorie de types appelée MLTT $\eta$ (Théorie des Types de Martin-Löf avec lois $\eta$ ). Ils ont montré que même dans ce système chaotique et potentiellement infini, si deux types sont égaux, leurs blocs de construction doivent aussi être égaux. C'est un événement majeur car cela prouve que le « filet de sécurité » du système de types fonctionne même lorsque le système est autorisé à être désordonné et infini.

Pourquoi Cela Importe

Les auteurs n'ont pas seulement résolu un puzzle pour un petit système de démonstration ; ils ont montré que leur méthode est robuste. Ils ont étendu leur preuve pour inclure :

Les sommes dépendantes (paires de données).
Les types unités (un type avec une seule valeur).
Les combinateurs de point fixe (outils permettant la récursion infinie).
Les entiers naturels avec le pattern matching.
Les types d'identité (prouver que deux choses sont les mêmes).
Les propositions d'irrélevance de preuve (où le contenu d'une preuve n'importe pas, seul son existence compte).

Ils ont même construit un modèle pour un « univers de propositions strictes », montrant que leur technique peut gérer les fonctionnalités complexes présentes dans des outils réels comme Lean, Agda et Rocq.

Les Limites et l'Avenir

Le papier est très clair sur ce qu'il ne fait pas. Il ne prouve pas que ces systèmes sont « normalisants » (qu'ils s'arrêtent toujours). En fait, il travaille explicitement pour des systèmes qui ne s'arrêtent pas. Il ne résout pas non plus le problème des « neutres » (des variables qui n'ont pas encore été remplies) de la même manière qu'il résout celui des termes fermés, bien qu'il suggère comment cela pourrait être fait à l'avenir.

Les auteurs ont déjà transformé leurs preuves mathématiques en code, les vérifiant trois fois dans trois assistants de preuve différents (Agda, Lean et Rocq). Cela suggère que leur méthode n'est pas seulement une idée théorique, mais un outil pratique.

L'Essentiel à Retenir

Ce papier est comme si l'on tendait aux bâtisseurs de la bibliothèque magique de nouvelles lunettes. Avant, ils ne pouvaient vérifier la sécurité de la bibliothèque que si les livres étaient statiques et terminés. Désormais, ils peuvent vérifier la sécurité de livres qui sont encore en cours d'écriture, ou de livres qui se réfèrent à eux-mêmes éternellement. En se concentrant sur le comportement observable (les empreintes) plutôt que sur la destination finale (l'arrêt), ils ont ouvert la porte à la vérification des systèmes de types les plus puissants, complexes et potentiellement infinis que nous puissions imaginer. Cela ouvre la voie à « Lean4Lean » et « MetaRocq » — des projets où les assistants de preuve vérifient leur propre code — rendant les outils que nous utilisons pour construire les mathématiques et les logiciels encore plus dignes de confiance.

Résumé Technique : Inversion Définitionnelle, Sans Normalisation

Problème
Les systèmes de types dépendants sous-tendent des assistants de preuve critiques (Agda, Lean, Rocq) et des langages de programmation (Idris, Haskell dépendant). L'établissement de leurs propriétés méta-théoriques, particulièrement les principes d'inversion définitionnelle (injectivité et absence de confusion des constructeurs de types), est essentiel pour prouver la correction, l'unicité des types et la vérification du noyau (kernel). Cependant, les outils méta-théoriques existants font face à de sévères limitations :

Approches basées sur la confluence : Elles peinent avec les fonctionnalités modernes comme les lois $\eta$ . Bien que la confluence fonctionne pour la réduction $\beta$ , le mélange avec la conversion typée et les lois $\eta$ (par exemple, pour les fonctions ou les paires) conduit souvent à des systèmes non-confluents ou nécessite des présentations complexes et non standard.
Approches basées sur la normalisation (Relations Logiques) : Les relations logiques traditionnelles reposent sur l'existence de formes normales. Elles échouent pour les théories de types non-normalisantes (courantes en pratique, par exemple avec Type:Type ou les combinateurs de point fixe). De plus, prouver la normalisation nécessite une logique ambiante plus forte que la logique de l'objet (impliquant souvent l'induction-récursion ou l'imprédicativité), ce qui rend impossible l'étude de la méta-théorie des assistants de preuve au sein de leurs propres structures (par exemple, Lean4Lean, MetaRocq).

L'article traite le cas spécifique de MLTT $\eta$ , une variante de la théorie des types de Martin-Löf avec des produits dépendants, des équations $\beta$ et $\eta$ , et un univers Type:Type. Ce système défie la confluence (à cause de $\eta$ ) et la normalisation (à cause de Type:Type), laissant ses propriétés d'inversion définitionnelle non prouvées.

Méthodologie
Les auteurs proposent une nouvelle technique de preuve basée sur la théorie des domaines, utilisant spécifiquement des projections finitaires. L'idée centrale est d'interpréter les types non pas par leurs formes normales (qui peuvent ne pas exister), mais par leur "comportement observable" via des éléments compacts dans un domaine de Scott.

Construction du Domaine : Les auteurs construisent un domaine $D$ $D$ comme la solution d'une équation de domaine récursive représentant les constructeurs de types ( $\Pi$ $Π$ , $\mathcal{U}$ $U$ , etc.). Le domaine est construit comme la limite d'une séquence croissante d'approximations finies ( $C_n$ $C_{n}$ ), où les éléments sont compacts (représentant des observations finies).
- Crucialement, le modèle identifie $\bot$ avec $\lambda x.\bot$ pour satisfaire les lois $\eta$ pour les fonctions, tout en gardant les constructeurs $\Pi$ distincts de $\mathcal{U}$ pour assurer la disjointness.
Typage Sémantique : Une relation de typage sémantique est définie sur les éléments compacts du domaine. Cette relation est formulée à l'aide de projecteurs finitaires (des applications continues $p: D \to D$ telles que $p(\alpha) \le \alpha$ et $p(p(\alpha)) = p(\alpha)$ ). Un type est interprété comme un projecteur finitaire, et un terme est lié à un type si sa dénotation est un point fixe de ce projecteur.
Relation Logique : Une relation logique est définie sur les termes syntaxiques et les témoins sémantiques (éléments compacts). Contra part aux relations logiques traditionnelles qui récursion sur les formes normales des types, cette relation récurse sur l'étape (stage) $n$ $n$ des éléments compacts et sur la structure du témoin sémantique.
- La relation gère les termes ouverts en interprétant les termes neutres comme $\bot$ , évitant ainsi la complexité de la quantification de style Kripke tout en supportant toujours l'inversion dans des contextes ouverts.
- La relation est définie jusqu'à la réduction de tête (head reduction), incorporant les règles $\beta$ et $\eta$ directement dans la structure de la relation logique.
Adéquation : Les auteurs prouvent un théorème d'adéquation : si deux termes sont définitionnellement égaux dans la syntaxe, ils sont liés dans la relation logique. Cela permet de dériver des propriétés syntaxiques (comme l'injectivité) à partir des propriétés sémantiques (disjointness des éléments du domaine).

Contributions Clés

Nouvelle Technique de Preuve : Une méthode de théorie des domaines pour prouver l'inversion définitionnelle (injectivité et absence de confusion) sans dépendre de la normalisation ou de la confluence.
Gestion de $\eta$ et de la Non-Normalisation : La technique prouve avec succès l'injectivité pour des systèmes avec des lois $\eta$ et Type:Type (ou des combinateurs de point fixe), une combinaison auparavant intraitable pour les méthodes standards.
Logique Ambiante Faible : La preuve ne repose que sur l'induction de base sur les entiers naturels, évitant les principes logiques forts (comme l'induction-récursion) requis pour les preuves de normalisation. Cela rend la méthode adaptée aux projets d'auto-vérification (par exemple, prouver les propriétés de Lean au sein de Lean).
Extensibilité : La technique est démontrée sur MLTT $\eta$ et montrée comme capable de passer à des théories plus riches incluant :
- Des sommes dépendantes ( $\Sigma$ ) et le type Unité ($1$) avec des lois $\eta$ .
- La récursion générale via un combinateur de point fixe ( $Y$ ).
- Les entiers naturels ( $\mathbb{N}$ ) avec le pattern matching.
- Les types d'identité ($Id$) avec transport.
- Un univers de propositions strictes ($Prop$) avec irrélevance de preuve définitionnelle.
Mécanisation : Les résultats sont mécanisés dans Agda, Lean et Rocq, couvrant les diverses extensions listées ci-dessus.

Résultats

Injectivité de $\Pi$ : L'article prouve que si $\Pi x:A.B \equiv \Pi x:A'.B'$ , alors $A \equiv A'$ et $B \equiv B'$ .
Disjointness : Les constructeurs de types sont disjoints (par exemple, $\Pi x:A.B \not\equiv \mathcal{U}$ ).
Subject Reduction et Progress : En tant que conséquences des principes d'inversion, les auteurs dérivent les théorèmes de progression (progress) et de préservation, établissant la correction du langage en tant que langage de programmation.
Échec de l'UIP : Le modèle démontre que l'Unicité des Preuves d'Identité (UIP/règle K) n'est pas dérivable dans ce système, car le modèle de domaine distingue les différentes preuves d'identité.

Signification
L'article affirme combler un "angle mort" de la méta-théorie des systèmes de types dépendants. En découplant l'inversion définitionnelle de la normalisation, la technique permet l'étude rigoureuse de systèmes non-normalisants et de systèmes possédant des théories équationnelles riches (comme $\eta$ ) qui sont prévalentes dans les assistants de preuve et les langages de programmation modernes.

Les auteurs positionnent ce travail comme une étape fondamentale pour des projets tels que Lean4Lean et MetaRocq, qui visent à vérifier la méta-théorie des assistants de preuve au sein de ceux-ci. Puisque ces projets ne peuvent pas supposer la normalisation de la logique de l'objet (en raison du second théorème d'incomplétude de Gödel), cette approche de théorie des domaines offre une voie viable pour vérifier les noyaux (kernels) et assurer la correction des algorithmes de typage sans nécessiter une logique ambiante plus forte. Les auteurs suggèrent également des applications potentielles pour les langages de programmation à types dépendants utilisant des fonctionnalités non-terminantes ou le typage graduel, là où la méta-théorie traditionnelle basée sur la terminaison échoue.