Cours 9  Sémantique du Calcul des Constructions Inductives

9.1  Le Calcul des Constructions pur (CC)

La théorie du Calcul des Constructions pur se ramène essentiellement à celle du système F_ω par effacement des dépendances en les preuves dans les types (cf chapitre sur l’extraction).

Tous deux correspondent à une logique très faible, puisqu’en interprétant Prop de manière booléenne, toute formule admet un modèle fini. En revanche, tous deux correspondent à un langage de fonctions très riche puisqu’ils contiennent toutes les fonctions prouvablement totales dans l’arithmétique d’ordre supérieur.

9.1.1  Puissance logique

Le modèle booléen à preuve unique (modèle « proof irrelevant »)

Le CC admet un modèle booléen, dans lequel Prop est interprété par l’ensemble a deux élément B={ true, false}. L’imprédicativité se résume alors à une quantification finie sur B. Les types de Type sont construits récursivement à partir de B et le produit fonctionnel. Dans le cas d’un produit A → T avec A une proposition et T un type, l’interprétation est celle¹. L’interprétation s’applique à tous les jugements qui ne sont pas des jugements de preuve (on note X, P, Q et T, U pour les objets et types du niveau Type et x, t, u et A, B pour les objets et types² du niveau Prop).

La règle de conversion est validée par le modèle et on a ⊢ t:A qui implique [[A]]= true, d’où la cohérence du CC puisque [[∀ A:Prop.A]]= false.

Le modèle est localement fini et [[A]]= true est décidable puisque les quantifications ne portent que sur des espaces fonctionnels engendrés à partir de B qui est fini et d’un nombre fini de construction par produit. En particulier la cohérence de CC est prouvable dans l’arithmétique.

Dans ce modèle, tous les entiers (dans le type ∀ A. (A → A) → (A → A)) sont identifiés. On ne peut donc prouver 0 ≠ 1. Les axiomes de Peano ne sont donc pas dérivables, en accord avec l’existence d’une preuve de cohérence dans l’arithmétique.

Question ouverte: complétion de F_ω (et plus généralement de CC dans son modèle booléen standard) vis à vis du modèle booléen. Quels axiomes ajouter pour obtenir ([[A]]= true)   →   ⊢ A (candidats: ∀ A:Prop. A= True ∨ A= False (complétude propositionnelle) et ∀ f,g:(∀ x:T.U). (∀ u:T. f u =_Uu g u) → f=g (extensionnalité)) ?

Remarque 1: l’indiscernabilité des preuves (« proof-irrelevance »), la complétude propositionnelle et le tiers-exclu sont tous les trois validés par le modèle booléen..

Remarque 2: on peut typiquement représenter false en théorie des ensembles par l’ensemble vide ∅ et true par un ensemble singleton (typiquement l’ensemble {∅} dont l’unique élément est l’ensemble vide); en ce cas, [[∀ X:T. B]]_ρ s’exprime comme ∩_V∈[[T]] [[B]]_ρ,X:=V.

Le modèle booléen sur le λ-calcul pur (modèle booléen non « proof irrelevant »)

Il existe une variante du modèle booléen qui préserve le contenu calculatoire des preuves. Ce modèle, non exprimable dans l’arithmétique, permet par exemple de montrer la non prouvabilité de l’induction de Peano [Geu01, SG95]. La différence par rapport au modèle booléen à preuve unique est que les propositions vraies sont interprétées par l’ensemble Λ de tous les λ-termes purs. L’interprétation est donc la suivante:

et on montre que ⊢ t:A implique [[t]] ∈ [[A]].

9.1.2  Puissance calculatoire

Le CC admet aussi un modèle par réalisabilité qui respecte le contenu intensionnel des fonctions (et des preuves). Un tel type de modèle permet de prouver la normalisation forte de CC et F_ω, donc la cohérence de l’arithmétique d’ordre supérieur et, a fortiori, de l’arithmétique. En particulier, le modèle par réalisabilité montre la cohérence de CC + (0≠ n+1) + injectivité du successeur + induction, c’est-à-dire de CC + les axiomes de Peano.

Tous les programmes prouvablement terminant dans l’arithmétique d’ordre supérieur sont dérivables dans F_ω et donc dans le CC [Gir72].

Schématiquement, le modèle par réalisabilité interprète les propositions comme des ensembles de λ-termes clos par β-expansion avec la propriété que t∈ [[A→ B]] ssi tu ∈ [[B]] pour tout u ∈ [[A]] (propriété dite de réductibilité). L’interprétation des types de Type est alors la même que pour le modèle booléen standard du CC : le produit du CC est interprété comme le produit ensembliste à ceci près que le domaine de base, Prop, est maintenant un ensemble de parties de λ-termes.

