Planche : 1


Programmation impérative


Planche : 2


A
Des nombres qui changent.
B
Formalisation des construction impératives.
C
Quelques trucs.

Planche : 3


Des nombres qui changent


Planche : 4


Une fonction du temps

La température à Palaiseau (ou à Brest) est une fonction du temps.

Mais vu de Palaiseau (ou de Brest) on se contente de mesurer (ressentir) la température.


Planche : 5


Le nombre de places disponibles

Change avec le temps.

Veut-on/Peut-on-le modéliser comme une fct places:Nat -> Nat ?

Si oui qqs questions.

En fait l’ordinateur possède une mémoire à l’état changeant, analogue d’un système physique qui ressent la température à Palaiseau.


Planche : 6


La référence, une adresse en mémoire civilisée

La mémoire est un grand tableau de cases.

On donne des noms aux cases (cellules).

Let x = Ref … In …

La valeur exacte des adresses est sans importance.

Ce sont des références, des constantes r1, r2 etc.


Planche : 7


Opérations sur les références


Planche : 8


Dans un langage impératif

Une variable est toujours une référence, pour créer, suffit de déclarer.

  int xyz ;

Changer le contenu d’une case, c’est contribuer à la construction de la fonction du temps.

  x = 1 ; y = 2 ; z = 3 ;

Planche : 9


Dans un langage impératif

Toutes les variables sont des références.

  y = x + 1 ; // Affecter y, lire x

À gauche de “=”, une variable ∼ une case à affecter, vs. à droite de “=”, une case à lire.



En PCF

Les opérations « affecter » et « lire » sont plus explicites.

  t1 := !t2 + 1

Le terme t1 s’évalue en une référence, le terme t2 s’évalue en une référence. Évidemment, t1 et t2 peuvent être des variables.

  y := !x + 1

Dans ce cas, l’environnement doit contenir des liaisons de x et y à des références.


Planche : 10


Le monde

Un modèle de la mémoire, ou de fonctions du temps vu de l’intérieur du système.

Un ensemble de paires (r,v), tel que (r,v) ∈ m et (r,v′) ∈ m entraîne v = v′ — r référence, peu importe ce que c’est précisément.

L’évaluation est donnée par une relation à cinq places.

Em ⊢ t ↪ vm
L’évaluation du terme t dans l’env. E et le monde m produit la valeur v et change le monde en m′.
Le changement de m en m′ vient en plus de la valeur v : rend compte des « effets de bord » (cf. « side effect »).

Planche : 11


Syntaxe étendue

Cinq nouvelles constructions.

type t =
Num of int | Var of string  | Op of op * t * t
App of t * t | Let of t * string * t
Fun of string * t | Fix of string * t
(* Syntaxe de PCF usuel *)
Ref of t (* Nouvelle référence, Ref t *)
Get of t (* Lecture, !t *)
Set of t * t (* Affectation, t1 :=t2 *)
Void (* Une nouvelle constante, notée () *)
Seq of t * t (* Séquence t1 ;t2 *)

Planche : 12


Valeurs étendues

Aux valeurs de PCF usuel (en appel par valeur), entiers n et fermetures <xtE>, on ajoute.

