💻 computer science

Directed proof-relevant logical relations in simplicial HoTT

Cet article développe un cadre dirigé et pertinent pour la preuve des relations logiques au sein de la théorie des types homotopiques simpliciaux en internalisant les réductions sous forme de types d'inégalité et en utilisant des familles contravariantes pour construire des modèles qui prouvent la canonicité booléenne dirigée et l'indépendance de la représentation pour les types dépendants.

Auteurs originaux : Runming Li, Harrison Grodin, Robert Harper

Publié 2026-07-10

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Runming Li, Harrison Grodin, Robert Harper

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 un château LEGO géant et magique. Dans le monde de l'informatique, ce château est une « théorie des types » — un ensemble de règles sur la façon dont les programmes sont construits et dont ils se comportent. Habituellement, quand les informaticiens vérifient si un programme fonctionne, ils regardent les briques finies et demandent : « Est-ce que ces deux briques sont exactement les mêmes ? » Si elles le sont, ils les considèrent comme identiques. C'est comme dire que deux structures LEGO sont les mêmes si elles sont identiques de l'extérieur.

Mais dans cet article, les auteurs, Runming Li, Harrison Grodin et Robert Harper, posent une question différente : Et si nous nous soucions du processus de construction ? Et si nous voulions suivre non seulement la forme finale, mais aussi le fait qu'une brique est devenue une autre par réduction ? Cette « transformation » est appelée réduction, et elle a une direction : la grande va vers la petite, mais la petite ne peut pas redevenir magiquement grande.

Le Problème : L'Énigme du « Retour en Arrière »

Dans l'ancienne méthode (utilisant la logique « équationnelle »), les scientifiques traitaient la réduction comme une rue à double sens. Si la Brique A se transforme en Brique B, ils disaient simplement « A égale B ». Cela rendait les mathématiques faciles, mais cela ignorait la direction du flux. C'est comme dire que « marcher pour aller au magasin » est la même chose que « marcher pour rentrer à la maison ». C'est vrai que l'on arrive au même endroit, mais le voyage est différent !

Les auteurs ont réalisé que pour prouver qu'un programme est « calculable » (c'est-à-dire qu'il finira par s'arrêter et donner une vraie réponse), il faut être capable de marcher en arrière le long de ce voyage. Si vous savez que la brique finale, parfaite, est bonne, vous devez prouver que la brique encombrante et désordonnée qui s'est transformée en elle était également bonne. C'est ce qu'on appelle la propriété d'« expansion ».

La Solution : Une Rue à Sens Unique avec une Carte Magique

Les auteurs ont construit un nouveau genre de jeu de LEGO en utilisant un cadre appelé Théorie des Types Homotopiques Simpliciaux. Considérez cela comme un terrain de jeu spécial où ils peuvent dessiner des flèches à sens unique (inégalités) au lieu de simples signes d'égalité.

Voici le tour de magie qu'ils ont découvert :

La Direction : Ils ont remplacé « égal » par « inférieur ou égal à » (≤). Ainsi, si un terme se réduit, il passe de $A \le B$ . C'est une rue à sens unique.
La Marche en Arrière : Pour prouver que les choses fonctionnent en marche arrière, ils avaient besoin d'une carte spéciale. En mathématiques, cela s'appelle une famille contravariante.
- L'Analogie : Imaginez que vous avez un sac à dos rempli de « preuves » (comme des billets de concert). Si vous marchez vers l'avant le long de la rue à sens unique, vous pourriez perdre vos billets. Mais cette carte spéciale est une machine à remonter le temps. Si vous avez un billet pour la destination ( $B$ ), la carte génère automatiquement un billet valide pour le point de départ ( $A$ ).
- L'article prouve que dans leur nouveau système, cette « machine à remonter le temps » n'est pas seulement un coup de chance ; elle est intégrée dans la structure même des mathématiques. C'est une machine « sensible à la preuve » (proof-relevant), ce qui signifie que le billet lui-même porte une petite note expliquant comment il a été généré, et pas seulement qu'il existe.