9.1.3  Extensions incohérentes du Calcul des Constructions

Systèmes U-, U et Type:Type

Les systèmes U- et U (dus à J.-Y. Girard [Gir72]) sont en fait des extensions du système F_ω. Alors que la couche Type de F_ω correspond à un λ-calcul simplement typé bati sur la constante Prop, la couche Type des systèmes U- et U correspond à un λ-calcul polymorphe (le système F) incluant Prop comme type de base.

Le système Type:Type (énoncé par P. Martin-Löf) est le système où Prop et Type sont confondus et où tous les produits sont permis. En particulier, Type:Type est un objet terminal de la catégorie des PTS : tout PTS se plonge dans Type:Type.

Ces trois systèmes sont incohérents. Une des manières de dériver une incohérence est de construire dans U- (et donc aussi dans les 2 autres systèmes) un type Univ:Type et une injection³ i:∀ A:Type.(A→ A→ Prop)→ (A→ Prop)→ Univ.

En spécialisant i à Univ, on peut plonger dans Univ toute relation R:Univ→ Univ→ Prop définie sur un domaine D:Univ→ Prop. Par ce fait, on peut dériver le paradoxe de Burali-Forti (cf Girard [Gir72, Coq86]), le paradoxe de Reynolds-Coquand (cf Coquand [Coq94b]), ou plus généralement encoder la théorie naïve des ensembles de Cantor et en particulier le paradoxe de Russell (cf Miquel [Miq01]).

9.2  Le Calcul des Constructions avec univers (CC_ω)

Le Calcul des Constructions avec univers CC_ω étend le CC avec une hiérarchie dénombrable d’univers Type₁:Type₂:Type₃... (on identifie alors le niveau Type de CC avec Type₁). Les produits sur cette hiérarchie sont prédicatifs : si T:Type_i et U(X):Type_j alors Π X:T. U(X):Type_max(i,j). La sorte Prop reste imprédicative : si T:Type_i et U(X):Prop alors Π X:T. U(X):Prop.

De plus, CC_ω introduit une relation de sous-typage vérifiant Prop ⊂ Type₁ ⊂ Type₂ ⊂ Type₃... Concrètement, la relation de conversion est remplacée par une relation de sous-typage définie par

La règle de conversion est remplacée en conséquence par

CC_ω correspond à la partie sans inductifs et sans Set du Calcul des Constructions Inductives⁴.

9.2.1  Encodage de l’arithmétique

Dans CC_ω, on peut définir l’ensemble des entiers naturels au niveau Type₂

puis on peut définir le prédicat caractéristique des entiers naturels par

On peut alors prouver que 0≠ s(n) et que s est injectif sur tout entier de IsNat, ce qui donne l’arithmétique de Peano.

Ainsi, CC avec juste un niveau supplémentaire de Type contient l’arithmétique⁵.

9.2.2  Encodage de la théorie des ensembles de Zermelo

En utilisant un codage des ensembles sous forme de graphe pointé, Miquel [Miq01] a pu plonger la théorie des ensembles de Zermelo (qui est beaucoup plus faible que ZF) dans CC_ω avec trois niveaux⁶ de Type.

9.2.3  Puissance logique

Nous allons faire une analyse de la force logique de CC_ω en termes ensemblistes, c’est-à-dire en termes de profondeur d’imbrication des ensembles que l’on peut construire dans ECC ⁷.

On vient de voir que Type₂ contient l’ensemble des entiers naturels (ω) ce qui correspond en théorie des ensembles à un ensemble de profondeur ω. Par ailleurs, la construction de chaque Type_i+1 permet au plus d’itèrer ω fois le produit fonctionnel à partir de Type_i. Les fonctions étant représentées en théorie des ensembles par des relations, une fonction de type A → B correspond en théorie des ensembles à une partie de l’ensemble produit A × B et plus généralement, une fonction de type Π x:A. B(x) est une partie de A × ∪_{x∈ A} B(x). Ainsi, l’ensemble de fonctions Π x:A. B(x) se construit en ajoutant un niveau d’imbrication au maximum des niveaux de A et des B(x). Les types de Type_i+1 ont donc un nombre fini de niveaux d’imbrication en plus du niveau d’imbrication de Type_i. En passant à la limite, le type Type_i+1 lui-même a donc ω niveaux d’imbrication en plus que Type_i. On arrive de la sorte à établir que Type_i contient des ensembles de niveaux d’imbrication ensemblistes ω.i. En passant à la limite une nouvelle fois, on établit que ECC doit contenir des ensembles de niveau d’imbrication au moins ω².

