Non-Derivability Results in Polymorphic Dependent Type Theory

Cet article démontre, à l'aide de modèles contre-exemples, que les principes d'induction et de coinduction ne sont pas dérivables dans la théorie des types dépendants polymorphes ($\lambda$P2) pure, soulignant ainsi la nécessité cruciale de l'extensionnalité fonctionnelle pour prouver l'induction et l'impossibilité de définir des types quotients paramétriques ou d'obtenir une coinduction forte dans ce système de base.

L'essentiel

Voici une explication simple et imagée de l'article de Herman Geuvers, conçue pour un public non spécialiste.

Le Titre : Pourquoi certaines règles de construction sont impossibles à inventer

Imaginez que vous êtes un architecte de l'univers logique. Vous avez un kit de construction très puissant appelé λP2 (une sorte de langage mathématique pour construire des données et des preuves). Avec ce kit, vous pouvez construire des briques de base comme les nombres, les listes ou les arbres.

Cependant, il y a un problème : ce kit est comme une boîte à outils qui vous donne les briques, mais qui ne vous donne pas les instructions de montage. Vous pouvez construire un mur, mais vous ne pouvez pas prouver mathématiquement que ce mur est solide pour toutes les tailles possibles, à moins d'ajouter des outils supplémentaires.

L'auteur, Herman Geuvers, écrit cet article pour rendre hommage à Stefano Berardi (un grand ami et collègue) en répondant à une question cruciale : « Quelles pièces supplémentaires devons-nous ajouter à notre boîte à outils pour pouvoir construire des structures parfaites ? »

---

1. Le Problème : La "Recette" manquante

Dans ce monde logique, on peut définir ce qu'est un nombre (comme 0, 1, 2...) ou une liste infinie (comme un flux de données). Mais il manque une règle fondamentale appelée l'induction.

• L'analogie de l'escalier : Imaginez que vous voulez prouver que vous pouvez monter un escalier infini. Vous savez que vous pouvez monter la première marche (0) et que si vous êtes sur une marche, vous pouvez monter la suivante. Mais dans le système de base (λP2), vous ne pouvez pas prouver que vous pouvez atteindre n'importe quelle marche, aussi haute soit-elle. La "recette" pour monter l'escalier entier n'existe pas dans le kit de base.

Les chercheurs savaient déjà que pour les nombres, il manquait cette règle. Mais la question était : Est-ce qu'on peut aussi construire des "quotients" (des groupes de choses considérées comme égales) ou des "flux infinis" (des streams) avec les bonnes règles de sécurité, sans ajouter de nouveaux outils ?

2. La Réponse : "Non, pas sans outils supplémentaires"

Geuvers utilise une méthode très intelligente pour répondre : il construit des mondes de contrefaçon (des modèles).

Imaginez que vous voulez prouver qu'un certain type de voiture ne peut pas rouler sur la lune. Au lieu de construire une voiture et d'essayer de la lancer, vous créez un modèle théorique de la lune où la gravité est telle que aucune voiture ne peut avancer. Si vous montrez que dans ce monde spécial, la voiture est immobile, alors vous savez qu'elle ne peut pas être universelle.

Geuvers a créé de tels "mondes logiques" où :

1. Les Quotients Paramétriques n'existent pas : C'est comme essayer de faire un tamis universel qui trie n'importe quel type de sable. Il a montré que dans son modèle, un tel tamis ne peut pas être construit. Le système est trop rigide pour permettre cette généralisation.
2. Les Flux (Streams) ne sont pas "terminaux" : Imaginez un fleuve infini. En théorie, on pourrait dire que deux fleuves sont identiques s'ils coulent de la même façon. Geuvers montre que dans son modèle, on peut avoir deux fleuves qui semblent identiques à l'œil nu (ils ont la même eau au début), mais qui sont en réalité différents dans leur structure profonde. Le système ne permet pas de dire "ils sont égaux" simplement parce qu'ils se comportent pareil.

3. Le Secret : L'Extensionnalité des Fonctions

L'article explore ensuite ce qui se passe si on ajoute des outils modernes (inspirés de la "Théorie des Types Homotopique"). On ajoute :

• Des types d'identité (pour dire "c'est la même chose").
• Des types sommes (pour grouper des données).
• L'unicité des preuves d'identité (si deux preuves disent la même chose, elles sont la même preuve).

Le résultat surprenant : Même avec tous ces outils, on ne peut toujours pas prouver la règle de l'induction pour les nombres naturels.

