COURS 544, EXAMEN FINAL

Luc Maranget

4 décembre 2007





⋆⋆⋆



Cet examen corrigé, en Postscript et en PDF



Quelques questions de cours


Question 1. Donner un terme de PCF t1, dont l’exécution termine en appel par nom et ne termine pas en appel par valeur ; puis un terme t2 dont l’exécution ne termine pas en appel par nom.

Pour t1 on peut prendre :
Let loop = Fix x -> x In 1
Pour t2 on peut prendre :
Fix x -> x


Question 2. Donner un terme t1 typable selon Damas et Milner mais pas selon Hindley (sections 6.2 et 6.1 du poly). Puis un terme t2 non-typable selon Damas et Milner.

Pour t1 :
Let id = Fun x -> x In id id
Pour t2, autant prendre un terme qui déclenche une erreur à l’exécution.
1 + (Fun x -> x)


Question 3. On propose les définitions suivantes pour un toplevel PCF.

Let b_true = Fun kt -> Fun kf -> kt;;
Let b_false = Fun kt -> Fun kf -> kf;;
Let b_loop = Fix x -> x;;

Donner les schémas de types de ces trois définitions selon le système de Damas et Milner. Puis donner une instance commune à ces trois schémas de types. On choisira cette instance de sorte que toutes les instances communes aux trois termes s’en déduisent par substitution de variables de type.

Le schéma type principal de b_true est ∀ X,Y[X -> Y -> X], celui de b_false est ∀ X,Y[X -> Y -> Y], et celui de b_loop est ∀ X[X].

L’instance « principale » commune demandée est X -> X -> X.


Question 4. Que peut-on dire de l’exécution d’un terme t tel que ⊢ t:X (le terme t a le type X dans l’environnement de typage vide). La réponse sera justifiée par l’emploi d’un théorème du cours.

L’exécution du terme t ne termine pas. En effet d’après la correction du typage (exprimée pour la sémantique à petit pas), on a alors tt′ entraîne ⊢ t′:X, et donc t* t″ entraîne ⊢ t″:X. Or, aucune forme normale ne possède le type X, puisque les formes normales sont soit les entiers (de type Nat) soit les fonctions (de type A -> B). L’exécution de t ne peut pas non plus produire de terme bloqué, puisque ceux-ci ne sont pas typables. On en déduit donc que l’exécution de t ne termine pas.

Extension de PCF par les booléens


Question 5. On considère d’abord l’extension de la syntaxe abstraite. Les termes additionnels sont définis par les symboles additionnels suivants.

Donner une déclaration en Caml du type des termes de PCF étendu, en étendant la définition donnée en annexe.

Par exemple
type t = …
Bool of bool
Not of t
And of t | Or of t
If of t * t * t


Question 6. Donner la sémantique à grand pas des nouvelles constructions, sous forme de jugements tv (section 2.4 du poly). On notera les points suivants :

TrueTrue
FalseFalse
tTrue
!tFalse
tFalse
!tTrue
t1False
t1 && t2False
t1True           t2v
t1 && t2v
t1True
t1 || t2True
t1False           t2v
t1 || t2v
t1True           t2v
If t1 Then t2 Else t3v
t1False           t3v
If t1 Then t2 Else t3v


Question 7. Exprimer !t, t1 && t2 et t1 || t2 uniquement à l’aide du If, des constantes True et False, et de PCF non-étendu. La sémantique donnée à la question précédente doit être respectée, sans que vous ayez à le prouver (cf. question suivante). La réponse à cette question peut servir à simplifier un interpréteur ou un compilateur de PCF étendu.

On définit :
!t  ∼  If t Then False Else True
t1 && t2  ∼  If t1 Then t2 Else False
t1 || t2  ∼  If t1 Then True Else t2


Question 8. Prouver que votre traduction de t1 && t2 est correcte vis à vis de la sémantique donnée à la question 6. C’est-à-dire, en notant T(t1,t2) votre réponse à la question précédente, prouver l’équivalence :

t1 && t2v ⇔T(t1,t2)↪v
La démonstration la plus sûre consiste à procéder par double implication, en discriminant selon la dernière règle appliquée pour prouver un jugement tv.

Montrons d’abord que t1 && t2vT(t1,t2)↪v

Réciproquement, on suppose T(t1,t2)↪v. Puisque T(t1,t2) est un terme If, il n’y a que deux règles possibles selon que l’on a t1True ou t1False.

