close

Se connecter

Se connecter avec OpenID

9 - ENS Cachan

IntégréTéléchargement
TD9
12 avril 2016
λ-Calcul et Logique Informatique
David Baelde
baelde@lsv.ens-cachan.fr
Exercice 1 — Connecteurs logiques dans le système F
On rappelle les règles de typage pour la nouvelle construction du système F, la
quantification du second ordre. On note en majuscule les variables de type, et
on suppose que la variable X n’apparaı̂t pas libre dans Γ.
Γ`u:F
Γ ` λX. u : ∀X. F
Γ ` u : ∀X. F
Γ ` u T : F [X := T ]
def
1. On pose ⊥ = ∀X. X. Démontrer ⊥ ⇒ P pour un type / une formule
quelconque P .
def
2. On pose A ∧ B = ∀X. (A ⇒ B ⇒ X) ⇒ X. Montrer que cet encodage
rend admissibles les règles usuelles de la conjonction, en donnant les
encodages correspondants pour les constructions de paire et projections :
Γ`u:A Γ`v:B
Γ ` hu, vi : A ∧ B
Γ ` u : A1 ∧ A2
Γ ` πi (u) : Ai
def
3. On pose A ∨ B = ∀X. (A ⇒ X) ⇒ (B ⇒ X) ⇒ X. Dériver les règles
usuelles :
Γ ` u : Ai
Γ ` ιi (u) : A1 ∨ A2
Γ`u:A∨B
Γ, x1 : A ` v1 : C
Γ, x2 : B ` v2 : C
Γ ` case(u, x1 .v1 , x2 .v2 ) : C
4. Proposer un encodage de ∃X. F qui permette de dériver les règles suivantes (où on suppose que X n’apparaı̂t pas dans Γ et P ).
Γ ` u : F [X := T ]
Γ ` u : ∃X. F
Γ ` hhT, uii : ∃X. F
Γ, x : F ` v : P
Γ ` CASE(u, x.v) : P
Remarque : on pourrait aussi vérifier que les réductions attendues (par exemple,
case(ιi (u), x1 .v1 , x2 .v2 ) → vi [xi := u]) sont simulées par nos encodages.
Exercice 2 — Types de données en système F
Nous allons maintenant exploiter le polymorphisme du système F pour pouvoir
typer les encodages vus au TD 2 (booléens, paires, entiers, listes. . . ).
1/2
λ-calcul et Logique Informatique
TD9
1. Les entiers naturels peuvent être définis comme les termes générés par la
signature { z : N, s : N ⇒ N }. En système F, le type N ainsi donné se
code en ∀X. X ⇒ (X ⇒ X) ⇒ X. Définir l’interprétation de z et s selon
cet encodage.
2. Montrer que tout terme clos u : N est β-équivalent à un (unique) entier
de Church λX.λz.λs. sn z. On écrira alors [u]−1 = n.
On pourra s’appuyer sur la caractérisation des formes normales en système
F : elles s’écrivent λV1 . . . λVm . x u1 . . . un où les V sont des variables de
terme ou de type.
Remarque : si on avait pris ∀X. (X ⇒ X) ⇒ X ⇒ X on aurait eu besoin
de la βη-équivalence.
3. Coder la multiplication par deux sur les entiers, comme une fonction
double : N ⇒ N. Enoncer et prouver sa correction.
4. On considère un type arbitraire T donné par un ensemble fini de constructeurs (Ci )1≤i≤n où chaque constructeur a un type de la forme A1 ⇒ . . . ⇒
An ⇒ T ⇒ . . . ⇒ T ⇒ T où les Ai sont déja des types de F. Expliquer
comment on peut encoder T et ses constructeurs en système F.
5. On définit le type B par trois constructeurs : b : B, i : B ⇒ B et o : B ⇒ B.
Donner l’encodage en système F du type B et de ses constructeurs.
6. Coder l’injection b2n : B ⇒ N définie par les équations suivantes :
b2n(b) = s z
b2n(i(x)) = s(double(b2n(x)))
b2n(o(x)) = double(b2n(x))
Que représente le type B via cette traduction ?
7. Pour les plus courageux, coder l’addition sur B : donner une fonction
bplus : B ⇒ B ⇒ B de telle sorte que pour tous termes x et y on a
plus (b2n x) (b2n y) = b2n (bplus x y).
2/2
Auteur
Document
Catégorie
Uncategorized
Affichages
4
Taille du fichier
121 KB
Étiquettes
1/--Pages
signaler