Par ailleurs, P.-A. Melliès et B. Werner [MW98] ont exhibé un modèle de cette cardinalité montrant que la force ordinale de ECC était bien ω² (itération ω² des parties).

9.3  Extensions cohérentes et incohérentes du Calcul des Constructions Inductives

On considère le Calcul des Constructions Inductives avec Set et Prop.

Dans le cas où Set est imprédicatif, il n’existe pas de modèle complet du CCI. Les deux approximations les plus proches sont

• le modèle de B. Werner qui ne prend en compte ni Prop ni la hiérarchie d’univers [Wer94]
• le modèle d’A. Miquel qui distingue une sorte Prop interprétée classiquement et une sorte Set interprétée par réalisabilité mais qui ne prend pas en compte les types inductifs[Miq01]

Dans le cas d’un Set prédicatif, il n’existe pas non plus explicitement de modèle, mais il est communément admis que le modèle booléen avec Set interprété comme Type₀ fonctionne.

Axiome K de Streicher

L’axiome K de Streicher énonce que toute preuve de la réflexivité de l’égalité peut être remplacée dans tout contexte par la preuve canonique de réflexivité

Cet énoncé est équivalent à l’existence d’une unique preuve de réflexivité de l’égalité

Il existe plusieurs autres formulations équivalentes à l’axiome K. L’une d’elle est particulièrement intéressante en pratique: elle exprime que deux objets dans des types dépendants sont égaux dès lors qu’ils sont dans la même instance dépendante

Notons que l’axiome K est dérivable si l’égalité sur A est décidable (ce qui est le cas en particulier en admettant la logique classique). Notons par ailleurs que l’axiome K est une conséquence directe de l’indiscernabilité des preuves, indépendamment alors de la logique classique.

Indiscernabilité des preuves

L’indiscernabilité des preuves s’exprime par

Indépendant dans CC : non prouvable (pas de preuve close), validé par le modèle booléen. Incohérent dans CCI en remplaçant Prop par Set (car 0≠1 dans Set).

Logique classique

La logique classique peut être exprimée par exemple par le tiers-exclu.

Indépendant dans CC et ECC : non prouvable (pas de preuve close), validé par le modèle booléen.

Incohérent dans CCI si la disjonction est dans Set : de part la dérivabilité de l’axiome du choix (somme forte/élimination dépendante) et de true ≠ false dans Set, on peut injecter Prop dans bool (une « rétraction »), puis encoder le système U- et dériver l’absurde.

Remarque: ∀ A:Set. A∨ ¬ A est supposé cohérent. Ce qui permet vraiment de montrer une incohérence, c’est que la disjonction soit dans Set.

Dans CCI, la logique classique entraîne l’indiscernabilité des preuves (la preuve nécessite l’élimination dépendante des inductifs de Prop et l’imprédicativité, cf Barbanera et Berardi [BB96]).

Extensionnalité propositionnelle et complétude propositionnelle

La complétude propositionnelle (∀ A:Prop.A=True ∨ A=False) est équivalente dans CC à la conjonction de la logique classique et de l’extensionnalité propositionnelle (∀ A,B:Prop.(A↔ B)→ A=B).

Dans CCI, l’extensionnalité propositionnelle entraîne l’indiscernabilité des preuves (la preuve nécessite l’élimination dépendante des inductifs de Prop).

Axiome du choix

L’axiome du choix (forme fonctionnelle) est dérivable si l’existentielle (notée alors comme un Σ-type) est dans Set ou dans Type :

Si l’existentielle est dans Prop et Y dans Set, l’axiome est incohérent en présence de la logique classique dans Prop, car alors, on peut injecter Prop dans bool et encoder le système U-.

En fait, une forme beaucoup plus faible de l’axiome du choix (bien que plus compliquée à exprimer), à savoir l’axiome de description suffit à obtenir cette contradiction.

Remarque: Si Y est dans Type, du fait du sous-typage Set ⊂ Type, la contradiction avec la logique classique persiste.

L’axiome du choix unique

Contrairement à ce que son nom suggère, l’axiome de choix unique ne choisit pas. Ce qu’exprime l’axiome du choix unique, c’est que toute relation fonctionnelle peut être « réifiée » en une fonction :

