Dans ce cours nous étudions le caractère constructif de la logique sous-jacente au calcul des constructions inductives. Nous montrons comment construire à partir d’une preuve, un programme qui “réalise” la propriété montrée. Nous expliquerons la distinction entre les sortes Prop et Set dans le système Coq.
La logique de Coq est intuitionniste, aucun axiome ne permet de dériver A ∨ ¬ A ou bien ¬ ¬ A ⇒ A pour une formule A arbitraire.
On se place par exemple dans l’arithmétique du premier ordre ou d’ordre supérieur. On notera ⊢ C A lorsque A est prouvable de manière classique et ⊢ I A lorsque A est prouvable de manière intuitionniste.
Il existe de nombreux résultats sur les liens entre les preuves classiques et intuitionnistes :
| si Γ ⊢ I A alors Γ ⊢ C A |
| si Γ ⊢ C A alors (Ci∨ ¬ Ci)i, Γ ⊢ I A |
| ⊢ C A ∨ B ⇔ ¬ (¬ A ∧ ¬ B) ⊢ C ∃ n:nat.P(n) ⇔ ¬∀ n.¬ P(n) |
| ⊢ I A ∨ B ⇒ ¬ (¬ A ∧ ¬ B) ⊢ I ∃ n:nat.P(n) ⇒ ¬∀ n.¬ P(n) |
| ⊢ C A ⇔ A* et si ⊢ C A alors ⊢ I A* |
| ⊢ C ∀ n.∃ m.Q(n,m) si et seulement si ⊢ I ∀ n.∃ m.Q(n,m) |
| si ⊢ I A ∨ B alors ⊢ I A ou ⊢ I B |
| si ⊢ I ∃ x.P(x) alors il existe t tel que ⊢ I P(t) |
| si ⊢ I ∀ x.P(x)∨ ¬ P(x) alors il existe f fonction récursive telle que ⊢ I f(x)=true⇔ P(x) |
| si ⊢ I ∀ x.∃ y. P(x,y) alors il existe f fonction récursive telle que ⊢ I P(x,f(x)) |
| (∀ x:A.∃ y:B. P(x,y)) ⇒ ∃ f. ∀ x. P(x,f(x)) |
Un avantage de la logique intuitionniste est qu’elle permet de parler de la décidabilité de propriétés de manière implicite sans faire appel à une théorie de la récursivité. Pour montrer qu’un prédicat est décidable ou qu’une relation fonctionnelle est récursive, il suffit d’exhiber une preuve d’une formule disjonctive ou existentielle. Cependant on ne capture pas ainsi toutes les fonctions récursives : en effet il existe des relations fonctionnelles correspondant à des fonctions récursives et pour lesquelles la formule disant que la relation est fonctionnelle n’est pas prouvable. Par exemple, il est possible de coder les termes du calcul comme des entiers et de définir la relation de réduction sur les termes. La preuve de totalité de la fonction de normalisation permet de montrer la cohérence logique du système et ne peut donc, du fait des théorèmes d’incomplétude de Gödel, être montrée dans le système lui-même.
La propriété suivante qui dit que toute fonction sur les entiers admet un minimum est vraie de manière classique mais pas de manière intuitionniste même si on se limite aux fonctions récursives :
| ∀ f. ∃ n. ∀ m. f(m) ≥ f(n) |
En effet il n’existe pas de fonction récursive qui pour une fonction quelconque calcule son minimum. Sinon on pourrait décider pour toute fonction si elle prend la valeur nulle et donc on pourrait décider du problème de l’arrêt.
On peut montrer de manière classique l’existence de deux nombre x et y irrationnels tels que xy soit rationnel. On suppose établi que √2 est irrationnel.
Cette démonstration ne permet pas d’exhiber une solution.
Les résultats précédents permettent d’établir que A ∨ ¬ A n’est pas démontrable en général. En effet supposons que ce soit le cas. On utilise le prédicat T de Kleene, T(n,m,p) signifie que la fonction récursive de code n s’exécute sur l’entrée de code m pour effectuer un calcul de code p. C’est un résultat bien connu que le prédicat P(n)=∃ p.T(n,n,p) n’est pas récursif car sinon ¬ P(n) le serait aussi et donc il existerait une fonction récursive de code q qui converge exactement lorsque ¬ P(n) est vérifiée c’est-à-dire pour tout n, ∃ p.T(q,n,p)⇔ ¬ ∃ p.T(n,n,p). Il suffit de prendre n=q pour aboutir à une contradiction.
Maintenant, en prenant pour A la formule P(x)=∃ p.T(x,x,p), si P(x)∨ ¬ P(x) est montrable il en est de même de ∀ x. P(x)∨ ¬ P(x) et on aurait la décidabilité de P(x) qui est contradictoire.
Pour montrer le caractère constructif de la logique de Coq, on s’appuie sur l’isomorphisme de Curry-Howard qui permet de représenter les preuves par des λ-termes fortement normalisables et la propriété syntaxique suivante qui caractérise les objets normaux clos dans les types inductifs :
Un terme normal clos dont le type est une instance d’une définition inductive est forcément de la forme (c t1… tn) avec c un des constructeurs du type inductif et ti des termes clos normaux.
En effet tout terme t s’écrit de manière unique (c t1… tn) avec c qui n’est pas une application. c peut donc être soit une abstraction, soit une variable, soit un constructeur, soit une sorte, soit un produit, soit un Case, soit un point fixe. On procède par récurrence sur la structure du terme et on examine chaque cas :
Inductive or (A B:Set) : Set := or_introl : A -> or A B | or_intror : B -> or A B.En normalisant cette preuve, on obtient soit un terme (or_introl a) avec a clos de type A et donc A est prouvable, soit (or_intror b) avec b clos de type B et donc B est prouvable.
Inductive ex (A:Set) (P:A->Set) : Set := ex_intro : forall (x:A), P x -> ex A P.Une preuve normale close de (ex A P) est de la forme (ex_intro t p) avec t terme clos de type A et p une preuve de (P t).
L’isomorphisme de Curry-Howard permet de montrer la constructivité de la logique intuitionniste. Cependant, il ne permet pas de justifier certains principes comme celui de l’indépendance des prémisses.
Soit une preuve du théorème de division euclidienne :
| ∀ a,b. b>0 ⇒ ∃ q.∃ r. a=b× q + r ∧ r < b |
Pour calculer effectivement le quotient et le reste, il faut fournir les entrées a et b mais aussi une justification de b>0 et le programme calculera le quotient et le reste mais aussi une preuve de correction. On voit que d’une part on doit fournir une information qui n’est pas utile pour le calcul (mais pour la terminaison et la correction du programme) d’autre part on calcule effectivement la preuve de correction du résultat ce qui est a priori inutile. La méthode proposée est donc inefficace.
L’isomorphisme de Curry-Howard n’est pas satisfaisant lorsqu’il s’agit de mettre en évidence les fonctions récursives sous-jacentes aux preuves. En effet, il ne permet pas de traiter le cas des preuves sous axiome, car alors les preuves ne sont plus closes et le calcul peut dépendre de manière essentielle de l’hypothèse.
Le problème est donc de savoir si étant donnée une preuve de ∀ x. P(x) ⇒ ∃ y. Q(x,y) il est possible de construire un programme f tel que ∀ x. P(x) ⇒ Q(x,f(x)).
Ce n’est en général pas vrai pour toutes les propriétés P(x). En effet la preuve de P(x) peut transporter une information servant au calcul du témoin y.
Par exemple si on prouve ∀ n,m.n ≤ m ⇒ ∃ p. n+p=m par induction sur la preuve de n ≤ m, alors le calcul de la différence entre n et m dépendra de cette preuve. Elle ne pourra plus être considérée comme non calculatoire et devra être donnée en argument au programme.
On s’intéressera à caractériser certaines formules P(x) dont les preuves ne contiennent pas d’information calculatoire intéressante. C’est le cas par exemple des formules de Harrop qui sont des formules n’ayant pas de disjonction ou de quantificateur existentiel en partie strictement positive (par exemple toutes les formules ¬ P).
Nous allons nous intéresser maintenant à des méthodes pour obtenir à partir d’une preuve intuitionniste de ∀ x. P(x) ⇒ ∃ y. Q(x,y) effectivement un programme f et une preuve de correction ∀ x. P(x) ⇒ Q(x,f(x)).
La réalisabilité a été introduite par Kleene en 1945. C’est une interprétation sémantique des propositions en logique intuitionniste.
On se donne un ensemble de réalisations qui représentent des programmes.
Chaque proposition P est interprétée comme un ensemble de réalisations qui est défini en général par récurrence sur la structure de la formule P. Cet ensemble est défini intentionnellement par une propriété de réalisabilité “x r P” dans lequel x est une nouvelle variable libre représentant une réalisation.
Une formule P dont l’interprétation est non vide sera dite réalisable.
L’idée de base des définitions est la suivante :
Une fois l’interprétation définie, on montre que si une formule est prouvable alors son interprétation est non vide et que de plus il est possible de construire, par récurrence sur la structure de la preuve, une réalisation particulière.
L’intérêt de cette méthode est qu’elle s’étend aux preuves sous contextes, c’est-à-dire que si une formule est prouvable sous hypothèses et que chaque hypothèse a une interprétation non vide alors il en est de même de la conclusion. Une conséquence de cette propriété est que toute formule dont l’interprétation est non vide est cohérente avec la théorie. En effet si on pouvait dériver l’absurde à partir de cette proposition alors l’interprétation de l’absurde serait non vide.
La réalisabilité peut servir également à montrer que certaines formules ne sont pas démontrables comme conséquence du fait qu’elles ne sont pas réalisables.
Il y a de très nombreuses notions de réalisabilité adaptées aux propriétés que l’on cherche à montrer. Elles se distinguent par la nature du langage de réalisation, on peut en effet prendre des entiers représentant des codes de fonction, ou bien un lambda-calcul pur ou typé ou tout autre langage. Ensuite on peut mettre différents ingrédients dans les formules de réalisabilité. Par exemple f appartient à l’interprétation de A ⇒ B peut être défini comme pour tout a dans l’interprétation de A, f(a) termine et est dans l’interprétation de B, ou bien on peut de plus demander que B soit démontrable, etc. Les preuves de normalisation par les méthodes de candidat de réductibilité peuvent se voir comme des cas particuliers de méthode de réalisabilité.
On peut définir la réalisabilité de manière sémantique, ou au contraire de manière syntaxique (on parle de réalisabilité abstraite), la propriété x r P qui dit qu’une réalisation x est dans l’interprétation d’une formule P est définie comme une formule du système logique lui-même, définie en général dans un fragment plus faible (on élimine les connecteurs intuitionnistes ∃ et ∨). Plus d’information sur la réalisabilité peut se trouver dans les livres de Troelstra [Tro73], Troelstra et van Dalen [TvD88] et Beeson [Bee85].
Nous décrivons trois notions de réalisabilité abstraite. Pour cela nous nous plaçons dans une arithmétique fonctionnelle du premier ordre qui est l’arithmétique que l’on étend de manière à pouvoir parler d’objets fonctionnels représentés par des λ-termes, on considère également la possibilité de former la paire de deux objets. Les objets de base sont les entiers. Un prédicat particulier x ∈ nat permet de distinguer les objets entiers. De manière usuelle, on écrira ∀ x ∈ nat.P pour ∀ x. x ∈ nat⇒ P et ∃ x ∈ nat.P pour ∃ x. x ∈ nat∧ P. La disjonction A ∨ B est définie comme ∃ b ∈ nat.(b=0 ⇒ A) ∧ (b≠0 ⇒ B).
La réalisabilité récursive a été introduite par Kleene [Kle45]. L’ensemble des réalisations est l’ensemble des fonctions récursives partielles. Une réalisation est forcément un objet qui a une valeur, soit un entier (qui peut représenter le code d’une fonction récursive) dans le cas de l’arithmétique du premier ordre, soit un entier ou une abstraction dans le cas de l’arithmétique fonctionnelle. On distingue un prédicat t⇓ qui est vrai lorsque le terme t a une valeur. Les quantifications portent implicitement sur les termes qui ont une valeur.
La définition de la réalisabilité récursive est décrite dans la figure 6.1.
x r A = x=0 ∧ A A atomique x r A∧ B = fst(x) r A ∧ snd(x) r B f r A⇒ B = ∀ x. x r A ⇒ f(x)⇓ ∧ f(x) r B x r ∃ y. B = snd(x) r B{y:=fst(x)} f r ∀ x.B = ∀ x. f(x)⇓ ∧ f(x) r B
Figure 6.1: Réalisabilité récursive
On montre que si une formule A est démontrable, alors on peut trouver un terme t tel que t ⇓ ∧ t r A soit démontrable.
La réalisabilité récursive sert à justifier par exemple le principe de Markov :
| (∀ x ∈ nat. P(x) ∨ ¬ P(x)) ⇒ ¬ ¬ ∃ x ∈ nat.P(x) ⇒ ∃ x ∈ nat.P(x) |
La réalisabilité récursive sert à justifier que le principe d’indépendance des prémisses n’est pas démontrable en logique intuitionniste :
| (¬ A ⇒ ∃ x.P(x)) ⇒ ∃ x. ¬ A ⇒ P(x) |
Tous les objets intermédiaires manipulés dans le programme ont une valeur ce qui permet d’assurer qu’un programme t qui réalise une formule pourra se calculer par une stratégie d’appel par valeur mais sans évaluer les termes sous les abstractions.
La réalisabilité modifiée (typée) a été introduite par Kreisel. Il s’agit d’assurer la terminaison des interprétations par une condition de bon typage. Les objets manipulés par la logique sont des termes typés dans un λ-calcul avec des types simples, un produit et des entiers. On notera explicitement le type des variables apparaissant dans les quantificateurs ∃ y:σ. P ou ∀ y:σ. P.
À chaque formule A est associé le type t(A) de ses réalisations. Dans la formule x r A, x représente une variable de type t(A).
t(A) = nat x r A = x=0 ∧ A A atomique t(A∧ B) = t(A) × t(B) x r A∧ B = fst(x) r A ∧ snd(x) r B t(A⇒ B) = t(A) → t(B) f r A⇒ B = ∀ x:t(A). x r A ⇒ f(x) r B t(∃ y:σ. B) = σ × t(B) x r ∃ y:σ. B = snd(x) r B{y:=fst(x)} t(∀ y:σ. B) = σ → t(B) f r ∀ x:σ. B = ∀ x:σ. f(x) r B
Figure 6.2: Réalisabilité modifiée
Une formule A est réalisable s’il existe un terme t de type t(A) tel que t r A soit prouvable.
Une manière alternative de présenter la réalisabilité modifiée est de prendre des suites finies de programmes pour les réalisations, on évite ainsi l’utilisation de produits, on peut de plus éliminer les réalisations des formules de Harrop.
La réalisabilité modifiée sert à justifier le principe d’indépendance des prémisses :
| (¬ A ⇒ ∃ x:σ.P(x)) ⇒ ∃ x:σ. ¬ A ⇒ P(x) |
La réalisabilité modifiée sert à justifier que le principe de Markov n’est pas démontrable en logique intuitionniste :
| (∀ x:nat. P(x) ∨ ¬ P(x)) ⇒ ¬ ¬ ∃ x:nat.P(x) ⇒ ∃ x:nat.P(x) |
Dans le cas de la réalisabilité modifiée, les réalisations sont des programmes typés fortement normalisables.
La réalisabilité modifiée non typée se place dans une logique où la quantification porte sur tous les objets qu’ils représentent ou non des programmes qui terminent. La définition est identique à celle de la réalisabilité modifiée décrite dans la figure 6.2. Simplement la condition pour qu’un programme t réalise une formule P est simplement que t r P et ne comporte plus de condition de bon typage de t.
Pour assurer la terminaison, il sera nécessaire que la formule à montrer explicite cette condition de terminaison. Par exemple, l’interprétation du prédicat de base x ∈ nat pourra être telle que l’existence d’une preuve de t ∈ nat assure que t est normalisable.
Une telle notion de réalisabilité est utilisée dans le système AF2 de J.-L. Krivine. Les formules utilisées pour garantir la terminaison des programmes ne permettent de garantir le calcul des valeurs que dans une stratégie paresseuse.
Lorsque la logique manipule des variables du second ordre, on ne sait pas a priori par quelle formule cette variable sera instanciée. On réalise donc cette variable par un prédicat unaire arbitraire.
|
Les formules auto-réalisées sont des formules pour lesquelles on connaît a priori une réalisation. Plus formellement, une formule P est auto-réalisée s’il existe un objet t tel que si P est réalisable alors t r P est vérifié.
Les formules de Harrop sont des formules auto-réalisées.
Par rapport à l’interprétation des preuves comme programmes par l’isomorphisme de Curry-Howard, l’introduction d’une notion de réalisabilité dans le Calcul des Constructions a pour but l’obtention de programmes plus efficaces ne conservant que la partie de la preuve utile pour le calcul des témoins. Elle sert également à justifier certaines propriétés qui ne sont pas démontrables.
On considère le Calcul des Constructions pur (sans univers et sans élimination forte sur les types inductifs) que nous noterons CC. On peut montrer que tout λ-terme pur typable dans CC est également typable dans le système Fω (avec types inductifs).
Cette propriété est simple à montrer. On associe à chaque terme t ou type de CC un terme ou un type E(t) dans Fω en oubliant les dépendances des types par rapport aux preuves et on montre que si ⊢ CC t:P alors ⊢ Fω E(t):E(P). La définition de la fonction d’oubli E(_) est donnée dans la figure 6.3.
E(Set) = Set E(X) = X X:A:Type E(x) = x x:A:Set E((x:A)B) = E(A) → E(B) A,B:Set E((X:A)B) = (X:E(A))E(B) A:Type,B:Set E((x:A)B) = E(B) A:Set,B:Type E((X:A)B) = E(A) → E(B) A,B:Type E([x:A]t) = [x:E(A)]E(t) t:B:Set ou A:Type E([x:A]t) = E(t) t:B:Type et A:Set E((t u)) = (E(t) E(u)) t:A:Set ou u:B:Type E((t u)) = E(t) t:A:Type et u:B:Set
Figure 6.3: Traduction de CC vers Fω
Cette traduction permet de montrer que 0≠1 n’est pas prouvable dans CC. En effet 0≠1 est une abréviation pour
| ((P:nat→ Set)(P 0)→(P 1))→ (C:Set)C |
S’il existait un terme de ce type, il y aurait également un terme de Fω de type E(0≠1) c’est-à-dire :
| ((P:Set)(P → P))→ (C:Set)C |
Mais comme il existe un terme de type (P:Set)(P → P) on aboutit à l’existence d’un terme de type (C:Set)C ce qui est absurde.
Une notion de réalisabilité modifiée naturelle est de demander de réaliser toute formule de P du Calcul des Constructions par un terme t de type E(P) qui satisfait de plus une certaine propriété x r P définie par récurrence sur P dans la figure 6.4. On commence par définir la formule x r P pour P:Set on aura également besoin de définir X r A lorsque A:Type ce qui est fait dans la figure 6.5. Dans le cas A:Type, X r A sera également une arité de type Type qui représente le type des prédicats de réalisabilité pour les objets d’arité A. Comme une proposition peut être formée par abstraction et application, nous définissons également dans la figure 6.6 une transformation R(P) qui s’applique à tous les objets P:A avec A:Type et qui coïncide avec la définition du prédicat λ x.x r A quand A est Set(en particulier R(A) a alors le type E(A) →Prop).
x r P = (R(P) x) P:Set et P n’est pas un produit f r (x:A)B = (x:E(A))x r A→ (f x) r B A,B:Set f r (X:A)B = (X:E(A))(Xr:X r A) (f X) r B A:Type,B:Set
Figure 6.4: Réalisabilité dans CC : x r P pour P:Set
X r Set = X → Prop F r (x:A)B = (x:E(A))F r B A:Set,B:Type F r (X:A)B = (X:E(A))(Xr:X r A)(F X) r B A,B:Type
Figure 6.5: Réalisabilité dans CC : x r P pour P:Type
R(X) = Xr X variable de prédicat R((P t)) = (R(P) E(t)) t:A:Set R((P T)) = (R(P) E(T) R(T)) T:A:Type R([x:A]P) = [x:E(A)]R(P) A:Set R([X:A]P) = [X:E(A)][Xr:X r A]R(P) A:Type R(P) = [x:E(P)]x r P si P est un produit
Figure 6.6: Réalisabilité dans CC : R(P) pour P:B:Type
À quelle condition un terme p réalise-t-il une preuve de l’égalité définie avec A:Set par :
| (P:A→ Set)(P t) → (P u) |
L’oubli des types dépendants n’est pas suffisant, il est important de pouvoir éliminer les parties de la preuve qui ne servent pas au calcul du résultat. La notion de formule de Harrop n’est pas naturelle dans un cadre d’ordre supérieur où il n’y a pas de formule atomique autre que les variables de prédicats.
Pour remédier à cela, Coq propose une distinction entre deux sortes Prop et Set. Les deux sortes sont imprédicatives, ce qui justifie les bonnes propriétés du système (il suffit d’identifier Prop et Set pour retrouver le calcul initial).
L’interprétation de t:A lorsque A:Prop est que A est vérifiée et que la preuve t de A ne sert pas au calcul. L’interprétation de t:A lorsque A:Set est que t est une preuve calculatoire de A dont il est possible d’extraire un programme.
Les règles de typage permettent d’assurer qu’aucun objet logique de sorte Prop ne sera utilisé pour la construction d’un objet calculatoire dans la sorte Set. Ceci permet de retirer de manière cohérente tout sous terme logique d’un terme calculatoire en préservant le résultat du calcul.
D’un point de vue technique, il faut étendre les notions d’extraction et de réalisabilité précédemment définies. La fonction d’extraction ne s’applique toujours qu’à des objets de type Set ou Type. Elle est définie dans la figure 6.7. La fonction de réalisabilité f r P s’applique à tous les objets de Set et Type et est définie figures 6.8, 6.9 et 6.10.
On dira que A:TypeP lorsque A est une suite de produits se terminant par Prop. La définition de la réalisabilité passe par la définition d’une transformation L(P) sur les objets de Prop ou TypeP qui est définie figure 6.11. Le rôle de cette transformation est d’ajuster les types des objets de Set ou Type apparaissant dans P en y appliquant la fonction d’extraction E(B). En particulier, si A est dans Prop, L(A) est aussi dans Prop.
E((x:A)B) = E(B) A:Prop ou A:TypeP E([x:A]t) = E(t) A:Prop ou A:TypeP E((t u)) = E(t) u:B:Prop ou u:B:TypeP
Figure 6.7: Extraction étendue à Prop
f r (x:A)B = (x:L(A))f r B (A:Prop ou A:TypeP) et B:Set f r (x:A)B = (x:L(A))f r B A:Prop et B:Type f r (x:A)B = (x:L(A))f r B A:TypeP et B:Type
Figure 6.8: Réalisabilité étendue à Prop : x r P avec P:Set
F r (x:A)B = F r B B:Type et A:Prop F r (X:A)B = (X:L(A))F r P B:Type et A:TypeP
Figure 6.9: Réalisabilité étendue à Prop : x r P pour P:Type
R((P t)) = R(P) P:B:Type et t:A:Prop R((P T)) = (R(P) L(T)) P:B:Type et T:A:TypeP R([x:A]P) = R(P) P:B:Type et A:Prop R([X:A]P) = [X:L(A)]R(P) P:B:Type et A:TypeP
Figure 6.10: Réalisabilité étendue à Prop : R(P) pour P:B:Type
L(Prop) = Prop L(X) = X X variable de type (B:TypeP ou B:Prop L((x:A)B) = (x:E(A))L(B) (B:TypeP ou B:Prop) et A:Set L((X:A)B) = (X:E(A))(Xr:X r A)L(B) (B:TypeP ou B:Prop) et A:Type L((x:A)B) = (x:L(A))L(B) (B:TypeP ou B:Prop) et A:TypeP L((x:A)B) = (x:L(A))L(B) (B:TypeP ou B:Prop) et A:Prop L((P t)) = (L(P) E(t)) P:B:TypeP et t:A:Set L((P T)) = (L(P) E(T) R(T)) P:B:TypeP et T:A:Type L((P T)) = (L(P) L(T)) (P:B:TypeP ou P:B:Prop) et T:A:TypeP L((P T)) = (L(P) L(T)) (P:B:TypeP ou P:B:Prop) et T:A:Prop L([x:A]P) = [x:E(A)]L(P) P:B:TypeP et A:Set L([X:A]P) = [X:E(A)][Xr:X r A]L(P) P:B:TypeP et A:Type L([X:A]P) = [X:L(A)]L(P) (P:B:TypeP ou P:B:Prop) et A:TypeP L([X:A]P) = [X:L(A)]L(P) (P:B:TypeP ou P:B:Prop) et A:Prop
Figure 6.11: Réalisabilité étendue à Prop : L(P)
Pour comprendre les interactions entre Prop et Set dans la réalisabilité, on peut prendre l’exemple de la définition imprédicative d’une famille list de listes d’objets de type A vérifiant un prédicat P. La famille list a pour type (A:Set)(A → Prop)→ Set et est définie par :
| list ≡ |
|
Le terme extrait de list est juste la définition usuelle des listes polymorphes. La propriété R(list) a pour type (A:Set)(Ar:A→Prop)(A → Prop)→ Prop et est définie par :
| R(list) ≡ |
|
On aurait pu choisir une autre notion d’extraction du contenu logique L(A) d’une proposition A. Par exemple, on aurait pu complètement ignorer les dépendances par rapport aux preuves logiques en modifiant la définition comme suit.
|
Dans un tel modèle, la propriété PI
| (A:Prop)(p,q:A)(P:A → Prop)(P p)→ (P q) |
qui dit que deux preuves dans un même type A:Prop sont égales aurait été vraie, c’est-à-dire que L(PI) qui se réduit à :
| (A:Prop)(p,q:A)(P:Prop)P → P |
est démontrable.
Les rôles de Prop et Set sont dissymétriques du fait de l’interprétation de réalisabilité. On peut plonger Prop dans un sous-ensemble de Set en faisant correspondre à A:Prop un ensemble à (il suffit de prendre (C:Set)(A → C)→ C)) qui a au plus un élément et qui est habité lorsque A est vérifié. On pourra montrer A ↔ Ã. La partie à → A peut se justifier dans CC par la réalisabilité. On peut également intégrer cet aspect directement dans le calcul par exemple par l’intermédiaire du sous-typage Prop ≤ Set.
Réciproquement, étant donné un type A:Set on peut cacher le contenu calculatoire des preuves de A en construisant Â:Prop tel que A →  et (C:Prop)(A → C)→  → C (il suffit de prendre (C:Prop)(A → C) → C). On n’a évidemment pas  → A mais  et A sont équivalents dès lors qu’il s’agit de montrer des propriétés logiques de type Prop.
Dans Coq les règles d’élimination des types inductifs permettent de faire la distinction entre Prop et Set. Lorsque c:I avec I instance d’une définition inductive alors :
On traite de manière un peu particulière les types I:A à un seul constructeur c:C tel que si on avait A:Type alors on aurait E(A)=Set et E(C)=E(I). C’est le cas en particulier des conjonctions sur des objets dans Prop ou bien de l’égalité. Dans ces cas-là, on peut justifier l’équivalence pour la réalisabilité de la définition inductive de I:A ou de I:A′ où A′ est obtenu en remplaçant Set par Prop à la fin de l’arité A. En pratique on traite ce cas en autorisant la construction par cas d’objets de type Set même si t:I:Prop. On étend la notion d’extraction pour que l’extraction de
| match t with (c x1… xp) ⇒ p end |
soit simplement l’extraction de p ce qui est possible car p a le bon type (les xi logiques, n’apparaissent pas dans P).
La notion d’extraction et de réalisabilité s’étend mal au cas des univers et de l’élimination forte sur les types inductifs. En effet la propriété d’oubli des dépendances ne s’applique plus. D’autre part les inclusions Prop ≤ Type et Set≤ Type qui sont essentielles pour un développement harmonieux sont incompatibles avec une extraction incrémentale, car il existe alors des types B:Type(n) (p.ex. (U:Type(1))U → U) dont des instances sont dans Type et d’autres sont dans TypeP. Il faut connaître le développement complet avant de décider si l’on doit extraire ou cacher les objets de B.
Le mécanisme d’extraction de Coq (à partir de la version 7) s’éloigne d’ailleurs du schéma présenté ici. La distinction TypeP et Type est abandonnée, et c’est une analyse ultérieure sur le programme qui permet de s’affranchir localement des occurrences de b:B:Type qui s’avèrent purement logique.
La distinction entre Prop et Set est utile sur le plan sémantique. En effet, certaines extensions (logique classique, extensionnalité,…) interagissent mal avec les aspects constructifs du Calcul des Constructions Inductives. Les prendre en compte simplement sur la sorte Prop permet de ne pas détruire la cohérence du système.
Tous les assistants de preuves permettant de manipuler des programmes intègrent une certaine notion d’objets logiques. Dans le système Nuprl, on utilise un opérateur pour cacher le contenu calculatoire des preuves analogue à notre construction Â. D’autres systèmes privilégient la notion de sous-ensemble, ou bien donnent un statut logique à des propriétés particulières comme l’égalité. Toutes ses méthodes sont héritées de la notion logique de formule non-calculatoire.
Le défaut de cette méthode est qu’elle ne permet pas de supprimer du programme certains arguments inutiles. C’est le cas des listes de longueur n, le constructeur cons aura pour type (n:nat)A → (list n) → (list (S n)) ce qui laisse un terme extrait de type nat→ A → list → list dans lequel chaque constructeur est appliqué à un argument de type entier représentant la longueur de la liste. Même si on le souhaite, les méthodes reposant sur la réalisabilité ne permettent pas aisément de supprimer cette composante.
Pour régler ce problème, on peut déplacer les marques des arités vers les quantifications. On introduit une quantification logique ∀ x:A.B avec
| E(∀ x:A.B)=E(B) et f r ∀ x:A.B=∀ x:A.f r B |
De tels systèmes ont été étudiés par Takayama [Tak91], Hayashi, ….
Une autre possibilité explorée plus récemment est de s’appuyer sur des méthodes d’analyse de code mort. Ces techniques ont été étudiées par Berardi [Ber96], Boerio [BB95], Damiani et Prost [DP98].
L’extraction a lieu a posteriori, le terme initial et le terme dans lequel on a retiré des parties de code mort sont prouvablement égaux pour une égalité extensionnelle (Berardi utilise une propriété générale qui dit que si deux termes du λ-calcul simplement typé ont le même type et que l’un est obtenu par élagage de certains sous-termes de l’autre alors les deux termes sont extensionnellement égaux).
Une des difficultés est qu’une même constante peut apparaître à plusieurs endroits avec des contenus calculatoires différents, d’où l’idée d’utiliser du sous-typage ou des types conjonctifs pour prendre en compte ce polymorphisme.
Le mécanisme d’extraction de Coq implante la fonction d’extraction E(_). Il se présente sous la forme d’une commande Extraction qui produit du code pour plusieurs langages de programmation fonctionnels (Ocaml, Haskell et Scheme). Cette commande peut être utilisée directement dans la boucle d’interaction de Coq pour afficher le code extrait :
La commande Recursive Extraction aura pour effet d’extraire récursivement tout ce qui est nécessaire. On peut également utiliser la commande Extraction pour écrire dans un fichier tout le code correspondant à un ensemble d’objets Coq (le caractère récursif est alors implicite) :
Coq < Extraction "arith.ml" plus mult.
Dans le cas d’Ocaml, une interface est également créée (fichier .mli).