Pourquoi ? Il manque une pièce maîtresse : l'Extensionnalité Fonctionnelle (FunExt).

• L'analogie du Chef et du Plat :
  • Imaginez deux chefs, Chef A et Chef B.
  • Le Chef A prépare un plat en suivant une recette secrète complexe.
  • Le Chef B prépare le même plat en suivant une recette totalement différente.
  • Au final, le plat est identique (même goût, même apparence).
  • Dans le système de base, le système dit : "Non, ce sont deux chefs différents, donc leurs plats sont différents."
  • L'Extensionnalité Fonctionnelle est la règle qui dit : "Peu importe comment vous avez cuisiné, si le résultat est le même, alors vous êtes le même chef."

Geuvers montre que sans cette règle (FunExt), le système reste aveugle à l'égalité des résultats. Il ne peut pas "voir" que deux constructions différentes mènent au même résultat, et donc il ne peut pas prouver les règles d'induction nécessaires pour construire des structures solides.

4. Conclusion : Ce que nous apprenons

En résumé, cet article nous dit :

1. Le langage de base (λP2) est puissant, mais il a des limites cachées. Il ne peut pas construire certaines structures "parfaites" (comme des nombres avec une induction parfaite ou des flux infinis avec une égalité parfaite).
2. On ne peut pas simplement "tricher" avec une astuce de codage pour contourner ces limites.
3. Pour débloquer ces capacités, il faut absolument ajouter l'Extensionnalité Fonctionnelle. C'est la clé qui permet au système de comprendre que "le résultat compte plus que la méthode".

C'est une belle démonstration de la rigueur mathématique : on ne se contente pas de dire "ça ne marche pas", on construit des mondes entiers pour prouver pourquoi ça ne marche pas, et on identifie exactement quel outil manque pour que tout fonctionne.

En hommage à Stefano Berardi : L'article est aussi une célébration de la carrière de Stefano, qui a travaillé sur ces questions dès ses débuts. Geuvers montre que les questions posées il y a des décennies sont toujours d'actualité et que la réponse finale nécessite une compréhension profonde de la nature de l'égalité et de la preuve.

Résumé technique

Voici un résumé technique détaillé de l'article « Non-Derivability Results in Polymorphic Dependent Type Theory » de Herman Geuvers, rédigé en français.

Titre : Résultats de non-dérivabilité dans la théorie des types dépendants polymorphes

