Comments on Une introduction à la correspondance de Curry-Howard

Bon, la principale correction, c'est que les deux phrases « Ce qui est moins évident […] soit généralisé. » se sont retrouvées au mauvais endroit et devraient être juste après « Pareil pour les preuves de ⊤ ∨ ⊤. ».

À part ça, ayant retrouvé un peu d'énergie après toute cette période, je suis en train de travailler à un billet où j'essaye de présenter de façon un peu cohérente MLTT, CIC et HoTT en les comparant. C'est quand même dingue que ce soit aussi impossible de trouver ça (Herbelin m'a confirmé qu'il y avait un gros manque de livres synthétiques et trop d'« inside knowledge » qui ne se trouve qu'éparpillée dans des articles).

En me relisant, je me rends compte que je me suis emmêlé les pinceaux sur quelques points. Oublie pour l'instant, je reprendrai ça quand j'aurai des neurones un peu plus fonctionnels.

On a déjà longuement discuté plusieurs fois de ces questions, mais je crois que j'ai un peu mieux compris certaines choses depuis, et je ne suis pas sûr que j'aurai le temps et la motivation pour continuer ma petite série de billets de blog sur la théorie des types, donc ça vaut peut-être la peine que je fasse une réponse un peu cohérente à la question que tu te poses à la toute fin, en espérant ne pas dire de bêtises :

> Remarque : j'ai présenté les deux questions discutées par mes deux addenda (la question du monde logique vs. le monde informatif, aka ‘∃’ vs. ‘Σ’, et la question de l'imprédicativité), comme indépendantes, mais ce n'est notamment pas du tout clair pour moi si elles sont vraiment indépendantes. Est-ce que le fait que Coq et les trucs à la Martin-Löf aient fait des choix différents sur les deux questions est un hasard, ou est-ce qu'il y avait une raison plus profonde ?

Oui, il y a bien une raison profonde (et tu es passé tout près de la comprendre).

Partons de MLTT (disons avec ω univers). C'est prédicatif et l'axiome du choix (avec Σ) est prouvable. On peut en donner un modèle classique et ensembliste, en interprétant chaque Type_i par un univers de Grothendieck, les types fonction par les ensembles de fonctions, etc. Le fait que ∀ (x : A), B x vive dans Type_i si A et B x vivent dans Type_i correspond bien à ce que tu attends d'un univers de Grothendieck. (Tu attends aussi que 𝒫(X) soit dans l'univers si X y est, mais j'y reviens.)

Maintenant, qu'est-ce qui se passe si on veut rajouter une sorte imprédicative pour obtenir le calcul des constructions (à ω univers) ? Là, le modèle ensembliste est cassé. Ce qui est moins évident, mais que montre le paradoxe de Girard, ou du moins l'une de ses variantes, c'est qu'en fait tous les modèles sont cassés, le système est incohérent. Mon intuition là-dessus, c'est que les règles de typage forcent les éléments du modèle à se comporter « suffisamment comme des ensembles » pour que ce problème ensembliste soit généralisé.

Bon, mais après tout, le système F arrive à être imprédicatif et cohérent, donc quel est le nœud du problème ? Au passage, j'ai l'impression qu'il y a une petite confusion là où tu écris « En fait, Girard a montré que l'imprédicativité du système F ne cause pas de paradoxe » : le théorème difficile montré par Girard, c'est la normalisation forte, mais pour la cohérence, tu n'en as pas besoin, il suffit de constater que le modèle booléen marche. Parce qu'il y a quand même ce modèle évident, qui certes est classique, mais qui suffit à prouver la cohérence.

Dans le modèle booléen, tous les types de Prop sont interprétés par {∗} ou ∅. Donc, et si on essayait d'appliquer la même idée au calcul des constructions ? À savoir : les types de Prop deviennent {∗} ou ∅, les autres sont interprétés comme avant.

Là, si tu regardes droit dans les yeux les règles de typage, tu vois que toutes vont bien s'interpréter dans le calcul des constructions. (Notamment, le fait que si X vit dans Type_i, alors X → Prop aussi, utilise la propriété X ∈ 𝒰 ⇒ 𝒫(X) ∈ 𝒰 des univers de Grothendieck 𝒰.)

