Planche : 1


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.

Planche : 3


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.


Planche : 4


Point fixe construit

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

x = (Fun y -> t′) x, avec t′ = [y\x]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.


Planche : 5


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).


Planche : 6


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 Φ)

Planche : 7


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 :


Planche : 8


Plus clair sur un exemple


Planche : 9


Fabriquer un tel graphe


Planche : 10


Environnements


Planche : 11


Appel par nom

t1nFun x -> t3           [t2\x]t3nv
t1 t2nv
Fun x -> tnFun x -> t
[t1\x]t2nv
Let x = t1 In t2nv
[(Fix x -> t)\x]tnv
Fix x -> tnv
t1n0           t2nv
Ifz t1 Then t2 Else t3nv
t1nn (n ≠ 0)           t3nv
Ifz t1 Then t2 Else t3nv
t1nn1         t2nn2
t1 op t2nn1 op n2
nnn

Planche : 12


Appel par valeur

t1vFun x -> t3           t2vv2           [v2\x]t3vv
t1 t2vv
Fun x -> tvFun x -> t
t1vv1           [v1\x]t2vv
Let x = t1 In t2vv
[(Fix x -> t)\x]tvv
Fix x -> tvv
t1v0           t2vv
Ifz t1 Then t2 Else t3vv
t1vn (n ≠ 0)           t3vv
Ifz t1 Then t2 Else t3vv
t1vn1         t2vn2
t1 op t2vn1 op n2
nvn

Planche : 13


Substitution (dans un évaluateur)

Pour évaluer (Fun x -> t1) t2,on calcule [t2\x]t1 (ou [v2\x]t1)

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

[t2\x](Fun x -> t1) = Fun x -> t1
[t2\x](Fun y -> t1) = Fun y -> [t2\x]t1

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

Toutefois,

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


Planche : 14


Substitution

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

(Fun x -> t)↪n(Fun x -> t)
         
4n4         4n4
4 * 4n16
          4n4
(4 * 4) + 4n20
(Fun x -> t4n20

Planche : 15


Une alternative


Planche : 16


Priorité (à droite)

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

En toute rigueur

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

Planche : 17


Priorité avec les environnements

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

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

Planche : 18


Formalisation de la liaison lexicale

On pourrait écrire :

[…, x=n] ⊢ xn
[…] ⊢ xn
[…, y=ny] ⊢ xn
[…, x=n] ⊢ tv
[…] ⊢ Let x = n In tv

On préfère une notation plus abstraite.

E(x) = n
E ⊢ xn
E ⊕ [x = n] ⊢ tv
E ⊢ Let x = n In tv

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)

Planche : 19


Implémentation de la liason lexicale

Avec de bêtes listes d’associations :

type 'a env = (Var.t * 'alist

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,t1)::(x,t2)::…) → t1

Mais c’est pareil.


Planche : 20


Exemples

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

Recommençons.


Planche : 21


Le glaçon (thunk)

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

Donc on considère

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

C’est-à-dire