Le Grand Succès : La Canonicité Booléenne

Pour démontrer que cela fonctionne, ils l'ont testé sur le bloc de construction le plus simple de la logique : les Booléens (Vrai et Faux).

L'Objectif : Ils voulaient prouver que si l'on part de n'importe quel terme booléen fermé (un programme qui n'a pas besoin d'aide extérieure), il finira par se « réduire » (se transformer) en true ou false.
Le Résultat : Ils ont prouvé que chaque terme de ce type se réduit vers une réponse canonique. C'est comme garantir que, peu importe à quel point vos instructions LEGO sont désordonnées, si vous suivez les règles, vous finirez par obtenir une brique parfaite et reconnaissable. Ils n'ont pas seulement dit que « ça devrait probablement marcher » ; ils ont construit une preuve mathématique rigoureuse que cela doit fonctionner.

Ce qu'ils n'ont pas fait (et ce qu'ils ont évité)

Il est important de savoir ce que cet article ne prétend pas :

Pas d'Égalité Magique : Ils rejettent explicitement l'idée que l'on puisse simplement prétendre que la réduction est la même chose que l'égalité. Ils soutiennent que traiter la « réduction » comme une « égalité » fait perdre la directionnalité nécessaire à leur preuve.
Pas Juste une Simulation : Il ne s'agit pas d'une simulation informatique ou d'une supposition. Ils ont construit un modèle mathématique formel et prouvé des théorèmes à son sujet. Ils ont même écrit un programme informatique (dans un langage appelé Cubical Agda) pour vérifier les parties simples de leur logique, agissant comme une « preuve de concept ».
Pas encore un Univers Complet : Bien qu'ils aient prouvé que cela fonctionne pour des types simples (comme les booléens et les paires) et qu'ils aient même commencé sur des « types dépendants » complexes (où les types peuvent dépendre des valeurs), la version complète, avec tous ses attributs, est encore un travail en cours. Ils ont montré que la voie est libre, mais que toute la montagne n'est pas encore gravie.

La Modalité « Plate » : Un Filtre Spécial

Lorsqu'ils ont essayé d'ajouter des « Univers » (une boîte qui contient d'autres boîtes de types), ils ont rencontré un obstacle. Les flèches à sens unique étaient devenues trop complexes à gérer.

La Correction : Ils ont introduit une « modalité plate » (notée par un symbole comme ♭). Considérez cela comme un filtre de discrétisation. Cela prend une rue à sens unique un peu floue et la force à devenir une rue à double sens nette, uniquement dans le but de vérifier si les types sont les mêmes. C'est comme porter des lunettes spéciales qui font disparaître la direction juste assez longtemps pour comparer deux briques, puis les retirer pour voir à nouveau la direction. Cela leur a permis de gérer les règles complexes des « univers » sans briser la logique de leur rue à sens unique.

La Vision Globale : L'Indépendance de la Représentation

Enfin, ils ont montré que cette méthode fonctionne pour les relations logiques binaires. C'est comme vérifier si deux ensembles LEGO différents (peut-être un fait de plastique, l'autre de bois) peuvent accomplir le même travail.

Ils ont séparé le mouvement « vertical » (comment un ensemble unique change au fil du temps) du mouvement « horizontal » (comment deux ensembles différents se rapportent l'un à l'autre).
En gardant ces éléments séparés, ils ont prouvé que vous pouvez remplacer les composants internes d'un programme (la « représentation ») sans changer ce que fait le programme (l'« interface »). C'est le cœur mathématique de l'« indépendance de la représentation », un concept crucial pour écrire des logiciels fiables.

Résumé