Remarque : Cela peut paraître un peu piéton. Mais il faut effectivement faire très attention dans ce genre de preuve. Suppons par exemple la définition suivante de T(t1,t2) (que l’on trouve dans beaucoup de copies).

If t1 Then If t2 Then True Else False Else False

Alors l’équivalence est fausse. Contre-exemple : supposer t1True et t2↪10, alors d’une part,

t1True           t2↪10
t1 && t2↪10

Et d’autre part, on ne peut pas prouver :

If t1 Then If t2 Then True Else False Else False↪10

Puisque la valeur du terme ci-dessus ne peut être que True ou False. Or si on procède trop rapidement, on risque de ne pas remarquer ce détail.

Au passage, on peut proposer cette traduction, mais alors il faut considérer une autre sémantique, exprimée par exemple ainsi :

t1False
t1 && t2False
t1True           t2True
t1 && t2True
t1True           t2False
t1 && t2False

Remarque encore : Le correcteur connaît le résultat, ce qu’il veut savoir c’est si vous savez prouver le résultat. Votre but est de l’en convaincre.

De quelles techniques de preuve disposons nous ?

  1. Prouver les doubles implications. Sûr, mais lourd, pour alléger un peu on peut se permettre d’être de moins en moins précis.
  2. Prouver directement les équivalences, ici c’est pas évident à formuler.
  3. Traiter tous les cas possibles d’évaluation de t1 et t2, pour constater que t1 && t2 et T(t1,t2) s’évaluent pareillement. Alors, il faut penser à tous les cas, et ne pas oublier le cas où t1 ne s’évalue pas en un booléen (i.e. la valeur de t1 n’est pas un booléen, ou t1 n’a pas de valeur), ainsi que le cas t1True et t2 n’a pas de valeur.


Question 9. Écrire en Caml l’interprétation des nouvelles constructions. On procédera par extension de l’interpréteur (en appel par valeur) donné en annexe. On détaillera les modifications apportées au type value, à la fonction print_value et à la fonction interv.

Extension du type des valeurs

type value = … | Bool_v of bool

Nouvelle fonction print_value

let print_value chan v = match v with
  …
Bool_v true -> fprintf chan "true"
Bool_v false -> fprintf chan "false"

Nouvel interpréteur

let rec interv env t = match t with
  …
Bool b -> Bool_v b
Not t -> Bool_v (not (inter_bool env t))
(* On profite de ce que la sémantique de && et || est celle de Caml *)
And (t1,t2) ->
    Bool_v (inter_bool env t1 && inter_bool env t2)
Or (t1,t2) ->
    Bool_v (inter_bool env t1 || inter_bool env t2)
If (t1,t2,t3) ->
    interv env
      (if inter_bool env t1 then t2 else t3)

Avec la définition suivante de la fonction mutuellement récursive inter_bool (à la fin)

and inter_bool env t = match interv env t with
Bool_v b -> b
_        -> raise (Error "bool expected, got something else")

Remarque Notre interpréteur ne respecte pas la sémantique de la question 6 sur un point : si la valeur de t1 est True et que la valeur v de t2 existe mais n’est pas un booléen, alors l’interprétation de t1 && t2 échoue — alors que la semantique donne la valeur v. Ce point est mineur (on peut n’interpréter que des termes bien typés) et surtout traité dans une question ultérieure 12.

Un point plus important est bien traité : si la valeur de t1 est False, alors la valeur de t1 && t2 est également False, quelque soit le comportement de t2 (valeur booléene, valeur autre, non-terminaison). Ce bon comportement découle directement de la sémantique de && en Caml. Ce point est plus important car il comprend le cas significatif d’un terme t2 de type Bool (Question 11) dont l’évaluation ne termine pas.

Remarquons encore que nous pouvons écrire un interpréteur complètement conforme.

And (t1,t2) ->
    if inter_bool env t1 then
      interv env t2
    else
      Bool_v false

Ou même…

And (t1,t2) -> interv env (If (t1,t2,Bool false))


Question 10. Proposer un schéma de compilation (section 4.4 du poly) pour les nouvelles constructions vers la machine ASEC du cours non-modifiée. On pourra considérer, comme c’est l’usage, que la représentation machine du booléen False est l’entier zéro.

Trois règles de base :
|True| = Ldi 1
|False| = Ldi 0
|If t1 Then t2 Else t3| = |t1|; Test(|t3|,|t2|)
On notera l’inversion des arguments du Test, par rapport à la compilation du Ifz.

Il reste à exploiter la question 7. Voici par exemple la compilation de t1 && t2.

|t1 && t2| = |If t1 Then t2 Else False|