Let y = [5\x](4 + xIn [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 <tE>.


Planche : 22


Reprenons

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


Planche : 23


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) = <tE′>         E′ ⊢ tv
E ⊢ xv
E ⊕ [x = <t1E>] ⊢ t2v
E ⊢ Let x = t1 In t2v

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

E ⊢ nn
E ⊢ t1n1         E ⊢ t2n2
E ⊢ t1 op t2n1 opn2

La conditionnelle pareillement aménagée.

E ⊢ t1↪0           E ⊢ t2v
E ⊢ Ifz t1 Then t2 Else t3v
E ⊢ t1n (n ≠ 0)           E ⊢ t3v
E ⊢ Ifz t1 Then t2 Else t3v

Et le point fixe pareillement aménagé.

E ⊕ [x = <Fix x -> tE>] ⊢ tv
E ⊢ Fix x -> tv

Planche : 24


Fermeture

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

Fun x -> tFun x -> t

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

E ⊢ Fun x -> t↪<xtE>

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

Nouvelle règle de l’application.

E ⊢ t1↪<xt1E′>           E′ ⊕ [x = <t2E>] ⊢ t1v
E ⊢ t1 t2v

NB : Les valeurs ne sont plus des termes.


Planche : 25


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 : <yy + x•[x=<4•[ ]>]>.

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

[x = …, f = …, x = <5•[…]>] ⊢ f 510
[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

Planche : 26


Toutes les règles

Les valeurs v sont des entiers n ou des fermetures <xtE>.

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

E ⊢ Fun x -> tn<xtE>
E ⊢ t1n<xt1E′>           E′ ⊕ [x = <t2E>] ⊢ t1nv
E ⊢ t1 t2nv
E ⊕ [x = <Fix x -> tE>] ⊢ tnv
E ⊢ Fix x -> tnv
E(x) = <tE′>         E′ ⊢ tnv
E ⊢ xnv
E ⊕ [x = <t1E>] ⊢ t2nv
E ⊢ Let x = t1 In t2nv
E ⊢ nnn
E ⊢ t1nn1         E ⊢ t2nn2
E ⊢ t1 op t2nn1 opn2
E ⊢ t1n0           E ⊢ t2nv
E ⊢ Ifz t1 Then t2 Else t3nv
E ⊢ t1nn (n ≠ 0)           E ⊢ t3nv
E ⊢ Ifz t1 Then t2 Else t3nv

Planche : 27


Interpréter par valeur


Planche : 28


Notable simplification

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

t1vFun x -> t3           t2vv2           [v2\x]t3vv
t1 t2vv
t1vv1           [v1\x]t2vv
Let x = t1 In t2vv

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

Comme v est n (entier) ou <xtE> (fermeture), plus besoin de glaçon.

Malheureusement, il y a la récursion.

[(Fix x -> t)\x]tvv
Fix x -> tvv

Planche : 29


Interprétation par valeur, simplicité ?

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

E ⊕ [x = <Fix x -> tE>] ⊢ tvv
E ⊢ Fix x -> tvv

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

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

E(x) = v
E ⊢ xvv
E(x) = <Fix x -> tE′>           E′ ⊢ Fix x -> tvv
E ⊢ xvv

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

E ⊢ t1v<xt′•E′>           E ⊢ t2vv2           E′ ⊕ [x = v2] ⊢ t′↪vv
E ⊢ t1 t2vv
E ⊢ t1vv1           E ⊕ [x = v1] ⊢ t2vv
E ⊢ Let x = t1 In t2vv

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


Planche : 30


Toutes les règles

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

E(x) = v
E ⊢ xvv
E(x) = <Fix x -> tE′>           E′ ⊢ Fix x -> tvv
E ⊢ xvv
E ⊢ t1v<xt′•E′>           E ⊢ t2vv2           E′ ⊕ [x = v2] ⊢ t′↪vv
E ⊢ t1 t2vv
E ⊢ t1vv1           E ⊕ [x = v1] ⊢ t2vv
E ⊢ Let x = t1 In t2vv
E ⊕ [x = <Fix x -> tE>] ⊢ tvv
E ⊢ Fix x -> tvv
E ⊢ nvn
E ⊢ t1vn1         E ⊢ t2vn2
E ⊢ t1 op t2vn1 opn2
E ⊢ t1v0           E ⊢ t2vv
E ⊢ Ifz t1 Then t2 Else t3vv
E ⊢ t1vn (n ≠ 0)           E ⊢ t3vv
E ⊢ Ifz t1 Then t2 Else t3vv

Planche : 31


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 -> tE>] ⊢ Fun x -> t↪<xtE′>
E ⊢ Fix f -> Fun x -> t↪<xtE′>

Avec

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

Planche : 32


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 <fxtE>, qui représente la fermeture à trois composants de la forme

<xt•[f = <FixFun f x -> tE>]>

On pose alors directement.

E ⊢ FixFun f x -> tv<fxtE>

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

E ⊢ t1v<fxtE′>           E ⊢ t2vv2           E′ ⊕ [f = <fxtE′>, x=v2] ⊢ tvv
E ⊢ t1 t2vv

Planche : 33


Astuce

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

On pose donc :

_f ∉F(t)
E ⊢ Fun x -> tv<_fxtE>

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

E ⊢ t1v<xt′•E′>           E ⊢ t2vv2           E′ ⊕ [x = v2] ⊢ t′↪vv
E ⊢ t1 t2vv

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


Planche : 34


Encore plus malin

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

 
E ⊕ [f = g] ⊢ Fun x -> bv<xbE ⊕ [f = g]>
E ⊢ FixFun f x -> bv<xbE ⊕ [f = g]>

g note le glaçon <FixFun f x -> bE>.

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

<xbE ⊕ [f = g]>

Et encore une fois

<xbE ⊕ [f = <xbE ⊕ [f = g]>]>

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

C = <xbE ⊕ [f = C]>

Planche : 35


Un graphe


Planche : 36


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 * valuelist (* les environnements *)

let rec inter E t = match t with

Fix (f,Fun (x,b)) ->
    let rec clo = Closure (xb, (f,clo)::Ein
    clo

Avantage définitif : une seule sorte de fermeture.


Planche : 37



Ce document a été traduit de LATEX par HEVEA