En bref, Li, Grodin et Harper ont construit un nouveau terrain de jeu mathématique où la direction compte. Ils ont montré qu'en traitant la réduction de programme comme une rue à sens unique et en utilisant une « carte inversée » spéciale (la contravariance), on peut prouver rigoureusement que les programmes finiront toujours par s'arrêter et donner une vraie réponse. Ils ne se sont pas contentés de le suggérer ; ils l'ont prouvé pour des cas simples et ont tracé le plan pour les cas complexes, tout en gardant les détails désordonnés de « comment » la réduction se produit au centre même des mathématiques.

Résumé technique : Relations logiques dirigées et pertinentes pour la preuve dans le cadre de la HoTT simpliciale

Énoncé du problème
Les relations logiques traditionnelles pertinentes pour la preuve (souvent formulées via le collage catégorique) interprètent les types comme des familles de termes calculables, où les prédicats de calculabilité sont des familles de types plutôt que de simples propositions. Dans les présentations équationnelles de la théorie des types, l'égalité jugée est représentée par une égalité au niveau méta, et les relations logiques reposent sur un lemme de « clôture sous expansion » : si un terme $M$ se réduit en $M'$ , et que $M'$ est calculable, alors $M$ est calculable. Cependant, cette approche traite le calcul comme une relation symétrique (via l'égalité) ou repose sur des preuves manuelles de clôture vers l'arrière. Elle n'internalise pas nativement la nature dirigée de la réduction, où les termes passent à d'autres termes ( $M \to M'$ ) mais pas nécessairement l'inverse. Cet article traite le défi de la construction d'une relation logique dirigée qui rend compte des réductions dirigées de manière interne, sans dépendre de relations de réduction externes ou de lemmes d'expansion non pertinents pour la preuve.

Méthodologie
Les auteurs développent leur cadre au sein de la théorie des types homotopiques (HoTT) simpliciale, une extension dirigée de la HoT qui inclut un intervalle dirigé et des types d'inégalité ( $x \leq_A y$ ).

Syntaxe dirigée via des QIIT dirigées :
La syntaxe du langage-objet est présentée comme un type inductif-inductif quotient dirigé (QIIT dirigé). Contrairement aux QIIT standards qui quotientent par des égalités jugées (constructeurs de chemins), cette syntaxe inclut des constructeurs dirigés qui génèrent des types d'inégalité. Par exemple, la $\beta$ -réduction pour les produits est internalisée comme une inégalité :
$\times\beta_1 : \text{fst}(\text{pair } a \, b) \leq a$
La syntaxe est construite pour être un « type de Segal mince », garantissant que les réductions composent et que les inégalités entre les mêmes extrémités sont uniques (non pertinentes pour la preuve), modélisant ainsi un préordre plutôt qu'une catégorie générale.
La contravariance comme expansion pertinente pour la preuve :
L'intuition théorique centrale est que les familles contravariantes dans la théorie des types simpliciale fournissent la structure exacte nécessaire pour la clôture pertinente pour la preuve sous expansion. Dans ce cadre, un prédicat de calculabilité $A^\bullet$ pour un type $A$ n'est pas seulement une famille de types ; il doit être une famille contravariante.
- Définition : Une famille $C: X \to \mathcal{U}$ est contravariante si pour toute inégalité $f: x \leq_X y$ et tout témoin $v: C(y)$ , le type des élévations $\sum_{u:C(x)} u \leq_{C(f)} v$ est contractile.
- Implication : Cette contractilité garantit une opération de « transport vers l'arrière » unique et fonctorielle $f^*: C(y) \to C(x)$ . Cette opération internalise le lemme d'expansion : l'évidence de calculabilité peut être transportée vers l'arrière le long des réductions de manière à respecter automatiquement les identités et la composition.
Gestion des types dépendants et des univers :
L'extension à cela introduit un conflit : la conversion de type nécessite une égalité symétrique, tandis que la syntaxe ne fournit que des inégalités dirigées.
- Discrétisation : Les auteurs discrétisent l'univers des types ($Ty$) en ajoutant un constructeur qui transforme les inégalités de types en égalités ( $A \leq Ty B \implies A = Ty B$ ). Cela permet la conversion de type standard tout en préservant les réductions dirigées pour les termes.
- Modalité plate : Pour maintenir la pertinence pour la preuve des prédicats d'univers sans perdre la discrétisation, les auteurs emploient la modalité plate ( $\flat$ ) issue de la théorie des types crispée. Les prédicats de calculabilité pour les univers sont stockés sous forme de codes plats. Puisque $\flat X$ est discret, les inégalités entre prédicats s'effondrent en égalités, assurant l'unicité requise pour le témoin de calculabilité de l'univers.