Par contre, si tu passes au calcul des constructions inductives (en rajoutant les types inductifs), les règles naïves sont cassées dans ce modèle. Ceci parce que les types inductifs te permettent de créer des valeurs dans des types de Prop qui sont prouvablement différentes, alors que tous les types de Prop habités sont censés être interprétés par {∗}. Le cas archétypal est celui de ∃ : tu as deux preuves de (mettons) ∃ n, n = 0 ∨ n = 1, et si tu peux éliminer le ∃ dans Type, tu peux prouver qu'elles sont différentes parce que leurs témoins sont différents, sauf que dans le modèle elles étaient censées être égales. Pareil pour les preuves de ⊤ ∨ ⊤. Et du coup, c'est pour ça qu'on est obligé d'imposer la restriction que les inductifs de Prop ne s'éliminent que dans Prop (sauf les ❝sous-singletons❞).

En fait, ce n'est pas vraiment une surprise parce que les types inductifs simples, qui ne sont pas récursifs, s'encodent de la manière standard que tu expliques dans ton billet, donc par exemple A ∨ B va être ∀ (C : ??), (A ⇒ B ⇒ C) ⇒ C, mais il faut quand même choisir le type sur lequel on quantifie C. Si ?? est Prop, alors le résultat vit dans Prop, mais tu ne peux l'éliminer (en l'occurrence, l'appliquer à une fonction A ⇒ B ⇒ C) que pour obtenir quelque chose (du C) qui est dans Prop. Alors que si ?? est un Type_i, tu peux éliminer le A ∨ B dans Type_i, mais la contrepartie, c'est que A ∨ B vit dans Type_i, parce que pour C : Type_i, (A ⇒B ⇒ C) ⇒ C est dans Type_i et pas Prop, même si A et B sont dans Prop. Du coup, cette restriction sur l'élimination des inductifs est naturelle et pas complètement tombée du ciel, parce qu'elle coïncide, sur les types inductifs simples comme ∨ et ∃ qui admettent ce genre d'encodage, avec les restrictions imposées par le calcul des constructions de base.

Avec tout ça, on a réparé le modèle classique (ensembliste, booléen, extensionnel pour les fonctions et les propositions, proof-irrelevant, …). Et au passage, on voit que l'extensionnalité propositionnelle est cohérente, vu qu'elle est vérifiée par ce modèle (bien qu'elle ne soit pas prouvable).

On peut aussi remarquer que l'axiome du choix, prenons-le par exemple sous sa forme « ∀ ∃ ⇒ ∃ ( → ) ∀ », est un « vrai » axiome du choix et pas une sorte de retour clandestin de l'élimination de Σ qui est interdite pour ∃. Parce que du moins dans le modèle ensembliste, les preuves de ∃ ne contiennent pas le témoin, donc on le sort vraiment d'un chapeau. Peut-être qu'il faut intuitivement penser à ∃ comme « j'ai vu le témoin (⟵ je suis intuitionniste), mais je l'ai oublié ». Ou se rappeler que c'est équivalent à ‖Σ …‖ (le ‖ ⋅ ‖ du HoTT book correspond plus ou moins, si je ne m'abuse, au « inhabited » de Coq), construction qui est un genre de {∗, x ∈ X} pour oublier les habitants.

