Constructing (Co)inductive Types via Large Sizes

1. Énoncé du problème

Les assistants de preuve (par exemple Agda, Lean, Rocq) reposent sur la théorie des types dépendants pour assurer la cohérence et la décidabilité. Une exigence critique est que toutes les fonctions récursives doivent être totales (terminantes) et que toutes les fonctions corecursives doivent être productives.

• Limitations actuelles : La plupart des systèmes imposent la totalité via des vérifications syntaxiques (par exemple, récursion structurelle ou terminaison par changement de taille). Ces vérifications sont souvent restrictives, non modulaires et sensibles au refactorisation du code.
• Types de tailles : Une alternative basée sur les types utilise des « tailles » (ordinaux) pour annoter les types, permettant de prouver la terminaison par induction bien fondée sur la taille.
• L'incohérence d'Agda : Agda implémente les types de tailles mais introduit une plus grande taille ($\infty$) pour définir le type inductif/coinductif complet comme son approximation à $\infty$. Cela conduit à une incohérence logique : le système prouve $\infty < \infty$, violant l'irréflexivité des ordres bien fondés stricts.
• Travaux théoriques précédents : Les tentatives antérieures pour corriger cela en utilisant des quantificateurs paramétriques (existantiel $\exists$ pour l'inductif, universel $\forall$ pour le coinductif) étaient limitées. Plus précisément, elles ne pouvaient construire que des types inductifs à branches finies car le type de taille était interprété comme l'ensemble des nombres naturels ($\mathbb{N}$), qui manque des ordinaux limites nécessaires aux structures à branches infinies.

Objectif : Construire une théorie des types cohérente qui supporte tous les types (co)inductifs (y compris ceux à branches infinies) en utilisant des types de tailles et des quantificateurs paramétriques, sans s'appuyer sur une plus grande taille incohérente.

2. Méthodologie

Les auteurs étendent la théorie des types de Martin-Löf (MLTT) avec des fonctionnalités spécifiques pour réaliser cette construction et prouver sa cohérence via un modèle de réalisabilité.

A. La théorie des types étendue

La théorie inclut les fonctionnalités standards de la MLTT (univers, $\Sigma$, $\Pi$, types d'identité) plus :

1. Un type de tailles (Size) :
   • Équipé d'un zéro ($0$) et d'un successeur ($\uparrow i$).
   • Ordonné par un préordre ($\leq$) encodé comme une simple proposition.
   • Crucialement : Size est un type grand (non dans l'univers $U$), mais la quantification sur celui-ci peut produire des types petits.
2. Quantificateurs paramétriques :
   • $\exists i. A(i)$ (Existentiel) : Représente l'union des approximations. Les termes sont des paires $\langle s, a \rangle$, mais la taille $s$ est abstraite (ne peut pas être utilisée dans un filtrage par motif). L'élimination est restreinte aux types petits.
   • $\forall i. A(i)$ (Universel) : Représente l'intersection des approximations. Les fonctions agissent uniformément sur n'importe quelle taille.
   • Axiomes de paramétricité : La théorie inclut des axiomes stipulant que ces quantificateurs commutent avec les constructeurs de types (par exemple, $\Pi x:A. \exists i. B(x,i) \simeq \exists i. \Pi x:A. \exists j < i. B(x,j)$). Cela internalise l'idée que les tailles sont traitées uniformément.
3. Induction bien fondée (fix) :
   • Un opérateur de point fixe permettant la définition par induction sur les tailles : $fix\ f : \forall i. A(i)$ étant donné $f : \forall i. ((\forall j < i. A(j)) \to A(i))$.
   • La règle $\beta$ est propositionnelle (et non définitionnelle) pour préserver la décidabilité du typage.

B. Construction des types (co)inductifs

Les auteurs encodent les types (co)inductifs comme des algèbres initiales et des coalgèbres finales pour des endofoncteurs polynomiaux ($F$).

1. Approximations ordinales : Ils définissent des foncteurs indexés par la taille $F[\exists -]$ et $F[\forall -]$. En utilisant l'opérateur fix, ils construisent des algèbres initiales ($\mu_3 F$) et des coalgèbres finales ($\nu_2 F$) pour ces foncteurs indexés par la taille. Ceux-ci représentent le type tronqué à une taille spécifique.
2. Types complets via quantification :
   • Types inductifs : Définis comme $\mu F := \exists i. (\mu_3 F) i$. Le quantificateur existentiel rassemble tous les termes bornés par une certaine taille.
   • Types coinductifs : Définis comme $\nu F := \forall i. (\nu_2 F) i$. Le quantificateur universel garantit que les termes sont observables à n'importe quelle profondeur.
3. Gestion des types à branches infinies : L'innovation clé consiste à montrer que les foncteurs polynomiaux commutent faiblement avec le quantificateur existentiel. Cela nécessite l'existence d'ordinaux limites (supremums de suites de tailles), ce qui est impossible si les tailles ne sont que $\mathbb{N}$.

C. Preuve de cohérence : Modèle de réalisabilité

Pour prouver que la théorie est cohérente, les auteurs construisent un modèle de réalisabilité basé sur le Topos Effectif de Hyland.

• Interprétation des types :
  • Types petits : Interprétés comme des Relations d'Équivalence Partielles (PER) sur les nombres naturels (données calculables).
  • Types grands : Interprétés comme des Assemblages (ensembles avec des relations de calculabilité).
• Interprétation de Size :
  • Le type Size est interprété comme $\nabla \omega_1$, où $\omega_1$ est le premier ordinal non dénombrable (l'ensemble de tous les ordinaux dénombrables).
  • Il est muni de la relation de réalisabilité « complète », ce qui signifie que les morphismes doivent traiter toutes les tailles uniformément (paramétricité).
• Validation :
  • Parce que $\omega_1$ contient des ordinaux limites, le modèle valide les axiomes de paramétricité requis pour les types inductifs à branches infinies.
  • Le modèle valide l'Impredicativité (quantifier sur des types grands produit des types petits) et l'Unicité des Preuves d'Identité (UIP), même si la syntaxe ne les suppose pas. Cela démontre que la syntaxe est compatible avec des théories plus fortes (comme la théorie des types homotopique) sans en être restreinte.

3. Contributions clés

1. Construction générale des types (co)inductifs : Contrairement aux approches paramétriques précédentes limitées aux types à branches finies, ce travail construit tous les types (co)inductifs, y compris ceux à branches infinies (par exemple, les ordinaux de Brouwer, les modèles de la théorie des ensembles constructifs).
2. Résolution de l'incohérence d'Agda : En remplaçant la « plus grande taille » incohérente ($\infty$) par des quantificateurs paramétriques sur un type grand de tailles, les auteurs fournissent une alternative cohérente à l'implémentation actuelle d'Agda.
3. Quantificateurs paramétriques comme mécanisme : Ils démontrent que l'internalisation de la paramétricité via $\exists$ et $\forall$ sur les tailles impose efficacement l'abstraction nécessaire pour prévenir les comportements non terminants et les incohérences logiques.
4. Modèle de réalisabilité robuste : La construction d'un modèle où Size est interprété comme $\omega_1$ fournit une justification sémantique rigoureuse de la théorie, prouvant que les axiomes de paramétricité sont cohérents.

4. Résultats

• Validité théorique : Le papier prouve que l'algèbre initiale et la coalgèbre finale pour tout endofoncteur polynomial existent au sein de la théorie étendue.
• Cohérence : Le modèle de réalisabilité confirme que la théorie est cohérente. Il montre que les axiomes pour les quantificateurs paramétriques tiennent lorsque les tailles sont interprétées comme un ordinal non dénombrable.
• Compatibilité : Les constructions ne reposent pas sur l'UIP ou l'imprédicativité dans la syntaxe, rendant les résultats compatibles avec la théorie des types homotopique (HoTT), malgré le fait que le modèle satisfasse ces propriétés.

5. Importance et travaux futurs

• Impact sur les assistants de preuve : Ce travail offre une voie pour implémenter des types de tailles dans les assistants de preuve (comme Agda) sans l'incohérence actuelle causée par la taille $\infty$. Il permet une vérification de terminaison plus modulaire et compositionnelle.
• Comportement computationnel : Les auteurs reconnaissent que, bien que la théorie soit cohérente, la syntaxe actuelle manque de comportement computationnel pour les axiomes de paramétricité (ce sont des axiomes, pas des règles de réduction). Les travaux futurs doivent relier cela à la paramétricité interne (par exemple, via des types ponts ou la théorie des types cubiques) pour assurer la décidabilité et la canonicité en pratique.
• Décidabilité de l'inégalité : Le modèle implique que l'inégalité sur les tailles n'est pas généralement décidable (en raison des supremums). Les auteurs suggèrent une approche hybride (inégalité définitionnelle vs propositionnelle) pour une implémentation pratique.
• Généralisation : Le modèle pourrait potentiellement être généralisé à d'autres algèbres combinatoires partielles ou intégré avec des effets et l'univalence.

En résumé, le papier comble avec succès le fossé entre le besoin théorique de types de tailles paramétriques et l'exigence pratique de cohérence, permettant la construction de types (co)inductifs complexes dans un cadre de théorie des types sain.