Interprétation (environnements)

Planche : 2

A: Un petit tour autour du point fixe.
B: De l’évaluaton à l’interprétation : environnements.
C: Interprétation par valeur.

Point fixe et réduction

On s’intéresse aux « solutions » d’équations du genre :

x =_s t, avec x variable, et t terme de PCF où x apparaît.

« =_s » est l’égalité dans la sémantique.

Soit u = Fix x -> t avec

u—→[u\x]t

C’est-à-dire, inventons le point fixe explicite.

On pose l’exigence sémantique t—→t′ ⇒ t =_s t′.

Il est alors évident que u est solution de x =_s t.

Point fixe construit

Une première étape : « abstraire x dans t ».

x = (Fun y -> t′) x, avec t′ = [y\x]t.

On a trivialement (Fun y -> t′) x—→t.
Il apparaît clairement que l’on recherche le point-fixe (x = Φ x) d’une fonction Φ = Fun y -> t′.

Soit un terme u tel que u—→^*Φ u—→[u\y]t′,

Soit en fait (car t′ = [y\x]t) :

u—→^*[u\y][y\x]t = [u\x]t

C’est à dire que u est solution.

Construction explicite

De u tel que u ←→^* Φ u.

Soit la fonction suivante curry :

Fun f -> (Fun x -> f (x x)) (Fun x -> f (x x))

On va montrer que pour tout terme Φ :

curry Φ ←→^* Φ (curry Φ)

(←→^* fermeture réflexive-symétrique-transitive de —→, entraîne =_s).

Démonstration de `curry` Φ ←→^* Φ (`curry` Φ)

Posons v = Fun x -> f (x x) Par une β-réduction il vient :

v v—→f (v v)

Lemme : t—→t′ ⇒ [u\x]—→[u\x]t′

Donc : [Φ\f](v v)—→[Φ\f]f (v v). (1)

Or (une β) : curry Φ—→[Φ\f](v v) (2)

Et c’est fini :

curry Φ —→ [Φ\f](v v) —→ [Φ\f](f (v v)) = Φ ([Φ\f](v v)) ←— Φ (curry Φ)

Astuce ultime

Notons F = Fix x -> t. On effectue les substitution de x dans t, dès que prêt :

F → [F\x]t → [[F\x]t\x]t → [[[F\x]t\x]t\x]t → …

On obtient un terme « infini », représentable par un graphe :

Plus clair sur un exemple

Fabriquer un tel graphe

En Caml, une définition récursive !
let rec pcf_fact =
  Fun ("n",
    Ifz (Var "n", Num 0,
      Op (Mul,Var "n",
        App (pcf_fact,Op (Sub,Var "n",Num 1)))))
En Java/langage machine : modification d’un terme.
Pcf node =
new App (null, new Op(Sub, new Var ("n"), new Num (1))) ;
Pcf top = new Fun("n",new Ifz (…)) ;
node.left = top

Environnements

Appel par nom

t₁↪_nFun x -> t₃ [t₂\x]t₃↪_nv

t₁ t₂↪_nv

Fun x -> t↪_nFun x -> t

[t₁\x]t₂↪_nv

Let x = t₁ In t₂↪_nv

[(Fix x -> t)\x]t↪_nv

Fix x -> t↪_nv

t₁↪_n0 t₂↪_nv

Ifz t₁ Then t₂ Else t₃↪_nv

t₁↪_nn (n ≠ 0) t₃↪_nv

Ifz t₁ Then t₂ Else t₃↪_nv

t₁↪_nn₁ t₂↪_nn₂

t₁ op t₂↪_nn₁ op n₂

n↪_nn

Appel par valeur

t₁↪_vFun x -> t₃ t₂↪_vv₂ [v₂\x]t₃↪_vv

t₁ t₂↪_vv

Fun x -> t↪_vFun x -> t

t₁↪_vv₁ [v₁\x]t₂↪_vv

Let x = t₁ In t₂↪_vv

[(Fix x -> t)\x]t↪_vv

Fix x -> t↪_vv

t₁↪_v0 t₂↪_vv

Ifz t₁ Then t₂ Else t₃↪_vv

t₁↪_vn (n ≠ 0) t₃↪_vv

Ifz t₁ Then t₂ Else t₃↪_vv

t₁↪_vn₁ t₂↪_vn₂

