Programmation impérative

Planche : 2

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

Des nombres qui changent

La capacité d’une salle de concert, vs. le nombre de places restantes.
La température de fusion de la glace, vs. la température à Palaiseau.
Une variable de PCF, vs. une variable de Java.

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.

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.

Quelle heure est-il ?
A-t-on réellement besoin de places(t-10) ?
Peut-on connaître places(t+10) ?

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

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 r₁, r₂ etc.

Opérations sur les références

Création
Let x = Ref 1
Création d’une nouvelle case. Noter : valeur initiale obligatoire (typage, contrôle de la programmation).
Regarder dans la case (valeur actuelle).
!x
Changer le contenu de la case (contribution à la construction de la fonction du temps).
x := 2

Dans un langage impératif

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

int x, y, z ;

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

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

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.

t₁ := !t₂ + 1

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

y := !x + 1

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

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.

E, m ⊢ t ↪ v, m′

L’évaluation du terme t dans l’env. E et le monde m produit la valeur v et change le monde en m′.

E donne la valeur des variables libres de t.
Le monde m donne les valeurs associées aux références.

Le changement de m en m′ vient en plus de la valeur v : rend compte des « effets de bord » (cf. « side effect »).

Syntaxe étendue

Cinq nouvelles constructions.

Planche : 12

Valeurs étendues

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

Des références notées r₁, r₂ etc, qui donnent accès aux paires du monde.
void, noté encore ().

type env = (string * value) list
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 t₁ ;t₂.

E, m ⊢ () ↪ (), m

E, m ⊢ t₁ ↪ v₁, m₁ E, m₁ ⊢ t₂ ↪ v₂, m₂

E, m ⊢ (t₁ ;t₂) ↪ v₂, m₂

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

E ⊢ t₁↪v₁ E ⊢ t₂↪v₂

E ⊢ (t₁ ;t₂)↪v₂

Planche : 16

Variante de la séquence

Si on souhaite ne pas oublier des valeurs v₁ potentiellement significatives.

E, m ⊢ t₁ ↪ (), m₁ E, m₁ ⊢ t₂ ↪ v₂, m₂

E, m ⊢ (t₁ ;t₂) ↪ v₂, m₂

Ainsi, on exige que t₁ 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.

E, m ⊢ t ↪ v, m′

E, m ⊢ (Ref t) ↪ r, (m′ ⊎ (r,v))

E, m ⊢ t ↪ r, m′ (r,v) ∈ m′

E, m ⊢ !t ↪ v, m′

E, m ⊢ t₁ ↪ r, m′ ⊎ (r,_) E, m′ ⊎ (r,_) ⊢ t₂ ↪ v, m″ ⊎ (r,_)

E, m ⊢ t₁ :=t₂ ↪ (), 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.

E, m ⊢ t₁ ↪ r, m′ ⊎ (r,_) E, m′ ⊎ (r,_) ⊢ t₂ ↪ v, m″ ⊎ (r,_)

E, m ⊢ t₁ :=t₂ ↪ (), m″ ⊎ (r,v)

t₁ est évalué avant t₂.
L’affectation change le dernier monde m″ ⊎ (r,_).

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 { (r_x, 1), (r_y, 1) }

Planche : 19

Variante de l’affectation

Pratiquée par Java (et C).

E, m ⊢ t₁ ↪ r, m′ ⊎ (r,_) E, m′ ⊎ (r,_) ⊢ t₂ ↪ v, m″ ⊎ (r,_)

