Majeure M1Cours Langages de Programmation
COMPOSITION D'INFORMATIQUE
Jean-Jacques Lévy
5 Décembre 2000, 3h
Avertissement
On attachera une grande importance à la clarté, à la
précision, à la concision de la rédaction. Seules les notes de
cours sont autorisées.
Question 1Variables libres et liées.
a) Soit M = (l f.l g.l x.g
x+3)(l x.x+4)(l y.x+y). Est-ce que f, g, x, y sont libres dans M?
b) Calculer M[f\ g], M[g\ f], M[x\ x+y],
M[y\ x+y].
c) Calculer la valeur de (l f.l g.l x.l y.M) I
J 3 2 1 avec I=l x.x, J =l x.2 en expliquant tous les pas
élémentaires de calcul.
Question 2On considère PCF avec les listes et la fonctionnelle
foldR2 telle que
foldR2 f
(a1 :: a2 ··· :: an :: nil)
(b1 :: b2 ··· :: bn :: nil)
c = f a1 b1 (f a2 b2 (··· (f an bn c)))
(n ³ 0)
a) Exprimer foldR2 en PCF.
b) Déterminer son type en appliquant rigoureusement les
règles de typage de PCF.
Question 3Un appel de fonction est déplié (inlining) quand son
invocation est remplacée par la substitution des arguments dans son
corps de fonction: (l x.M)N remplacé par M[x\ N].
a) Précisez quand cette opération est valide.
b) Quels sont les avantages et les inconvénients du dépliage.
Question 4Récursion
a) Exprimer letrec x = M in N en PCF. Exprimer µ
x. M en fonction de letrec .
b) Donner une règle de réduction pour letrec .
c) On rajoute une constante Y à PCF telle que Y M ® M
(Y M). Exprimer µ x.M en fonction de Y et de M.
d) Montrer que Y est déjà exprimable par une expression
bien typée de PCF.
e) Quelle est la valeur de (l f. µ x. f x) (l y. 2)?
Question 5On considère PCF sans références, ni objets, mais avec les
listes et les tableaux.
a) Quels sont les shémas de types des tableaux
[| nil |] et [| l x.x |], et des fonctions l x.x[0]
et l x.l y.x[0] ¬ y.
Peut-on généraliser les variables de type de ces termes?
b) Les débordements de tableaux sont-elles les seules
erreurs possibles à l'exécution? Montrer que les tableaux ne vérifient
pas le théorème de progression?
c) Donner une règle de typage pour les tableaux qui permette
d'exprimer les algorithmes de tri sur les tableaux comme des fonctions
de type polymorphe, et qui vérifie le théorème de progression.
Question 6On rajoute les exceptions à PCF. On étend l'ensemble des
termes par:
| M, N, P |
::= |
... |
|
|
| |
| |
fail |
|
exception levée |
| |
| |
try M with N |
|
gestionnaire de l'exception |
Le terme try M with N calcule M
sauf si fail est exécuté dans M, auquel cas il renvoie N.
a) Un contexte est un terme C[ ] avec un trou
(sous-terme manquant). Et C[M] désigne le terme obtenu en mettant
M à la place du trou. Un contexte est actif si son trou est
en position évaluable. Ainsi C[ ]=[ ]2 ou
C'[ ]=(l x.x)(2+[ ]) sont des contextes actifs; mais
C[ ]=(l x.[ ])M n'en est pas un (puisqu'on ne calcule pas à
l'intérieur d'une valeur).
Donner les règles de réduction pour calculer try M with N avec
l'aide d'un ensemble de contextes actifs soigneusement définis.
b) Rajouter les exceptions à l'espace des valeurs
V. Donner la sémantique bigstep pour |- try M
with N = V.
c) Donner sa règle de typage, ainsi que celle pour le terme
fail.
d) Quelles modifications doit-on faire à l'algorithme W pour
tenir compte de cette nouvelle instruction.
e) On donne maintenant un argument à fail, qu'il est
plus judicieux d'appeler maintenant failwith. Ainsi l'espace des
termes est
| M, N, P |
::= |
... |
|
|
| |
| |
failwith M |
|
exception levée |
| |
| |
try M with N |
|
gestionnaire de l'exception |
Alors l'instruction try M with l x.N renvoie N[x\ V] si
failwith V est exécuté dans M. Recommencer les questions précédentes
avec cette nouvelle construction.
f) Donner une piste pour construire un système de type plus
robuste?
Question 7Codage des entiers unaires avec les objets dans PCF (sans
les constantes n entières).
a) On représente les entiers par un objet à trois champs:
|
|
= |
{est_zero= true; pred= z x.... ;
succ = z x.... } |
|
|
= |
{est_zero= false; pred= z x.... ;
succ = z x.... } |
Donner une expression possible pour les deux méthodes pred
et succ donnant le prédécésseur et le successeur de tout
entier naturel. (On posera true=0 et
true=1 pour obtenir des termes de corrects de PCF
en l'absence de booléens).
b) Donner un codage (toujours dans les objets
non-modifiables) qui minimise le nombre d'objets créés.
This document was translated from LATEX by HEVEA.