Preuves Constructives Examen DEA de Programmation

13 Décembre 2000

1 Echauffement

L’étudiant Géo Codetout a construit en théorie de Martin-Löf un terme clos t de type suivant :

t : Πx : nat.Σy : nat.((x = S(y) + x = 0).

Dites ce que l’on sait des formes normales des termes suivants : π_{1}(t (S(S(S(0))))), π_{1}(S(0)) et π_{1}(0).

2 Listes en déduction modulo

On se place en déduction modulo. La signature de la théorie considérée permet de décrire des listes d’entiers naturels ; on a donc les sortes nat et list. Les entiers sont construits à l’aide des constantes 0 et S, comme d’habitude. Les listes sont obtenues à partir des constantes suivantes :

– [] pour la liste vide,

– _:: _pour le cons,

– _@_pour la concaténation,

– rev(_) pour la fonction qui renverse une liste. Le cons et la concatenation sont notés de manière infixe. Comme d’habitude, on s’autorise a noter [a; b; c] pour, par exemple, a :: b :: c :: [].

On s’autorise à raisonner par récurrence structurelle sur les listes. Le principe de récurrence est semblable à l’axiome de Peano ; il est donné par le schéma de regles suivantes pour chaque prédicat P sur les listes :

\frac{Γ ⊢ P ([]) Γ ⊢ ∀nata.∀_{list}l.P (l) ⇒ P (a :: l)}{Γ ⊢ ∀_{list}l.P (l)} (RecL)

Par ailleurs, on raisonne modulo la congruence engendrée par les règles de réécriture suivantes :

[]@l ⊳ l  (1)
l@[] ⊳ l  (2)
(x :: l)@m ⊳ x :: (l@m)  (3)
(l@m)@n ⊳ l@(m@n)  (4)
rev([]) ⊳ []  (5)
rev(a : : l) ⊳ rev(l)@[a]  (6)
rev(l@m) ⊳ rev(m)@rev(l)  (7)

a) Donnez les signatures des différentes constantes.

b) Donnez une preuve que la fonction rev(_) est involutive :

∀_{list}l.rev(rev(l)) = l.

On rappelle à ce sujet les deux règles principales caractérisant l’égalité :

\overline{Γ ⊢ t = t}(refl)  \frac{Γ ⊢ P  Γ ⊢ t = u}{Γ ⊢ P′}(Leibniz)

Où, dans la seconde règle, P′ est obtenue en remplaçant une occurence de u par t.

c) On ajoute à la théorie un prédicat discr sur les listes, ainsi que les deux règles de réductions suivantes :

discr([]) ⊳ 0 = 0  (8)
discr(a :: l) ⊳ ⊥  (9)

Informellement, que “signifie” la proposition discr(l) ?

A l’aide de ce prédicat, donnez une preuve de la proposition [] = x :: l ⇒ ⊥.

d) Si vous deviez étendre la définition de discr, par quoi remplaceriez vous les points de suspension suivants :

discr(rev(l)) ⊳ ….

Informellement, expliquez pourquoi on ne peut pas ajouter une règle de la forme discr(l@m) ⊳ . . ..

3 Listes dans la théorie de Martin-Löf

On considère maintenant la théorie de Martin-Löf étendue par des listes. Seules les constantes [] et _:: _ sont primitives, ainsi que la familles d’opérateurs RecL_{P} pour calculer et raisonner sur les listes. Les règles sont donc :

\frac{Γ wf}{Γ ⊢ list : Type}  \frac{Γ wf}{Γ ⊢ [] : list}
\frac{Γ wf}{Γ ⊢ _:: _: nat → list → list}

\frac{Γ ⊢ P : list → Type}{Γ ⊢ RecL_{P} : (P []) → (Πa : nat.Πl′ : list.(P l′) → (P a :: l′)) → Πl : list.(P l)}

La β-réduction est étendue par les deux règles suivantes :

(RecL_{P} p_{0} p_{c} []) ⊳ p_{0}  (10)
(RecL_{P} p_{0} p_{c} a :: l) ⊳ (p_{c} a l (RecL_{P} p_{0} p_{c} l))  (11)

a) Définissez les fonctions _@_puis rev(_) dans cette théorie des types.

b) Certaines des réductions de la partie 2 sont directement vérifiées par ces nouvelles définitions. Lesquelles ?

c) Les autres réductions de la question 2 peuvent être transformées en égalités ; par exemple Πl : list.(l@[]) =list l. Enoncez tous ces lemmes. Dans quel ordre faut-il les prouver ? De quelles manières ?

d) Indiquez les étapes principales de la preuve de l’involutivité de rev(_).

4 Un doigt d’imprédicativité

Sauriez-vous définir la propriété “être divisible par trois” dans la théorie des types simples de Church ? Donnez le λ-terme qui définit ce prédicat.