exam

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

Pour t₁ on peut prendre :

Let loop = Fix x -> x In 1

Pour t₂ on peut prendre :

Fix x -> x

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

Pour t₁ :

Let id = Fun x -> x In id id

Pour t₂, autant prendre un terme qui déclenche une erreur à l’exécution.

1 + (Fun 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 t → t′ 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

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

True↪True

False↪False

t↪True

!t↪False

t↪False

!t↪True

t₁↪False

t₁ && t₂↪False

t₁↪True t₂↪v

t₁ && t₂↪v

t₁↪True

t₁ || t₂↪True

t₁↪False t₂↪v

t₁ || t₂↪v

t₁↪True t₂↪v

If t₁ Then t₂ Else t₃↪v

t₁↪False t₃↪v

If t₁ Then t₂ Else t₃↪v

Question 7. Exprimer !t, t₁ && t₂ et t₁ || t₂ 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
t₁ `&&` t₂	∼	If t₁ Then t₂ Else False
t₁ `\|\|` t₂	∼	If t₁ Then True Else t₂

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

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 t↪v.

Montrons d’abord que t₁ && t₂↪v ⇒ T(t₁,t₂)↪v

On suppose

t₁↪False

t₁ && t₂↪False

On a donc t₁↪False. Alors, par l’axiome False↪False et la seconde règle du If, on a :

t₁↪False
False↪False

If t₁ Then t₂ Else False↪False
On suppose

t₁↪True t₂↪v

t₁ && t₂↪v

On a donc t₁↪True et t₂↪v, l’utilisation directe de ces hypothèses dans la première règle du If prouve T(t₁,t₂)↪v.

Réciproquement, on suppose T(t₁,t₂)↪v. Puisque T(t₁,t₂) est un terme If, il n’y a que deux règles possibles selon que l’on a t₁↪True ou t₁↪False.

Dans le premier cas, on a nécessairement t₂↪v et donc t₁ && t₂↪v.
Dans le second, v vaut nécessairement False, qui se trouve alors également être la valeur de t₁ && t₂ (première règle du &&).

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(t₁,t₂) (que l’on trouve dans beaucoup de copies).

If t₁ Then If t₂ Then True Else False Else False

Alors l’équivalence est fausse. Contre-exemple : supposer t₁↪True et t₂↪10, alors d’une part,

t₁↪True t₂↪10

t₁ && t₂↪10

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

If t₁ Then If t₂ 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 :

t₁↪False

t₁ && t₂↪False

t₁↪True t₂↪True

t₁ && t₂↪True

t₁↪True t₂↪False

t₁ && t₂↪False

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 ?

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.
Prouver directement les équivalences, ici c’est pas évident à formuler.
Traiter tous les cas possibles d’évaluation de t₁ et t₂, pour constater que t₁ && t₂ et T(t₁,t₂) s’évaluent pareillement. Alors, il faut penser à tous les cas, et ne pas oublier le cas où t₁ ne s’évalue pas en un booléen (i.e. la valeur de t₁ n’est pas un booléen, ou t₁ n’a pas de valeur), ainsi que le cas t₁↪True et t₂ 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 t₁ est True et que la valeur v de t₂ existe mais n’est pas un booléen, alors l’interprétation de t₁ && t₂ é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 t₁ est False, alors la valeur de t₁ && t₂ est également False, quelque soit le comportement de t₂ (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 t₂ 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 t₁ Then t₂ Else t₃| = |t₁|; Test(|t₃|,|t₂|)

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 t₁ && t₂.

|t₁ && t₂| = |If t₁ Then t₂ 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 E ⊢ t: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 ⊢ t₁:Bool E ⊢ t₂:Bool

E ⊢ t₁ && t₂:Bool

E ⊢ t₁:Bool E ⊢ t₂:Bool

E ⊢ t₁ || t₂:Bool

E ⊢ t₁:Bool E ⊢ t₂:A E ⊢ t₃:A

E ⊢ If t₁ Then t₂ Else t₃: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 E ⊢ 2:Nat (et non pas E ⊢ 2: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 ⊥_B ≼ true et ⊥_B ≼ false. 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 :

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.

⊥_{B ↦ B}, la fonction qui à tout élément de B, associe ⊥_B.
F la fonction constante qui à tout élément de B associe false.
I l’identité sur B.

Alors la dénotation du terme est la fonction de B dans B ↦ B, qui

À ⊥_B, associe ⊥_{B ↦ B}.
À false, associe F.
À true, associe I.

Annexes

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

Interpréteur par valeur

open Ast

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

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)::env) t2
| App (t1,t2) ->
    let x,t_clo,e_clo = inter_clo env t1 in
    let v2 = interv env t2 in
    interv ((x,v2)::e_clo) t_clo
| Fun (x,t) -> Clo_v (x,t,env)
| Fix (f,Fun (x,t)) ->
    let rec clo = Clo_v (x,t,(f,clo)::env) in
    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")

Quelques questions de cours

Extension de PCF par les booléens

Annexes

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

Interpréteur par valeur

Quelques questions de cours

Extension de PCF par les booléens

Annexes

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

Interpréteur par valeur

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