Si l’existentielle est dans Set ou Type, l’axiome est dérivable. Dans Prop (et avec B dans Set ou Type), il entraîne l’existence d’une rétraction de Prop vers bool:Set. Ainsi, l’axiome est incohérent avec la logique classique dans Prop pour le CCI avec Set imprédicatif (car alors on peut simuler le système U-). Si Set est prédicatif, il reste cohérent avec la logique classique (la rétraction s’interprète comme un oracle qui décide la validité de toute proposition).

On peut aussi s’intéresser aux interactions avec la logique classique calculatoire, c’est-à-dire basée sur une réalisation par l’opérateur call-cc de Scheme ou SML ou l’opérateur µ de Parigot. Une telle interprétation calculatoire de la logique classique est incompatible avec l’axiome de description même avec Set prédicatif [Her05].

Le principe de description indéfinie (opérateur є de Hilbert)

Le principe de description indéfinie affirme l’existence a priori d’un témoin canonique dans tout prédicat non vide sur un domaine non vide. On peut l’exprimer en Coq par la proposition

Ce principe est équivalent à se donner, pour tout A non vide, un opérateur є:(A→ Prop)→ A tel que ∃ x:A. P(x) → P(є(P)) (opérateur є de Hilbert).

De manière évidente, le principe de description indéfinie entraîne l’axiome du choix.

Le principe de description indéfinie (version constructive)

Le principe de description indéfinie (dans sa version constructive) exprime que si une proposition est prouvablement habitée, alors il existe un terme qui dénote un habitant de cette proposition. Ce principe peut être exprimé dans le CCI par la formule

Notons que le principe de description indéfinie est dérivable si A est dénombrable et P décidable. En effet, on peut alors construire un programme qui teste successivement si chacun des éléments de A, dans l’ordre, vérifie P. Ce programme est calculable par décidabilité de P et terminant par existence d’un habitant dans P. On en déduit le principe de description (cf theories/Logic/ConstructiveEpsilon.v).

Le principe de description définie (opérateur ι de Church)

Le principe de description définie restreint le principe de description indéfinie au cas des prédicats habités par un objet unique. Le témoin a priori de la non vacuité du prédicat ne vérifie le prédicat que si ce terme est prouvablement unique. Le principe de description définie peut être exprimé dans le CCI par la formule

Ce principe est équivalent à se donner, pour tout A non vide, un opérateur ι:(A→ Prop)→ A tel que ∃ ! x:A. P(x) → P(ι(P)) (opérateur ι de Church).

Ce schéma n’entraîne pas l’axiome du choix mais il entraîne l’axiome du choix unique.

Le principe de description définie (version constructive)

Dans sa version constructive, le principe de description définie ne présuppose pas l’existence a priori de témoins : le témoin d’un prédicat n’aura une dénotation que si le prédicat est effectivement habité de manière unique. Ce principe s’exprime dans le CCI par la formule

Tout comme le principe de description indéfinie dans sa version constructive, la description définie est dérivable dans sa version constructive si A est dénombrable et P décidable.

Axiome du choix relationnel

L’axiome du choix sous sa forme relationnelle s’exprime par

L’axiome du choix relationnel + l’axiome de choix unique est équivalent à l’axiome du choix fonctionnel.

Dans les conflits entre logique classique, axiome du choix et imprédicativité de Set, c’est la composante « choix unique » qui pose problème. En effet, cette dernière, en présence de la logique classique, peuple le monde des fonctions d’objets non calculables, ce qui est incompatible avec la vision du monde requise par l’imprédicativité, vision pour laquelle seules existent les fonctions qui sont calculables.

Ainsi, l’axiome du choix (avec sa réelle capacité à ordonner les domaines non dénombrables) n’a semble-t-il rien d’incompatible avec logique classique et imprédicativité si l’on se restreint à sa formulation relationnelle.

Extensionnalité des prédicats et axiome du choix

L’extensionnalité des prédicats + l’axiome du choix (même sous une forme relationnelle qui n’implique pas l’axiome de description) entraîne la logique classique !! C’est à l’origine un résultat de Diaconescu pour la théorie des ensembles qui a été adapté à la théorie des types par Lacas et Werner [Dia75, LW99].

Extensionnalité fonctionnelle

L’extensionnalité des fonctions exprime pour deux types A et B (ou plus généralement pour un produit fonctionnel ∀ x:A.B(x)) que deux fonctions ayant le même graphe d’entrées-sorties sont égales