type env = (string * valuelist
and
 value =
Num_v of int | Clo_v of string * Ast.t * env
(* Valeurs de PCF usuel *)
Void_v
Ref_v of value World.ref

Planche : 13


Le module World

Pour le moment, le monde est une valeur (Caml) de type World.t

type 'a t (* Le type du monde *)
val create : unit -> 'a t (* Nouveau monde *)

type 'a ref (* Le type des références *)

(* Création d'une nouvelle case, renvoie une ref vers icelle *)

val alloc : 'a t -> 'a -> 'a ref * 'a t
(* Affectation *)
val set : 'a t -> 'a ref -> 'a -> 'a t
(* Lecture *)
val get : 'a t -> 'a ref -> 'a

Planche : 14


Règles des constructions impératives


Planche : 15


Séquence

La constante “void” () et la séquence t1 ;t2.

Em ⊢ () ↪ (), m
Em ⊢ t1 ↪ v1m1           Em1 ⊢ t2 ↪ v2m2
Em ⊢ (t1 ;t2) ↪ v2m2

L’enchaînement en séquence de t1 puis t2 est exprimé par la production puis l’usage de m1 (une espèce de relation de Chasles). Comparer avec :

E ⊢ t1v1         E ⊢ t2v2
E ⊢ (t1 ;t2)↪v2

Planche : 16


Variante de la séquence

Si on souhaite ne pas oublier des valeurs v1 potentiellement significatives.

Em ⊢ t1 ↪ (), m1           Em1 ⊢ t2 ↪ v2m2
Em ⊢ (t1 ;t2) ↪ v2m2

Ainsi, on exige que t1 s’évalue en “void”.

Dans ce cas (1 ; 2) est une erreur de type choisie.

Le contrôle statique des types reste possible (“void” seule valeur du type unit).


Planche : 17


Références

Créer une reférence, lire une référence, affecter une référence.

Em ⊢ t ↪ vm
Em ⊢ (Ref t) ↪ r, (m′ ⊎ (r,v))
Em ⊢ t ↪ rm′           (r,v) ∈ m
Em ⊢ !t ↪ vm
Em ⊢ t1 ↪ rm′ ⊎ (r,_)           Em′ ⊎ (r,_) ⊢ t2 ↪ vm″ ⊎ (r,_)
Em ⊢ t1 :=t2 ↪ ()m″ ⊎ (r,v)

Note : dans la première règle, r est nouveau, (exprimé par ⊎ + pas de paires avec la même référence), et on exige une valeur initiale.


Planche : 18


Affectation

La règle est particulièrement précise.

Em ⊢ t1 ↪ rm′ ⊎ (r,_)           Em′ ⊎ (r,_) ⊢ t2 ↪ vm″ ⊎ (r,_)
Em ⊢ t1 :=t2 ↪ ()m″ ⊎ (r,v)

Ainsi, nous connaissons la sémantique de par ex.

Let x = Ref 0 In Let y = Ref 1 In
(Ifz !x Then x Else y) := !x + 1

Le monde final est { (rx, 1), (ry, 1) }


Planche : 19


Variante de l’affectation

Pratiquée par Java (et C).

Em ⊢ t1 ↪ rm′ ⊎ (r,_)           Em′ ⊎ (r,_) ⊢ t2 ↪ vm″ ⊎ (r,_)
Em ⊢ t1 :=t2 ↪ vm″ ⊎ (r,v)

Permet ce genre de truc :

   x = (y = 1) ;

À comprendre avec des parenthèses.


Planche : 20


Encore une variation

En C, il est possible de récupérer la référence associée à une case Avec l’opérateur « & ».

On peut se hasarder à lui donner une sémantique (au moins dans le cas où on l’applique à une variable.

E(x) = r
Em ⊢ &x ↪ rm

Le type d’une référence est « pointeur vers le type du contenu de la case », noté t*.

  int x = 1 ;
  int * p = &x ; /* p est une référence vers la case de nom x */
  *p = 2 ;       /* !p := 2, en quelque sorte */

Planche : 21


Le reste des règles

Extension des règles de l’amphi 03. Transporter le monde.

Em ⊢ n ↪ nm
Em ⊢ (Fun x -> t) ↪ 
<
<
xtE>
>
m
Em ⊢ t1 ↪ n1m1           Em1 ⊢ t2 ↪ n2m2
Em ⊢ (t1 op t2) ↪ (n1 opn2), m2
Em ⊢ t1 ↪ 
<
<
xtE1>
>
m1           Em1 ⊢ t2 ↪ v2m2           E1 ⊕ [x = v2], m2 ⊢ t ↪ vm3
Em ⊢ (t1 t2) ↪ vm3
Em ⊢ t1 ↪ v1m1           E ⊕ [x=v1], m1 ⊢ t2 ↪ v2m2
Em ⊢ (Let x = t1 In t2) ↪ v2m2
Em ⊢ (Fix f -> Fun x -> t) ↪ 
(C=<
<
xtE ⊕ [f=C]>
>
)
m

(Fermeture récursive, cf. fin du cours 03.)


Planche : 22


Variante sans la séquence

La séquence t1 ;t2 est exprimable comme Let x = t1 In t2, où xF(t2).

Em ⊢ t1 ↪ v1m1           E ⊕ [x=v1], m1 ⊢ t2 ↪ v2m2
Em ⊢ (Let x = t1 In t2) ↪ v2m2

Car la liaison impose d’évaluer t1 avant t2.

Une construction spécifique de la séquence reste plus parlante.

En Caml, on peut écrire.


let _ = t1 in t2   (* Variante qui oublie v2 *)

let () = t1 in t2  (* Variante qui force v1 vaut void *)

(NB. Dans les deux cas l’environnement d’évaluation de t2 n’est pas étendu.)


Planche : 23


Quelques trucs


Planche : 24


Impact du transport du monde

Avant.

E ⊢ t1n1           E ⊢ t2n2
E ⊢ (t1 op t2)↪(n1 opn2)

Maintenant.

Em ⊢ t1 ↪ n1m1           Em1 ⊢ t2 ↪ n2m2
Em ⊢ (t1 op t2) ↪ (n1 opn2), m2

L’usage du monde impose de spécifier l’ordre d’évaluation, ici c’est de gauche à droite. On aurait pu choisir l’autre sens, mais on doit choisir.

Et de même pour l’application etc.


Planche : 25


Implémentation du monde

Voici une réalisation où le monde est une liste de valeurs.

exception Error of string
type
 'a t = 'a list
type
 'a ref = int (* Référence = indice  dans la liste *)

let alloc w v0 = w@[v0], List.length w

let
 get w i =
  try List.nth w i
  with Failure _ -> raise (Error "Get")

let rec set w i vi = match i,w with
| 0,_::w -> vi::w
_,v::w -> v::set w (i-1) w
_,_ -> raise (Error "Set")

Planche : 26


Un bout d’interpréteur

Une règle :

Em ⊢ t1 ↪ v1m1           Em1 ⊢ t2 ↪ v2m2
Em ⊢ (t1 ;t2) ↪ v2m2
let rec inter e m t = match t with

Seq (t1,t2) ->
   let _,m1 = inter e m t1 in
   let v2,m2 = inter e m1 t2 in
   v2,m2
Op (Add,t1,t2) ->
   let n1,m1 = inter_int e m t1 in
   let n2,m2 = inter_int e m1 t2 in
   Num_v (n1+n2),m2

Planche : 27


Usage du monde

L’usage du monde suit une « relation de Chasles ». Le paramètre monde suit exactement le temps.

let rec inter e m t = match t with

Seq (t1,t2) ->
   let _,m = inter e m t1 in
   let v2,m = inter e m t2 in
   v2,m
Op (Add,t1,t2) ->
   let n1,m = inter_int e m t1 in
   let n2,m = inter_int e m t2 in
   Num_v (n1+n2),m

Planche : 28


Caml est impératif

On peut implémenter les références de PCF par celles de Caml.

type value = … | Ref_v of value ref

let
 rec inter e t = match t with

Seq (t1,t2) ->
   let _ = inter e t1 in (* Respecter l'ordre *)
   let v2 = inter e t2 in
   v2
Op (Add,t1,t2) ->
   let n1 = inter_int e t1 in
   let n2 = inter_int e t2 in
   Num_v (n1+n2)

Mais un monde explicite reste indispensable pour implémenter PCF impératif dans PCF.


Planche : 29


Liaison dynamique

Le monde donne accès à des valeurs « à un instant donné »

Let x = Ref 0 In
Let
 addx = Fun y -> !x + y In
x
 := 3 ; addx 1

Le résultat est 4.

C’est à dire que « !x » est calculé dans un monde (rx,3) (i.e. valeur à l’appel et pas lors de la définition de addx.)

La liaison « dynamique » est une généralisation excessive de ce comportement : l’environnement est traité comme un monde.

Let x = 0 In (* Env: (x,1) *)
Let addx = Fun y -> x + y In
Let
 x = 3 In  (* Env: (x,3) *)
addx 1        (* x+y évalué dans (x,3); (y,1) *)

Planche : 30


Fermeture récursive

La valeur de Fix f -> Fun x -> t est la fermeture récursive.

C = <
<
xtE ⊕ [f = C]>
>

Qui est une notation pour le graphe.

Nous pouvons fabriquer ce graphe avec une référence…


Planche : 31


Le Fix avec le Ref


Planche : 32


Appel par nom

Les règles sont parfaitement définies.

Rappel : En appel par valeur.

E(x) = v
E ⊢ xvv
E ⊢ t1vv1           E ⊕ [x = v1] ⊢ t2vv
E ⊢ Let x = t1 In t2vv

En appel par nom.

E(x) = <
<
tE>
>
         E′ ⊢ tnv
E ⊢ xnv
E ⊕ [x = <
<
t1E>
>
]
 ⊢ t2nv
E ⊢ Let x = t1 In t2nv
E ⊢ t1n
<
<
xbE1>
>
         
E1 ⊕ [x,<
<
t2E>
>
]
 ⊢ bnv
E ⊢ (t1 t2)↪nv

Planche : 33


Le monde en appel par nom

Formellement rien de neuf, on conserve les règles des références.

Em ⊢ t ↪ vm
Em ⊢ (Ref t) ↪ r, (m′ ⊎ (r,v))
Em ⊢ t ↪ rm′           (r,v) ∈ m
Em ⊢ !t ↪ vm

Ou l’alternative logique :

Em ⊢ (Ref t) ↪ r
(m ⊎ (r,<
<
tE>
>
))

Mais passons.

Et on transporte le monde.

E(x) = <
<
tE>
>
         E′, m ⊢ t ↪ vm
Em ⊢ x ↪ vm
E ⊕ [x = <
<
t1E>
>
]
m ⊢ t2 ↪ vm
Em ⊢ (Let x = t1 In t2) ↪ vm
Em ⊢ t1 ↪ 
<
<
xbE1>
>
m1          
E1 ⊕ [x,<
<
t2E>
>
]
m1 ⊢ b ↪ vm2
Em ⊢ (t1 t2) ↪ vm2

Planche : 34


Un usage particulièrement délicat

Let x = Ref 0
Let id = Fun x -> x
Let
 kx = Fun y -> !x

Soit le terme t = (x := !x+1 ; !x).

La valeur de id t est 1.

La valeur de kx t est 0.

Considérer maintenant :

Let f = Fun x -> x + x

Et la valeur de f t, qui est 3.

Les effets de bord sont retardés : en pratique c’est inutilisable car bien confus.


Ce document a été traduit de LATEX par HEVEA