Parenthèse : Je me suis moi-même planté là-dessus dans mon billet de blog sur l'axiome du choix, où j'ai écrit à un endroit que « (∀ x, inhabited (F x)) ⇒ inhabited (∀ x, F x) » revenait en quelque sorte à transgresser le typage pour éliminer les inhabited vers Type, mais en se faisant pardonner parce qu'on revient immédiatement dans Prop en mettant le tout dans un inhabited. C'est une intuition fausse, parce qu'en fait, l'axiome du choix global « global_choice : forall (T : Type), inhabited T -> T » est parfaitement cohérent, mais si on ajoute en plus « global_choice_retract : forall (T : Type) (x : T), global_choice T (inhabits x) = x », ça devient incohérent (enfin, il faudrait quand même que je vérifie ça, mais c'est certain qu'avec en plus « forall (T : Type) (h : inhabited T), inhabits (global_choice T h) = h », c'est incohérent comme me l'a montré Gaëtan Gilbert ici <URL:https://coq.discourse.group/t/allowing-large-elimination/2451/3>).

Maintenant, vu que je n'ai parlé que d'un modèle classique, à quoi ressemblent les modèles du calcul des constructions inductives qui ne valident pas le tiers exclu ? Je n'a pas du tout les idées claires là-dessus. Ce qui est sûr, c'est que pour le système F, tu dois pouvoir prendre un topos (vu qu'ils interprètent une logique beaucoup plus générale), et en particulier le topos effectif ; je crois qu'on peut étendre ça pour obtenir un modèle de réalisabilité de CICω.

La morale, c'est que si tu as l'imprédicativité, tu es obligé de restreindre l'élimination. Après, tu pourrais aussi imaginer restreindre l'élimination tout en gardant la sorte restreinte prédicative. Parce qu'une fois qu'on a cette élimination restreinte, au départ pour des raisons logiques, on se rend compte que ça peut servir aussi à délimiter ce qui est conservé par l'extraction de programmes et ce qui ne l'est pas (cette distinction n'a aucun raison théorique d'exister : un peu comme tu as des APIs publiques et des fonctions privées qui ne sont pas dans l'API, c'est utile d'avoir des types pour les preuves tels que l'utilisateur de ton API ne puisse pas se servir de la construction faite dans ta preuve). Disons qu'on a besoin d'une délimitation pour des raisons théoriques et une autre pour des raisons pratiques, et c'est plus simple de mettre les deux au même endroit. En tous cas, c'est ce que fait Coq.

Mais du coup, le résultat est imparfait. Très concrètement, je peux écrire en Coq une fonction normalize : forall t : system_F_term, exists u : system_F_term, (reduces t u) /\ (normal u), en utilisant la force logique de l'imprédicativité (parce que la normalisation du système F n'est pas prouvable dans MLTT). Je ne peux pas éliminer ce « exists » pour en tirer une fonction system_F_term → system_F_term : en termes de programmation pure, c'est difficile à justifier (« si on pouvait faire ça, on pourrait exploiter l'imprédicativité de manière subtile et intelligente pour créer un programme qui ne termine pas et s'en servir pour montrer False »), je ne sais le justifier de manière satisfaisante que du côté logique de Curry-Howard. Mais une fois qu'on a cette fonction, on sait, par la propriété de canonicité, que « normalize t » où t est clos se réduit forcément en « inhabited u », et on peut très bien en tirer le u. Donc on pourrait ignorer cette séparation Prop/Type et extraire un programme qui normalise un terme du système F. Fondamentalement, la raison pour laquelle on ne peut faire ça qu'a posteriori est que l'extraction n'a pas à se soucier d'assurer la terminaison. Sauf que comme Coq choisit de mettre la barrière d'extraction au même endroit que la barrière d'imprédicativité, il ne va pas te laisser extraire un tel programme.

D'ailleurs, il faudrait que j'essaie de comprendre à quoi correspond l'extraction, du point de vue théorique. J'ai la vague impression que ça veut dire « interpréter dans un modèle de réalisabilité et prendre le résultat ».

Je ne maîtrise pas encore toutes les subtilités du topos effectif, mais je crois qu'il y a des phénomènes analogues dans ce cadre : Si Eff valide ∀ x ∈ ℕ, ∃ y ∈ ℕ, R(x, y), alors Eff valide ∃ f : ℕ → ℕ, ∀ x ∈ ℕ, R(x, f(x)). Mais ce n'est sans doute plus vrai si tu remplaces ℕ par un objet qui n'est pas une assemblée parce que tu ne sais pas réaliser la compatibilité de f à l'égalité, ou quelque chose comme ça ? Je commence à fatiguer, j'arrête de réfléchir pour l'instant. En tous cas, hope that helps et hope that was not *too* wrong :-)

La théorie *cubique* des types, basée sur la théorie homotopique des types, et implémentée dans Cubical Agda, permet d'avoir de vrais types quotients qui réduisent correctement (ce sont un cas particulier des "types inductifs supérieurs" (Higher Inductive Types) limités au niveau des ensembles (types 0-tronqués)).

Par exemple: <URL: https://1lab.dev/Data.Set.Coequaliser.html >

Introduction intelligible, mis à part les addenda. Je n'ai toujours pas vraiment compris comment se matérialise côté typage la distinction entre les deux notions d'existence — le fait que je n'ai aucune notion en théorie des types et ne connaisse pas les langages utilisés ici n'aide certainement pas… (mais bon, ce n'est pas grave, à mon niveau la compréhension de CH dans le cas "Martin-Löf" me suffit).

Autre sujet, mais puisque tu mentionnes les problématiques de preuve constructive, logique intuitionniste, etc. cette question <https://math.stackexchange.com/questions/4831457/non-constructiveness-and-finite-mathematics> que je me posais et la réponse obtenue t'intéresseront peut-être.