Contributions clés

Syntaxe quotient dirigée : Une formalisation de la syntaxe de la théorie des types où les réductions jugées sont internalisées comme des inégalités dirigées via des QIIT dirigées.
Contravariance comme expansion : L'identification des familles contravariantes dans la théorie des types simpliciale comme la généralisation pertinente pour la preuve de l'lemme d'expansion, fournissant une fonctorialité intégrée et des propriétés universelles pour le transport vers l'arrière.
Relation logique unaire : Une construction d'un modèle de relation logique unaire qui prouve la canonicité booléenne dirigée : tout terme booléen fermé $M$ satisfait $M \leq \text{true}$ ou $M \leq \text{false}$ .
Mécanisation : Une preuve de concept mécanisée dans Cubical Agda pour le fragment simplement typé (produits, fonctions, booléens), démontrant la faisabilité de l'approche dirigée.
Extension aux types dépendants et aux univers : Une solution pour les types dépendants utilisant la discrétisation des types et la modalité plate pour gérer les prédicats d'univers.
Parametricité binaire : Une adaptation de la méthode aux relations logiques binaires, séparant les réductions verticales (contravariance) de la parametricité horizontale, illustrée par un argument d'indépendance de la représentation pour les files d'attente (queues).

Résultats

Canonicité dirigée : Le théorème fondamental des relations logiques est établi pour le cadre dirigé. Pour tout terme booléen fermé $M$ , le modèle produit un témoin que $M$ se réduit à un booléen canonique.
Indépendance de la représentation : La relation logique binaire sépare avec succès la dimension verticale (réduction/contravariance) de la dimension horizontale (parametricité), permettant des comptes pertinents pour la preuve de l'indépendance de la représentation où la relation est un span plutôt qu'un zig-zag.
Mécanisation : Le fragment simplement typé, incluant la construction de la syntaxe dirigée et du modèle de relation logique, a été formalisé dans Cubical Agda.

Signification et affirmations
L'article affirme fournir une internalisation de type théorique de l'idée que les relations logiques doivent valider la canonicité et la parametricité même lorsque la syntaxe est présentée par des réductions plutôt que par des égalités.

Unification théorique : Il unifie la vue opérationnelle du calcul (réduction dirigée) avec la vue sémantique des relations logiques (collage pertinent pour la preuve) en exploitant la structure dirigée native de la théorie des types simpliciale.
Nouveau rôle pour la contravariance : Il élève les familles contravariantes du statut d'outil pour la théorie des catégories synthétiques à celui de mécanisme fondamental pour les relations logiques, remplaçant les lemmes d'expansion ad hoc par une propriété universelle.
Modestie : Les auteurs notent que le résultat est « peu surprenant » dans sa conclusion (les relations logiques doivent fonctionner pour les réductions) mais significatif dans son internalisation. Ils reconnaissent que l'extension aux types dépendants présente des défis de transport importants et que la mécanisation actuelle est limitée au cas simplement typé. Ils ne prétendent pas avoir résolu tous les problèmes concernant les types d'identité dans les cadres dirigés, suggérant des travaux futurs impliquant des distinctions de phase ou des modalités monadiques.

Le travail démontre que la théorie des types simpliciale est non seulement un outil pour la théorie des $\infty$ -catégories synthétiques, mais aussi une métathéorie viable pour raisonner sur la sémantique de réduction des langages de programmation et des théories de types.