t₁ op t₂↪_vn₁ op n₂

n↪_vn

Substitution (dans un évaluateur)

Pour évaluer (Fun x -> t₁) t₂,on calcule [t₂\x]t₁ (ou [v₂\x]t₁)

Si t₂ n’a pas de variable libre, alors la substitution est simplifiée :

[t₂\x](Fun x -> t₁) = Fun x -> t₁

[t₂\x](Fun y -> t₁) = Fun y -> [t₂\x]t₁

Et c’est tout, car y n’est certainement pas libre dans t₂ .

Toutefois,

La substitution reste chère (copie de termes).
Les corps de fonctions sont transformés (ce qui éloigne du modèle où les fonctions sont du code).

On veut mélanger évaluation et substitution, comme on avait mélangé recherche de radical et réduction.

Substitution

Pour évaluer (Fun x -> (x * x) + x) 4 — noté (Fun x -> t) 4.

(Fun x -> t)↪_n(Fun x -> t)

4↪_n4 4↪_n4

4 * 4↪_n16

4↪_n4

(4 * 4) + 4↪_n20

(Fun x -> t) 4↪_n20

Évaluer Fun x -> t.
Effectuer la substitution [4\x]t, ce qui donne (4 * 4) + 4.
Et un peu d’arithmétique (calculer (4 * 4) + 4).

Une alternative

Garder la définition x = 4 dans un environnement.
Évaluer le terme ouvert dans cet environnement, noté E ⊢ t↪v.

[x = 4] ⊢ x↪4 [x = 4] ⊢ x↪4

[x = 4] ⊢ (x * x)↪16

[x = 4] ⊢ x↪4

[x = 4] ⊢ (x * x) + x↪20
La règle nouvelle étant du genre

[x=n] ⊢ x↪n
Cela revient à retarder la substitution, jusqu’à l’évaluation du corps de la fonction.

Priorité (à droite)

Valeur de Let x = 4 In Let x = 5 In x ?

En toute rigueur

[5\x]x↪_n5

Let x = 5 In x↪_n5

[4\x](Let x = 5 In x)↪_n5

Let x = 4 In Let x = 5 In x↪_n5

Effectuer [4\x](Let x = 5 In x), soit Let x = 5 In x.
Effectuer [5\x]x, soit 5.
Évaluer le résultat (qui est en forme normale).
En gros, on a calculé [4\x]([5\x]x).

Priorité avec les environnements

Un environnnement contient maintenant plusieures définitions x=n, et on applique la priorité.

[x = 4, x = 5] ⊢ x↪5

[x = 4] ⊢ Let x = 5 In x↪5

⊢ Let x = 4 In Let x = 5 In x↪5

Évaluer Let x = 5 In x dans l’env. [x = 4].
Évaluer x dans l’env. [x = 4, x = 5].
Ce qui nous donne 5 qui est une valeur.
Les définition de l’env. sont à considérer dans l’ordre.

Formalisation de la liaison lexicale

On pourrait écrire :

[…, x=n] ⊢ x↪n

[…] ⊢ x↪n

[…, y=n_y] ⊢ x↪n

[…, x=n] ⊢ t↪v

[…] ⊢ Let x = n In t↪v

On préfère une notation plus abstraite.

E(x) = n

E ⊢ x↪n

E ⊕ [x = n] ⊢ t↪v

E ⊢ Let x = n In t↪v

Les environnements sont des fonctions des variables. Avec un opérateur ⊕ défini par

(E ⊕ [x = n])(x) = n

(E ⊕ [x = n])(y) = E(y)

Implémentation de la liason lexicale

Avec de bêtes listes d’associations :

type 'a env = (Var.t * 'a) list

Opération « ⊕ ».