Question 11. Soit Bool, le type des booléens. Donner les règles de typage des nouvelles constructions, dans le style des jugements Et:A de la section 6.1 du poly. Les règles de typage seront les règles usuelles, qui correspondent par exemple à celles de Java ou de Caml.

E ⊢ True:Bool
E ⊢ False:Bool
E ⊢ t:Bool
E ⊢ !t:Bool
E ⊢ t1:Bool         E ⊢ t2:Bool
E ⊢ t1 && t2:Bool
E ⊢ t1:Bool         E ⊢ t2:Bool
E ⊢ t1 || t2:Bool
E ⊢ t1:Bool          E ⊢ t2:A           E ⊢ t3:A
E ⊢ If t1 Then t2 Else t3:A


Question 12. Soit le terme (True && 2) + 1. Ce terme est-il typable selon les règles de la question précédente ? Que se passe-t-il lors de l’exécution avec votre interpréteur ? Avec votre compilateur ?

Le terme n’est pas typable car E2:Nat (et non pas E2:Bool).

L’interpréteur échoue lors du calcul de True && 2 car il évalue 2 comme Num_v 2 – plus précisément c’est l’appel inter_bool (Num 2) qui va échouer. Le code ASEC en revanche s’exécute sans erreur et calcule la valeur entière 3.

Remarque : Ni l’interpréteur, ni la machine ASEC ne « vérifient les types », ils ne disent rien par ex. du terme 1 + True. Tous deux commencent à évaluer le terme, et réagiront lorsqu’une erreur de type empêche l’exécution de se poursuivre. — notons au passage que ces erreurs sont définies sur les valeurs et non sur les termes.

Dans le cas de la machine ASEC, aucune erreur ne se produit, mais le résultat rendu est non-conforme à la sémantique.


Question 13. Le domaine de booléens de Scott B est constitué de trois valeurs ⊥B, true et false, avec ⊥Btrue et ⊥Bfalse. On interprète le type Bool comme étant B. Dans le cadre de PCF explicitement typé, donner la sémantique dénotationnelle du terme suivant :

Fun (x:Bool) -> Fun (y:Bool) -> x && y

On remarquera qu’une fonction « à deux arguments » est en fait une fonction qui renvoie une fonction.

On définit les fonctions suivantes de B dans B. Alors la dénotation du terme est la fonction de B dans BB, qui

Annexes

Syntaxe abstraite des termes de PCF (fichier ast.mli)

type op = Add | Sub | Mul | Div

type t =
  | Num of int
  | Var of string
  | Op  of op * t * t
  | Ifz of t * t * t
  | Let of string * t * t
  | App of t * t
  | Fun of string * t
  | Fix of string * t

Interpréteur par valeur

open Ast

type
 value = Num_v of int | Clo_v of string * Ast.t * env
and
 env = (string * valuelist

open
 Printf
let
 print_value chan v = match v with
Num_v i -> fprintf chan "%i" i
Clo_v (_,_,_) -> fprintf chan "<fun>"


exception Error of string

let
 rec interv env t = match t with
Num i -> Num_v i
Var x ->
    begin try List.assoc x env
    with Not_found ->
      raise (Error ("variable: "^x^" undefined")) end
Op (op,t1,t2) ->
    let n1 = inter_int env t1 in
    let n2 = inter_int env t2 in
    Num_v
      (match op with
      | Add -> n1+n2
      | Sub -> let m = n1-n2 in if m < 0 then 0 else m
      | Mul -> n1*n2
      | Div -> n1/n2)
Ifz (t1,t2,t3) ->
    let v1 = inter_int env t1 in
    interv env (if v1 = 0 then t2 else t3)
Let (x,t1,t2) ->
    let v1 = interv env t1 in
    interv ((x,v1)::envt2
App (t1,t2) ->
    let x,t_clo,e_clo = inter_clo env t1 in
    let v2 = interv env t2 in
    interv ((x,v2)::e_clot_clo
Fun (x,t) -> Clo_v (x,t,env)
Fix (f,Fun (x,t)) ->
    let rec clo = Clo_v (x,t,(f,clo)::envin
    clo
Fix _ -> raise (Error "Fix allowed on Fun only")

and inter_int env t = match interv env t with
Num_v i -> i
Clo_v _ -> raise (Error "Int expected, got Clo")

and inter_clo env t = match interv env t with
Clo_v (x,t,e) -> (x,t,e)
Num_v _ -> raise (Error "Clo expected, got Int")

Ce document a été traduit de LATEX par HEVEA