Typiquement, l’extensionnalité fonctionnelle implique que l’addition sur les entiers définie par récurrence sur son premier argument est égale à l’addition définie par récurrence sur son second argument. L’extensionnalité n’est pas prouvable (elle n’est pas validée par le modèle de réalisabilité qui est intentionnel; par ailleurs, une inspection des formes normales possibles d’une éventuelle preuve devraient permettre d’affirmer l’absence d’une telle preuve).

Un modèle ensembliste validerait l’extensionnalité fonctionnelle. Donner un modèle ensembliste du Calcul des Constructions Inductives avec Set prédicatif est faisable à la condition de retirer la règle de sous-typage Prop ⊂ Type.

En présence de Prop ⊂ Type, il est vraisemblable que le modèle ensembliste fonctionne mais il reste des obstacles techniques. Une question ouverte reste donc la compatibilité de l’extensionnalité fonctionnelle avec le sous-typage Prop ⊂ Type.

Condition de garde

Sans condition de garde, on peut directement dériver l’absurde:

Fixpoint Paradox (u:unit) : False := Paradox u.

Condition de positivité

Sans condition de positivité, on peut facilement dériver l’absurde:

Inductive A : Prop := intro : (A->False)->A.
Definition Paradox : False := (fun (H:A->False) => H (intro H)).

Élimination forte sur un ensemble large

Sans restriction de l’élimination forte sur un inductif large, on pourrait encapsuler le type des propositions (un type large) comme une proposition (un petit type) et le redécapsuler à volonté sans perte d’information.

Inductive prop : Prop := down : Prop -> prop.
Definition up (p:prop) : Prop := let (A) := p in A.

Theorem iso : forall A:Prop, up (down A) = A.
Proof. reflexivity. Qed.

La quantification imprédicative dans Type du système U- deviendrait ainsi simulable dans le CCI par une simple quantification imprédicative dans Prop, rendant possible la dérivation d’un paradoxe dans le CCI.

Condition de positivité stricte

La positivité large n’est pas suffisante pour garantir l’absence de paradoxe. De fait, autoriser le type non strictement positif suivant

Inductive T : Type := I : ((T->Prop)->Prop)->T.

conduit à un paradoxe. L’idée (extraite de Coquand–Paulin-Mohring [CPM90]) est la suivante: Tout objet de type A peut s’interpréter comme un ensemble singleton de type A→Prop en posant s_A(t) = λ x:A. x=t. Pour A étant T→ Prop, on en déduit l’existence d’un plongement φ(P) = I (s_T→Prop(t)) de T→Prop vers T. Ce plongement est injectif par injectivité de I. On pose alors

Par injectivité de φ, on montre que P₀(φ(P₀)) est équivalent à ¬ P₀(φ(P₀)). Contradiction.

1

Le modèle booléen standard de CC différencie selon que A est prouvable ou pas (cf par exemple [MW03]) de T. Ce raffinement, qui force à considérer des interprétations partiellement définies n’est pas nécessaire pour notre analyse. Autrement dit, on se restreint à un modèle ayant le grain du modèle booléen de F_ω

2

qui sont incidemment aussi des objets du niveau Type

3

Typiquement il suffit de prendre Univ = ∀ A:Type.(A→ A→ Prop)→ (A→ Prop).

4

Une première version de CC avec univers apparaît dans la thèse de T. Coquand [Coq85] sous le nom de Calcul des Constructions Généralisé (GCC): c’est une version sans la règle Prop ⊂ Type_i et dont le sous-typage (appelé cumulativité) ne passe pas sous les produits (ainsi, si f est une variable de type A→ Type₁, alors on a λ x:A.(f x):A→ Type₂ mais pas f:A→ Type₂). La version de CC avec univers décrite ici est due à Luo [Luo90] dont le Calcul des Constructions Étendu (ECC) correspond à l’extension de CC_ω avec une construction primitive pour les types existentiels (Σ-types). La terminologie CC_ω, quant à elle, remonte à Miquel [Miq01]

5

En fait, les dépendances en les preuves ne sont pas nécessaires pour encoder l’arithmétique. Ainsi, F_ω avec un niveau supplémentaire convient tout aussi bien.

6

Comme pour l’encodage de l’arithmétique, F_ω avec deux niveaux supplémentaires (ce qui se note F_ω.3) suffit pour encoder la théorie des ensembles de Zermelo.

7

En théorie des ensembles, un niveau supplémentaire d’imbrication des ensembles correspond à une application de l’axiome des parties. On démarre de l’ensemble vide dont la profondeur est nulle. Le passage à la limite se fait avec l’axiome de l’union.