E, m ⊢ t₁ :=t₂ ↪ v, m″ ⊎ (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

E, m ⊢ &x ↪ r, m

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.

E, m ⊢ n ↪ n, m

E, m ⊢ (Fun x -> t) ↪

<
<

x•t•E

>
>

, m

E, m ⊢ t₁ ↪ n₁, m₁ E, m₁ ⊢ t₂ ↪ n₂, m₂

E, m ⊢ (t₁ op t₂) ↪ (n₁ opn₂), m₂

E, m ⊢ t₁ ↪

<
<

x•t•E₁

>
>

, m₁ E, m₁ ⊢ t₂ ↪ v₂, m₂ E₁ ⊕ [x = v₂], m₂ ⊢ t ↪ v, m₃

E, m ⊢ (t₁ t₂) ↪ v, m₃

E, m ⊢ t₁ ↪ v₁, m₁ E ⊕ [x=v₁], m₁ ⊢ t₂ ↪ v₂, m₂

E, m ⊢ (Let x = t₁ In t₂) ↪ v₂, m₂

E, m ⊢ (Fix f -> Fun x -> t) ↪

(C=

<
<

x•t•E ⊕ [f=C]

>
>

)

, m

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

Planche : 22

Variante sans la séquence

La séquence t₁ ;t₂ est exprimable comme Let x = t₁ In t₂, où x ∉F(t₂).

E, m ⊢ t₁ ↪ v₁, m₁ E ⊕ [x=v₁], m₁ ⊢ t₂ ↪ v₂, m₂

E, m ⊢ (Let x = t₁ In t₂) ↪ v₂, m₂

Car la liaison impose d’évaluer t₁ avant t₂.

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

En Caml, on peut écrire.

let _ = t₁ in t₂ (* Variante qui oublie v₂ *)

let () = t₁ in t₂ (* Variante qui force v₁ vaut void *)

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

Planche : 23

Quelques trucs

Implémentation du monde, en Caml et en PCF.
Coder le Fix
Constructions impératives et appel par nom.

Planche : 24

Impact du transport du monde

Avant.

E ⊢ t₁↪n₁ E ⊢ t₂↪n₂

E ⊢ (t₁ op t₂)↪(n₁ opn₂)

Maintenant.

E, m ⊢ t₁ ↪ n₁, m₁ E, m₁ ⊢ t₂ ↪ n₂, m₂

E, m ⊢ (t₁ op t₂) ↪ (n₁ opn₂), m₂

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 :

E, m ⊢ t₁ ↪ v₁, m₁ E, m₁ ⊢ t₂ ↪ v₂, m₂

E, m ⊢ (t₁ ;t₂) ↪ v₂, m₂

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 (r_x,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 =

<
<

x•t•E ⊕ [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

Construire un arbre.
Let rf = Ref (Fun x -> x)

Let pow = Fun x -> Ifz x Then 1 Else 2 * !rf (x-1)
Boucler rf := pow.

Planche : 32

Appel par nom

Les règles sont parfaitement définies.

Rappel : En appel par valeur.

E(x) = v

E ⊢ x↪_vv

E ⊢ t₁↪_vv₁ E ⊕ [x = v₁] ⊢ t₂↪_vv

E ⊢ Let x = t₁ In t₂↪_vv

⋮

En appel par nom.

E(x) =

<
<

t•E′

>
>

E′ ⊢ t↪_nv

E ⊢ x↪_nv

E ⊕ [x =

<
<

t₁•E

>
>

]

⊢ t₂↪_nv

E ⊢ Let x = t₁ In t₂↪_nv

E ⊢ t₁↪_n

<
<

x•b•E₁

>
>

E₁ ⊕ [x,

<
<

t₂•E

>
>

]

⊢ b↪_nv

E ⊢ (t₁ t₂)↪_nv

…

Planche : 33

Le monde en appel par nom

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

E, m ⊢ t ↪ v, m′

E, m ⊢ (Ref t) ↪ r, (m′ ⊎ (r,v))

E, m ⊢ t ↪ r, m′ (r,v) ∈ m′

E, m ⊢ !t ↪ v, m′

⋮

Ou l’alternative logique :

E, m ⊢ (Ref t) ↪ r,

(m ⊎ (r,

<
<

t•E

>
>

))

…

Mais passons.

Et on transporte le monde.

E(x) =

<
<

t•E′

>
>

E′, m ⊢ t ↪ v, m′

E, m ⊢ x ↪ v, m′

E ⊕ [x =

<
<

t₁•E

>
>

]

, m ⊢ t₂ ↪ v, m′

E, m ⊢ (Let x = t₁ In t₂) ↪ v, m′

E, m ⊢ t₁ ↪

<
<

x•b•E₁

>
>

, m₁

E₁ ⊕ [x,

<
<

t₂•E

>
>

]

, m₁ ⊢ b ↪ v, m₂

E, m ⊢ (t₁ t₂) ↪ v, m₂

…

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 L^AT_EX par H^EV^EA

Planche : 1

Planche : 2

Planche : 3

Des nombres qui changent

Planche : 4

Une fonction du temps

Planche : 5

Le nombre de places disponibles

Planche : 6

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

Planche : 7

Opérations sur les références

Planche : 8

Dans un langage impératif

Planche : 9

Dans un langage impératif

En PCF

Planche : 10

Le monde

Planche : 11

Syntaxe étendue

Planche : 12

Valeurs étendues

Planche : 13

Le module World

Planche : 14

Règles des constructions impératives

Planche : 15

Séquence

Planche : 16

Variante de la séquence

Planche : 17

Références

Planche : 18

Affectation

Planche : 19

Variante de l’affectation

Planche : 20

Encore une variation

Planche : 21

Le reste des règles

Planche : 22

Variante sans la séquence

Planche : 23

Quelques trucs

Planche : 24

Impact du transport du monde

Planche : 25

Implémentation du monde

Planche : 26

Un bout d’interpréteur

Planche : 27

Usage du monde

Planche : 28

Caml est impératif

Planche : 29

Liaison dynamique

Planche : 30

Fermeture récursive

Planche : 31

Le Fix avec le Ref

Planche : 32

Appel par nom

Planche : 33

Le monde en appel par nom

Planche : 34

Un usage particulièrement délicat

Le module `World`