Auteur : Herman Geuvers (Université Radboud, Nijmegen ; Université de technologie d'Eindhoven)
Contexte : Article dédié à Stefano Berardi, publié dans EPTCS 441 (2026).

---

1. Problématique et Contexte

L'article s'inscrit dans le cadre de la théorie des types dépendants, spécifiquement le $\lambda P2$ (théorie des types dépendants d'ordre deux), qui est un sous-système du Calcul des Constructions (CC).

• Le problème central : Bien que le $\lambda P2$ permette d'encoder des types de données inductifs (comme les nombres naturels via les numéros de Church) et de définir des fonctions sur ces types, les principes d'induction ne sont pas démontrables pour ces encodages. Il a été établi précédemment (notamment par l'auteur dans [12]) qu'aucune représentation « intelligente » des types de données ne permet de prouver l'induction dans le $\lambda P2$ pur.
• Les extensions récentes : Des travaux récents ([1], [8]) ont montré que dans une extension du $\lambda P2$ incluant des types $\Sigma$ (sommes dépendantes), des types d'identité avec l'unicité des preuves d'identité (UIP), et l'extensionnalité fonctionnelle (FunExt), il devient possible de définir des types de données (inductifs et co-inductifs) satisfaisant leurs principes d'induction et de co-induction appropriés.
• Les questions ouvertes :
  1. Les types quotients (quotient types) et les types co-inductifs (comme les flux ou streams) sont-ils impossibles à définir avec leurs principes dans le $\lambda P2$ pur ?
  2. Parmi les extensions utilisées dans [1] (UIP, FunExt, $\Sigma$), lesquelles sont strictement nécessaires ? En particulier, l'extensionnalité fonctionnelle est-elle cruciale pour l'induction ?

2. Méthodologie

L'auteur adopte une approche syntaxique et sémantique pour répondre à ces questions, en construisant des contre-modèles.

• Modèles Polysets (Polyset Models) : L'étude repose sur une sémantique de réalisabilité basée sur des algèbres combinatoires faiblement extensionnelles (WECA). Les types sont interprétés comme des sous-ensembles (polysets) de l'algèbre combinatoire.
• Stratégie de preuve : Pour montrer qu'un principe (comme l'induction ou la co-induction) n'est pas dérivable, l'auteur construit un modèle spécifique du $\lambda P2$ où :
  1. Le type de données (ex: les nombres naturels ou les flux) est bien défini.
  2. La proposition correspondant au principe d'induction ou de co-induction est vide (non habitée) dans ce modèle.
  3. Cela prouve que le principe ne peut pas être dérivé dans la théorie de base, car s'il l'était, il serait vrai dans tous les modèles (par la propriété de soundness).
• Outils spécifiques : L'auteur utilise des algèbres combinatoires basées sur les termes $\lambda$ non typés modulo $\beta$ ou $\beta\eta$, et introduit des constantes spécifiques pour modéliser les types d'identité et les sommes.

3. Contributions et Résultats Clés

L'article apporte des réponses partielles mais décisives aux questions ouvertes :

A. Non-dérivabilité des types quotients paramétriques

• Résultat : Les types quotients paramétriques (où l'opération de quotient est polymorphe) ne sont pas définissables dans le $\lambda P2$.
• Preuve : L'auteur construit un modèle où l'existence d'un terme de quotient polymorphe cls impliquerait qu'une fonction constante (dans le modèle) se comporte comme une fonction identité, ce qui mène à une contradiction (ex: true = false).
• Nuance : Des quotients non-paramétriques (pour des relations spécifiques et triviales) peuvent exister, mais pas de manière générale et polymorphe.

B. Absence de principe de co-induction pour les flux (Streams)

• Résultat : Le type de flux (streams) définissable classiquement dans le $\lambda P2$ n'est pas une coalgèbre finale.
• Preuve : L'auteur définit deux flux $s_1$ et $s_2$ qui sont bisimilaires (ils produisent les mêmes observations finies) mais qui ne sont pas égaux dans le modèle. Puisque le principe de co-induction exige que la bisimilarité implique l'égalité ($s_1 \sim s_2 \implies s_1 = s_2$), et que ce n'est pas le cas ici, le principe échoue.

C. Nécessité de l'Extensionnalité Fonctionnelle (FunExt) pour l'induction

• Contexte : L'article examine l'extension du $\lambda P2$ avec des types $\Sigma$ et des types d'identité (avec UIP), sans encore inclure FunExt.
• Résultat Majeur : Même avec $\Sigma$-types, types d'identité et UIP, le principe d'induction pour les nombres naturels reste non démontrable.
• Preuve : Un modèle est construit (basé sur l'algèbre $\Lambda_{id}$ étendue avec des constantes pour l'identité et les sommes) où :
  • L'UIP est valide.
  • Les règles pour les types d'identité et les sommes sont soundes.
  • Cependant, le principe d'induction pour les nombres naturels est faux (le type d'induction est vide).
• Conclusion : L'extensionnalité fonctionnelle (FunExt) est cruciale et indispensable pour rendre l'induction démontrable dans ce cadre. Sans elle, même avec les autres extensions, on ne peut pas obtenir de types de données inductifs « forts ».

4. Signification et Implications

• Limites du $\lambda P2$ : L'article confirme et étend les limites fondamentales du $\lambda P2$ pur. Il ne suffit pas d'avoir des types dépendants et de l'ordre deux pour obtenir une théorie des types complète pour les données inductives et co-inductives.
• Rôle des extensions : Il établit une hiérarchie claire des besoins :
  • Les types $\Sigma$ et l'UIP ne suffisent pas pour l'induction.
  • L'extensionnalité fonctionnelle (FunExt) est le composant manquant critique qui permet de passer d'une logique faible à une logique capable de raisonner sur l'induction et la co-induction via des encodages.
• Méthodologie : La construction de modèles syntaxiques basés sur des algèbres combinatoires faiblement extensionnelles s'avère être un outil puissant pour prouver l'impossibilité de certaines dérivations, là où les modèles standards (souvent paramétriques ou extensionnels) échouent car ils satisfont trop de propriétés.
• Perspectives : Ces résultats suggèrent que pour obtenir une théorie des types robuste pour les données (comme dans les travaux de HoTT ou les systèmes modernes), l'ajout de l'extensionnalité fonctionnelle n'est pas une option, mais une nécessité structurelle.

En résumé, cet article démontre rigoureusement que sans extensionnalité fonctionnelle, le $\lambda P2$ (et même ses extensions avec $\Sigma$ et UIP) reste incapable de supporter les principes d'induction et de co-induction forts pour les types de données standards, confirmant ainsi la nécessité des extensions proposées dans la littérature récente.