(* Ajouter l'association de x à t *)
let add x t env = (x,t)::env

Recherche :

let rec find x env = match env with
| [] -> raise (Error ("Variable libre : " ^ x))
| (y,t)::env -> if x=y then t else find x env

(C’est List.assoc).

La priorité à droite devient la priorité à gauche :

find x ((x,t₁)::(x,t₂)::…) → t₁

Mais c’est pareil.

Exemples

Généralisons les définitions des environnements : [x = t] (et non plus slt [x=n]).

On interprète Let y = 4 + 5 In y + 3 dans l’env. vide.
On interprète y + 3 dans [y = (4 + 5)].
On interprète y dans [y = (4 + 5)].
On interprète 4 + 5 dans… peu importe : terme clos.

Recommençons.

On interprète Let y = 4 + x In y + 3 dans [x = 5].
On interprète y + 3 dans [x = 5, y = (4 + x)].
On interprète y dans [x = 5, y = (4 + x)].
On interprète 4 + x dans … [x = 5] ?

**Le glaçon (thunk)**

Dans l’exemple précédent, nous avons négligé la définition de la substitution.

On interprète Let y = 4 + x In y + 3 dans [x = 5].

Donc on considère

[5\x](Let y = 4 + x In y + 3)

C’est-à-dire

Let y = [5\x](4 + x) In [5\x](y + 3)

Principe de l’interprétation = ne pas substituer par avance.

Donc, les environnements contiennent des applications de substitutions retardées : des glaçons, notés <t•E>.

Reprenons

Le terme clos 5 se représente facilement comme le glaçon <5•[]>

On interprète Let y = 4 + x In y + 3 dans [x = <5•[]>].
On interprète y + 3 dans [x = <5•[]>, y = <4 + x•[x = <5•[]>]>].
On interprète y dans [x = <5•[]>, y = <4 + x•[x = <5•[]>]>].
- Et donc on évalue 4+x dans l’environnement [x = <5•[]>].
- Ce qui finira par donner 9
Ce qui finira par donner 9 + 3 et donc 12.

Les règles de l’interprétation

Sachant que l’environnement lie des variables à des glaçons, qui sont eux-mêmes des paires « terme × environnement ».

Deux règles « faciles »

E(x) = <t•E′> E′ ⊢ t↪v

E ⊢ x↪v

E ⊕ [x = <t₁•E>] ⊢ t₂↪v

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

Mais aussi, bien évidemment, l’arithmétique un peu aménagée.

E ⊢ n↪n

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

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

La conditionnelle pareillement aménagée.

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

E ⊢ Ifz t₁ Then t₂ Else t₃↪v

E ⊢ t₁↪n (n ≠ 0) E ⊢ t₃↪v

E ⊢ Ifz t₁ Then t₂ Else t₃↪v

Et le point fixe pareillement aménagé.

E ⊕ [x = <Fix x -> t•E>] ⊢ t↪v

E ⊢ Fix x -> t↪v

Fermeture

Nous avions la règle d’évaluation des fonctions

Fun x -> t↪Fun x -> t

Quelle peut-être la règle d’interprétation ?

E ⊢ Fun x -> t↪<x•t•E>

On a très envie de dire <Fun x -> t•E>, mais cela compliquerait exagérément le concept de valeur. On définit plutôt la fermeture <x•t•E> comme ce glaçon là.

Nouvelle règle de l’application.

E ⊢ t₁↪<x•t′₁•E′> E′ ⊕ [x = <t₂•E>] ⊢ t′₁↪v

E ⊢ t₁ t₂↪v

NB : Les valeurs ne sont plus des termes.

Impact de la fermeture

Quelle est la valeur du terme

Let x = 4 In
Let f = Fun y -> y + x In
Let x = 5 In
f x

Le point crucial est de savoir à quoi se rapporte x dans y + x.

À la définition de x active au moment de la définition de f (et non pas de son application).

Et donc le résultat est 9 (et non pas 10).

La fermeture est ici cruciale, f est liée au glaçon

<Fun y -> y + x•[x=<4•[ ]>]>

Dont la valeur est la fermeture : <y•y + x•[x=<4•[ ]>]>.

Et y + x s’évalue dans [x=<4•[ ]>, y = <x•[…,x = <5•⋯>]>].

[x = …, f = …, x = <5•[…]>] ⊢ f 5↪10

[x=…, f= <Fun y -> y + x•[x=<4•[ ]>]>] ⊢ Let x = 5 In ⋯↪10

[x = <4•[ ]>] ⊢ Let f = Fun y -> y + x In ⋯↪10

⊢ Let x = 4 In ⋯↪10

Toutes les règles

Les valeurs v sont des entiers n ou des fermetures <x•t•E>.

Les environnements E lient les variables x à des glaçons <t•E>.

E ⊢ Fun x -> t↪_n<x•t•E>

E ⊢ t₁↪_n<x•t′₁•E′> E′ ⊕ [x = <t₂•E>] ⊢ t′₁↪_nv

E ⊢ t₁ t₂↪_nv

E ⊕ [x = <Fix x -> t•E>] ⊢ t↪_nv

E ⊢ Fix x -> t↪_nv

E(x) = <t•E′> E′ ⊢ t↪_nv

E ⊢ x↪_nv

E ⊕ [x = <t₁•E>] ⊢ t₂↪_nv

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

E ⊢ n↪_nn

E ⊢ t₁↪_nn₁ E ⊢ t₂↪_nn₂

E ⊢ t₁ op t₂↪_nn₁ opn₂

E ⊢ t₁↪_n0 E ⊢ t₂↪_nv

E ⊢ Ifz t₁ Then t₂ Else t₃↪_nv

E ⊢ t₁↪_nn (n ≠ 0) E ⊢ t₃↪_nv

E ⊢ Ifz t₁ Then t₂ Else t₃↪_nv

Interpréter par valeur

Notable simplification

Les règles de l’évaluation par valeur.

t₁↪_vFun x -> t₃ t₂↪_vv₂ [v₂\x]t₃↪_vv

t₁ t₂↪_vv

t₁↪_vv₁ [v₁\x]t₂↪_vv

Let x = t₁ In t₂↪_vv

Les substitutions retardées sont de la forme [v\x]⋯

Comme v est n (entier) ou <x•t•E> (fermeture), plus besoin de glaçon.

Malheureusement, il y a la récursion.

[(Fix x -> t)\x]t↪_vv

Fix x -> t↪_vv

Interprétation par valeur, simplicité ?

Récursion avec environnement (et glaçon) :

E ⊕ [x = <Fix x -> t•E>] ⊢ t↪_vv

E ⊢ Fix x -> t↪_vv

Donc : les environnements lient des variables à des valeurs v, ou à des glaçons de la forme <Fix x -> t•E> (exclusivement).

Deux règles pour les variables au lieu d’une.

E(x) = v

E ⊢ x↪_vv

E(x) = <Fix x -> t•E′> E′ ⊢ Fix x -> t↪_vv

E ⊢ x↪_vv

Et changer les règles de l’application et du Let.

E ⊢ t₁↪_v<x•t′•E′> E ⊢ t₂↪_vv₂ E′ ⊕ [x = v₂] ⊢ t′↪_vv

E ⊢ t₁ t₂↪_vv

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

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

Et c’est tout, mais il est dommage d’avoir des glaçons, juste pour coder la récursion.

Toutes les règles

Les valeurs v sont des entiers n ou des fermetures <x•t•E>. Les environnements E lient les variables x à des valeurs v ou à des glaçons de la forme <Fix x -> t•E>.

E(x) = v

E ⊢ x↪_vv

E(x) = <Fix x -> t•E′> E′ ⊢ Fix x -> t↪_vv

E ⊢ x↪_vv

E ⊢ t₁↪_v<x•t′•E′> E ⊢ t₂↪_vv₂ E′ ⊕ [x = v₂] ⊢ t′↪_vv

E ⊢ t₁ t₂↪_vv

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

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

E ⊕ [x = <Fix x -> t•E>] ⊢ t↪_vv

E ⊢ Fix x -> t↪_vv

E ⊢ n↪_vn

E ⊢ t₁↪_vn₁ E ⊢ t₂↪_vn₂

E ⊢ t₁ op t₂↪_vn₁ opn₂

E ⊢ t₁↪_v0 E ⊢ t₂↪_vv

E ⊢ Ifz t₁ Then t₂ Else t₃↪_vv

E ⊢ t₁↪_vn (n ≠ 0) E ⊢ t₃↪_vv

E ⊢ Ifz t₁ Then t₂ Else t₃↪_vv

Une remarque

En appel par valeur, Fix sert surtout à définir des fonctions.

Let fact =
Fix f Fun x -> Ifz x Then 1 Else x * f (x - 1) In
…

Interprétation de Fix f -> Fun x -> t, noté FixFun f x -> t

E ⊕ [f = <FixFun f x -> t•E>] ⊢ Fun x -> t↪<x•t•E′>

E ⊢ Fix f -> Fun x -> t↪<x•t•E′>

Avec

E′ = E ⊕ [f = <FixFun f x -> t•E>]

Première variante

Si Fix f -> ⋯ est nécessairement de la forme FixFun f x -> t, on peut remplacer les glaçons par une forme particulière de fermeture.

La nouvelle fermeture <f•x•t•E>, qui représente la fermeture à trois composants de la forme

<x•t•[f = <FixFun f x -> t•E>]>

On pose alors directement.

E ⊢ FixFun f x -> t↪_v<f•x•t•E>

On a alors une règle supplémentaire pour appliquer les nouvelles fermetures…

E ⊢ t₁↪_v<f•x•t•E′> E ⊢ t₂↪_vv₂ E′ ⊕ [f = <f•x•t•E′>, x=v₂] ⊢ t↪_vv

E ⊢ t₁ t₂↪_vv

Astuce

Si on représente une fermeture à trois composantes <x•t•E> comme une fermeture à quatre composantes <_f•x•t•E>, alors la nouvelle règle d’application des fermetures remplace l’ancienne !

On pose donc :

_f ∉F(t)

E ⊢ Fun x -> t↪_v<_f•x•t•E>

Et on supprime l’ancienne règle d’application.

E ⊢ t₁↪_v<x•t′•E′> E ⊢ t₂↪_vv₂ E′ ⊕ [x = v₂] ⊢ t′↪_vv

E ⊢ t₁ t₂↪_vv

Mais c’est bien artificiel (liaison de _f inutile).

Encore plus malin

Revenons à l’interprétation de t = FixFun f x -> b (page 33)

E ⊕ [f = g] ⊢ Fun x -> b↪_v<x•b•E ⊕ [f = g]>

E ⊢ FixFun f x -> b↪_v<x•b•E ⊕ [f = g]>

Où g note le glaçon <FixFun f x -> b•E>.

Anticipons maintenant l’interprétation de g. Une fois

<x•b•E ⊕ [f = g]>

Et encore une fois

<x•b•E ⊕ [f = <x•b•E ⊕ [f = g]>]>

Etc. on obtient une fermeture ordinaire, mais bouclée, avec :

C = <x•b•E ⊕ [f = C]>

Un graphe

Encore plus fort

Soit un interpréteur (qui est au final un programme)

Reste à construire le graphe, pour interpréter FixFun f x -> b dans l’env. E, par ex. en Caml.

type value = (* Les valeurs *)
| Integer of int | Closure of Var.t * Ast.t * env
and env = (Var.t * value) list (* les environnements *)

let rec inter E t = match t with
…
| Fix (f,Fun (x,b)) ->
let rec clo = Closure (x, b, (f,clo)::E) in
clo

Avantage définitif : une seule sorte de fermeture.

Planche : 37

TP, divers interpréteurs.
La prochaine fois, compilation.

Ce document a été traduit de L^AT_EX par H^EV^EA

Planche : 1

Planche : 2

Planche : 3

Point fixe et réduction

Planche : 4

Point fixe construit

Planche : 5

Construction explicite

Planche : 6

Démonstration de curry Φ ←→* Φ (curry Φ)

Planche : 7

Astuce ultime

Planche : 8

Plus clair sur un exemple

Planche : 9

Fabriquer un tel graphe

Planche : 10

Environnements

Planche : 11

Appel par nom

Planche : 12

Appel par valeur

Planche : 13

Substitution (dans un évaluateur)

Planche : 14

Substitution

Planche : 15

Une alternative

Planche : 16

Priorité (à droite)

Planche : 17

Priorité avec les environnements

Planche : 18

Formalisation de la liaison lexicale

Planche : 19

Implémentation de la liason lexicale

Planche : 20

Exemples

Planche : 21

Le glaçon (thunk)

Planche : 22

Reprenons

Planche : 23

Les règles de l’interprétation

Planche : 24

Fermeture

Planche : 25

Impact de la fermeture

Planche : 26

Toutes les règles

Planche : 27

Interpréter par valeur

Planche : 28

Notable simplification

Planche : 29

Interprétation par valeur, simplicité ?

Planche : 30

Toutes les règles

Planche : 31

Une remarque

Planche : 32

Première variante

Planche : 33

Astuce

Planche : 34

Encore plus malin

Planche : 35

Un graphe

Planche : 36

Encore plus fort

Planche : 37

Démonstration de `curry` Φ ←→^* Φ (`curry` Φ)

**Le glaçon (thunk)**