5 Style de passage de continuations
Les modèles sémantiques dénotationnels que l'on a vus
jusqu'ici — dits en style direct — ont l'avantage
d'oublier tous les détails liés à l'ordre d'évaluation,
excepté les points importants comme la terminaison (valoir ⊥
ou pas). C'est parfois aussi un inconvénient, et on aimerait
parfois pouvoir exprimer une partie de la stratégie
d'évaluation. Par exemple, dans la sémantique proposée en
figure 4, rien ne dit que pour évaluer uv, on
doive évaluer u avant v.
C'est gênant notamment si l'on enrichit notre λ-calcul
avec des constructions telles que les affectations
(setq en Lisp, := ou <- en Caml, := en
Pascal, = en C), ou les sauts non locaux (try
et raise en Caml, goto en Pascal, setjmp et
longjmp en C). Prenons le cas des affectations tout d'abord,
parce qu'il est plus simple à expliquer. Supposons qu'on veuille
calculer la valeur de uv, et que l'évaluation de u affecte une
référence x à 1, et l'évaluation de v affecte x à
2. Si u est évalué avant v, alors x vaudra 2 à la
fin du calcul, et si c'est v, alors x vaudra 1 à la fin du
calcul: la sémantique des deux cas n'est donc pas la même.
5.1 Le concept de continuation
Une façon de spécifier l'ordre d'évaluation en sémantique
dénotationnelle est de faire prendre à la fonction
d'évaluation un deuxième argument, la continuation
κ, qui est une fonction de D vers D, et de convenir que:
[u] ρ κ
est la valeur non pas de u mais d'un programme tout entier dont un
sous-terme est u: κ dénote la suite du calcul une fois
qu'on aura évalué u, et si la valeur de u est d, alors la
valeur du programme tout entier sera κ (d). Graphiquement,
on peut imaginer que l'on a un programme π, dont l'exécution
va consister en une suite d'instructions, et qu'au milieu de cette
suite on trouve une sous-suite d'instructions pour évaluer u:
Lorsque l'exécution se trouve au début de u (au point 1), ce
graphique dit que ce qu'il reste à faire pour trouver la valeur de
π au point 3, c'est calculer la valeur de u, et une fois qu'on
l'aura (au point 2), il suffira d'appliquer κ, la suite du
calcul.
Formellement, examinons déjà comme on peut modéliser une
stratégie (faible) d'appel par valeur gauche sur les
λ-termes purs par ce moyen (le codage des booléens, des
entiers, etc., est laissé en exercice), et nous verrons ensuite
comment ce style de sémantique permet de modéliser les
constructions de style setjmp/longjmp, puis les
affectations.
Tout d'abord, [x] ρ κ, lorsque x est une variable,
doit évaluer x, et passer sa valeur ρ (x) à κ. On
va donc définir [x] ρ κ =def κ (ρ (x)).
Dans le cas des applications, [uv] ρ κ doit d'abord
évaluer u, puisque nous avons décidé d'une stratégie
gauche. [uv] ρ κ vaudra donc [u] ρ κ'
pour une continuation κ' à trouver. Cette continuation
κ' est une fonction qui prend la valeur f de u, et va
ensuite calculer v. Donc κ' doit être de la forme (f
↦ [v] ρ' κ'') pour un environnement ρ' et
une continuation κ'' à trouver. Mais v s'évalue dans
le même environnement que uv, donc ρ'=ρ. D'autre part,
κ'' doit être une fonction qui prend la valeur d de v,
applique la valeur f de u (que l'on supposera être une
fonction) à d, et continue le reste du calcul (κ) avec la
valeur f (d). En résumé:
[uv] ρ κ =def [u] ρ (f ↦ [v] ρ (d ↦ κ (f (d))))
Cette formule peut avoir l'air illisible, mais voici un truc pour
déchiffrer ce genre de notations intuitivement: [u] ρ (f
↦ … se lit “évaluer u dans l'environnement ρ,
ceci donne une valeur f; ensuite ...”. D'autre part, appliquer
κ à une valeur d se lit: “retourner d”. La formule ci-dessus
se lit donc:
| Évaluer u dans l'environnement ρ, ceci donne une valeur f; ensuite, |
| évaluer v dans l'environnement ρ, ceci donne une valeur d; ensuite, |
| retourner f (d). |
Pour évaluer une λ-abstraction λ x ⋅ u dans
l'environnement ρ et la continuation κ, on va d'abord
calculer la valeur de λ x ⋅ u, et ensuite la retourner
par κ. Cette valeur est une fonction qui prend une valeur
d pour x, et ensuite évalue u ...mais avec quelle
continuation ? L'idée, c'est qu'une fois que le calcul de u
sera terminé, la continuation devra juste retourner cette valeur:
la continuation cherchée est l'identité id. En somme:
[λ x⋅ u] ρ κ =def κ (d ↦ [u] (ρ[x:=d]) id)
Cette sémantique, qui est notre premier exemple d'une sémantique
par passage de continuations, est résumée en
figure 5. Nous avons affiné la définition dans
le cas de l'application uv, pour tenir compte de ce qui se passe
lorsque f n'est pas une fonction dans le domaine sémantique D
considéré. Noter qu'on ne retourne pas ⊥ (on n'a pas
écrit κ (⊥)), mais on interrompt l'exécution
complète du programme, qui retourne immédiatement ⊥.
(C'est un plantage.)
| [x] ρ κ |
=def |
κ (ρ (x)) |
| [uv] ρ κ |
=def |
| [u] ρ |
⎛
⎜
⎝ |
f ↦ [v] ρ |
⎛
⎜
⎝ |
d ↦
|
⎧
⎨
⎩ |
| κ (f (d)) |
si f est une fonction |
| ⊥ |
sinon |
|
|
⎞
⎟
⎠ |
⎞
⎟
⎠ |
|
| [λ x⋅ u] ρ κ |
=def |
κ (d ↦ [u] (ρ[x:=d]) id) |
Figure 5: Une sémantique de l'appel par valeur en style de passage de continuations
On notera que l'on aurait pu définir l'application autrement, par exemple:
|
[u] ρ |
⎛
⎜
⎝ |
f ↦
|
⎧
⎨
⎩ |
| [v] ρ (d ↦ κ (f (d))) |
si f est une fonction |
| ⊥ |
sinon |
|
|
⎞
⎟
⎠ |
5.2 Sauts non locaux et captures de continuations
Voyons maintenant comment on peut coder un mécanisme à la
setjmp/longjmp de C. Rappelons que setjmp
capture une copie du contexte d'évaluation courant (le compteur de
programme, le pointeur de pile, les registres) et la met dans une
structure k, que nous représenterons par une variable du
λ-calcul, puis retourne 0; longjmp appliqué à
k et à une valeur d réinstalle k comme contexte
d'évaluation courant, ce qui à pour effet de faire un saut non
local à l'endroit du programme où se trouve le setjmp qui
à défini k, et de faire retourner la valeur d par ce
dernier. Ceci permet de gérer des conditions d'erreur, par ex:
x = setjmp (k);
if (x==0) /* retour normal */
{
/* faire un certain nombre de calculs, eventuellement imbriques,
qui arrivent a la ligne suivante : */
if (erreur)
longjmp (k, errno); /* longjmp ne retourne pas,
et saute a l'endroit du setjmp ci-dessus */
/* si pas d'erreur, continuer... */
}
else
{ /* ici, on est revenu sur erreur, avec x==errno */
printf ("Erreur no. %d.\n", x);
}
Comme beaucoup de constructions en C, celle-ci manque de
l'élégance des constructions similaires de langages
fonctionnels, et la plus proche est une construction, appelée
call-with-current-continuation ou call/cc, et qui a
été introduite dans le langage Scheme, un dialecte Lisp. (Le
manque d'élégance de la construction C est due à deux choses.
D'une part, si errno vaut 0, on ne peut pas distinguer un
retour normal de setjmp d'un retour sur erreur dans l'exemple
ci-dessus. D'autre part, longjmp a une sémantique
indéfinie s'il est appelé après que la fonction dans laquelle
setjmp a été appelé a retourné.)
L'idée est simple: le concept concret de contexte d'évaluation
courant n'est rien d'autre que la continuation κ ! On peut
donc définir en première approche une construction callcc
k in u qui capture à la façon de setjmp le
contexte (la continuation) courante, la met dans k et évalue
u; et une construction throw k v qui évalue k et
v, et réinstalle la continuation k pour faire retourner la
valeur de v par l'instruction callcc qui a défini k.
Sémantiquement:
| [callcc k in u] ρ κ |
=def |
[u] (ρ [k:=κ]) κ |
| [throw k v] ρ κ |
=def |
[k] ρ (κ' ↦
[v] ρ κ') |
Remarquer que dans la définition de throw, la continuation
κ n'intervient pas dans le côté droit de l'égalité:
elle est tout simplement ignorée, car c'est la continuation
κ', valeur de k, qui va être utilisée pour continuer le
calcul. Le fait que κ n'intervienne pas signifie que
throw k v ne retourne jamais.
On peut tester sur quelques exemples que le comportement est bien le
comportement attendu:
Exercice 32
Montrer que callcc k in 3 retourne 3; autrement dit, en
supposant que l'on a une constante 3 telle que [3] ρ κ = κ (3), montrer que [callcc k in 3] ρ κ = κ (3).
Exercice 33
Selon cette sémantique, que valent callcc k in throw k 3, callcc k in (throw k 3) 2, callcc k in 1+callcc k' in throw k' (throw k 3) ? (On
supposera que 1 et l'addition ont leurs sémantiques
naturelles, que l'on précisera.)
Mais en fait, non, le comportement des continuations n'est pas le
comportement attendu en général. Considérons le programme
callcc k in (λ x ⋅ throw
k (λ y ⋅ y)) 3. On s'attend à ce qu'il ait
la même sémantique que le β-réduit callcc k
in throw k (λ y ⋅ y), autrement dit
qu'il retourne la fonction identité, mais ce n'est pas le cas. En
effet, formellement:
|
|
| |
[callcc k in (λ x ⋅ throw
k (λ y ⋅ y)) 3]
ρ κ |
| = |
[(λ x ⋅ throw k (λ y ⋅ y)) 3]
(ρ[k:=κ]) κ |
| = |
[λ x ⋅ throw k (λ y ⋅ y)] (ρ[k:=κ])
(f ↦ [3] (ρ[k:=κ])
(d ↦ κ (f (d))) |
| = |
[λ x ⋅ throw k (λ y ⋅ y)] (ρ[k:=κ])
(f ↦ κ (f (3))) |
| = |
(f ↦ κ (f (3)))
(d ↦ [throw k (λ y ⋅ y)]
(ρ[k:=κ, x:=d]) id) |
| = |
κ ([throw k (λ y ⋅ y)]
(ρ[k:=κ, x:=3]) id) |
| = |
κ ([k] (ρ[k:=κ, x:=3]) (κ' ↦
[λ y ⋅ y] (ρ[k:=κ, x:=3]) κ')) |
| = |
κ ((κ' ↦
[λ y ⋅ y] (ρ[k:=κ, x:=3]) κ') κ) |
| = |
κ ([λ y ⋅ y] (ρ[k:=κ, x:=3]) κ) |
| = |
κ (κ (d ↦ [y] (ρ[k:=κ, x:=3, y:=d]) id)) |
| = |
κ (κ (d ↦ d)) |
|
|
|
| |
[callcc k in throw k (λ y ⋅ y)]
ρ κ |
| = |
[throw k (λ y ⋅ y)] (ρ[k:=κ]) κ |
| = |
[k] (ρ[k:=κ]) (κ' ↦
[λ y ⋅ y] (ρ[k:=κ]) κ') |
| = |
(κ' ↦ [λ y ⋅ y] (ρ[k:=κ]) κ')
κ |
| = |
[λ y ⋅ y] (ρ[k:=κ]) κ |
| = |
κ (d ↦ [y] (ρ[k:=κ, y:=d]) id) |
| = |
κ (d ↦ d) |
|
Le problème est dans la façon dont nous avons défini la
sémantique de l'abstraction en figure 5, bien que
cela ne soit pas facile à voir sur l'exemple. Raisonnons donc par
analogie, en identifiant continuation et pile courante (plus
compteur de programme). La sémantique de la
figure 5 demande à évaluer λ x⋅ u
dans la pile κ en retournant une fonction qui doit exécuter
u dans la pile id, mais c'est absurde: si jamais la fonction
doit être appelée un jour dans le contexte d'une autre pile
κ', alors u doit être évalué dans la pile κ'.
Il est donc nécessaire de modifier la définition de sorte
qu'elle prenne en paramètre la pile κ' de l'appelant en
plus de la valeur d de l'argument x:
[λ x ⋅ u] ρ κ =def
κ (κ', d ↦ [u] (ρ[x:=d]) κ')
et la sémantique de l'application uv doit tenir compte de ce
changement: la valeur f de u est maintenant une fonction qui
prend non seulement la valeur d de v en argument, mais aussi la
pile courante κ; f (κ, d) calcule alors la valeur u
avec x valant d dans la continuation κ. En particulier,
comme κ est passée à f, c'est f (κ, d) qui sera
chargée de calculer tout le reste du programme, et on n'a donc pas
besoin de calculer κ (f (κ, d)). On pose alors:
[uv] ρ κ =def [u] ρ (f ↦ [v] ρ (d ↦ f (κ, d)))
En résumé, on a obtenu la sémantique de la
figure 6.
| [x] ρ κ |
=def |
κ (ρ (x)) |
| [uv] ρ κ |
=def |
| [u] ρ |
⎛
⎜
⎝ |
f ↦
[v] ρ |
⎛
⎜
⎝ |
d ↦
|
⎧
⎨
⎩ |
| f (κ, d) |
si f est une fonction binaire |
| ⊥ |
sinon |
|
|
⎞
⎟
⎠ |
⎞
⎟
⎠ |
|
| [λ x ⋅ u] ρ κ |
=def |
κ ((κ', d) ↦ [u] (ρ[x:=d]) κ') |
| [callcc k in u] ρ κ |
=def |
[u] (ρ [k:=κ]) κ |
| [throw k v] ρ κ |
=def |
[k] ρ (κ' ↦
[v] ρ κ') |
Figure 6: Une sémantique en passage par valeur avec des sauts non locaux
Exercice 34
On pose let x=u in v =def (λ x⋅ v)
u. Calculer [let x=u in v] ρ
κ.
Exercice 35
On appelle valeur au sens de Plotkin
, ou P-valeur
, les
λ-termes qui sont soit des variables soit des
abstractions. Montrer que si V est une P-valeur, [(λ x ⋅ u) V] ρ κ = [u [x:=V]] ρ
κ. (On dit que la règle (βv): (λ x ⋅
u) V → u [x:=V] est valide.) Montrer que ce résultat ne se
généralise pas au cas où V n'est pas une P-valeur.
En Scheme, les constructions callcc...in et
throw ne sont pas présentes telles quelles. Comme k est
une variable liée dans callcc k in u, on
peut en effet s'arranger pour la lier via un λ, et définir
callcc k in u = call/cc (λ
x⋅ u), où call/cc est un opérateur primitif du
langage. La sémantique (provisoire) de call/cc est:
[call/cc] ρ κ =def
κ ((κ', f) ↦ f (κ', κ'))
En fait, il est traditionnel lorsqu'on étudie les opérateurs de
capture de continuation de faire de la valeur de la variable k de
continuation directement une valeur de fonction. En effet, la seule
utilisation possible d'une continuation stockée dans k est
d'appeler throw k v. Posons k' =def throw k
=def λ x ⋅ throw k x: la valeur de k' est la
seule chose que call/cc a besoin de stocker. On
définit donc (définitivement):
[call/cc] ρ κ =def
κ ((κ', f) ↦ f (κ', (_, d') ↦ κ' (d')))
où (_, d') ↦ κ' (d') est la fonction qui prend une
continuation κ'', une valeur d' et retourne κ' (d')
après avoir jeté κ''.
Exercice 36
Montrer que, si k est une variable telle que ρ (k) = f,
alors [λ x ⋅ throw k x] ρ κ =
κ ((_, d) ↦ f (d)).
Exercice 37
Vérifier que, si k n'est pas libre dans u, alors [call/cc (λ k' ⋅ u)] ρ κ = [callcc k in u [k':=λ x ⋅
throw k x]] ρ κ. (Pour faciliter le calcul,
on remarquera que λ x ⋅ throw k x est une
P-valeur, donc par l'exercice 35, il suffit de montrer
que [call/cc (λ k' ⋅ u)] ρ κ =
[callcc k in (λ k' ⋅ u)
(λ x ⋅ throw k x)] ρ κ.)
Exercice 38
L'opérateur call/cc connaît de nombreuses
variantes, notamment l'opérateur C de Felleisen, dont la
sémantique est:
[ C] ρ κ =def κ ((κ', f) ↦ f (_ ↦ ⊥,
(_, d') ↦ κ' (d')))
où _ ↦ ⊥ est la fonction qui retourne toujours
⊥. Montrer que, pour tout t:
[ C t] ρ κ = [t] ρ (f ↦ f (_ ↦ ⊥,
(_, d') ↦ κ (d')))
Exercice 39
On dit que u retourne normalement
dans l'environnement
ρ si et seulement si, pour toute continuation κ,
[u] ρ κ = κ (d) pour une certaine valeur d,
appelée la valeur
de u.
Montrer que si u retourne normalement dans ρ[k:=(_, d') ↦
κ (d')], alors [ C (λ k ⋅ u)] ρ κ =
⊥. (Autrement dit, si u retourne normalement, alors C
(λ k ⋅ u) plante.)
Exercice 40
Montrer que l'on peut réaliser call/cc à l'aide de
C. Plus précisément, on montrera que call/cc
(λ k ⋅ u) et C (λ k ⋅ k u) ont la
même sémantique.
L'opérateur C est souvent plus pratique pour les
manipulations formelles que call/cc. Faisons quelques
calculs, dans l'espoir de découvrir quelques égalités
sémantiques entre termes. Notamment, que vaut C (λ
k ⋅ t) appliqué à v ? Intuitivement, on va récupérer
dans k la continuation consistant à appliquer la valeur f de
t à la valeur d de v, et ensuite appliquer la continuation
courante κ à f (d). Mais on peut récupérer la
continuation courante dans une variable k' en écrivant C
(λ k' ⋅ …), et alors le calcul consistant à
calculer t avec comme continuation la fonction qui prend la valeur
f de t, l'applique à v et continue le calcul (par k') est
donc t [k:=λ f ⋅ k' (f v)] — ceci du moins tant que
v est une P-valeur. Ceci suggère que C (λ k ⋅
t) v = C (λ k' ⋅ t [k:=λ f ⋅ k' (f v)],
au moins si v est une P-valeur. Plus généralement, posons u
=def λ k ⋅ t, et comparons les deux quantités C
u v et C (λ k' ⋅ u (λ f ⋅ k' (f v))):
|
|
| [ C u v] ρ κ = |
[ C u] ρ (g ↦ [v] ρ (d ↦ g (κ, d))) |
| = |
[u] ρ (f ↦ f (_ ↦ ⊥,
(_, d') ↦ (g ↦ [v] ρ (d ↦ g (κ, d))) (d'))) |
| |
par l'exercice 38 |
| = |
[u] ρ (f ↦ f (_ ↦ ⊥,
(_, d') ↦ [v] ρ (d ↦ d' (κ, d)))) |
|
|
|
| |
[ C (λ k' ⋅ u (λ f ⋅ k' (f v)))] ρ κ |
| = |
[λ k' ⋅ u (λ f ⋅ k' (f v))]
ρ (f ↦ f (_ ↦ ⊥, (_, d') ↦ κ (d'))) |
| = |
(f ↦ f (_ ↦ ⊥, (_, d') ↦ κ (d')))
((κ', d'') ↦ [u (λ f ⋅ k' (f v))] (ρ[k':=d'']) κ') |
| = |
[u (λ f ⋅ k' (f v))] (ρ[k':=(_, d') ↦ κ (d')])
(_ ↦ ⊥) |
| = |
[u] (ρ[k':=(_, d') ↦ κ (d')])
(g ↦ [λ f ⋅ k' (f v)] (ρ[k':=(_, d') ↦ κ (d')])
(d'' ↦ g (_ ↦ ⊥, d''))) |
| = |
[u] ρ
(g ↦ [λ f ⋅ k' (f v)] (ρ[k':=(_, d') ↦ κ (d')])
(d'' ↦ g (_ ↦ ⊥, d''))) |
| |
à condition que k' ne soit pas libre dans u |
| = |
[u] ρ
(g ↦
(d'' ↦ g (_ ↦ ⊥, d''))
((κ', g') ↦ [k' (f v)] (ρ[k':=(_, d') ↦ κ (d'), f:=g'])
κ')) |
| = |
[u] ρ
(g ↦
g (_ ↦ ⊥,
(κ', g') ↦ [k' (f v)] (ρ[k':=(_, d') ↦ κ (d'), f:=g'])
κ')) |
| = |
[u] ρ
(g ↦
g (_ ↦ ⊥,
(κ', g') ↦
[k'] (ρ[k':=(_, d') ↦ κ (d'), f:=g']) |
| |
(f' ↦ [fv] (ρ[k':=(_, d') ↦ κ (d'), f:=g'])
(d ↦ f' (κ', d))))) |
| = |
[u] ρ
(g ↦
g (_ ↦ ⊥,
(κ', g') ↦ |
| |
(f' ↦ [fv] (ρ[k':=(_, d') ↦ κ (d'), f:=g'])
(d ↦ f' (κ', d)))
((_, d') ↦ κ (d')))) |
| = |
[u] ρ
(g ↦
g (_ ↦ ⊥,
(κ', g') ↦
[fv] (ρ[k':=(_, d') ↦ κ (d'), f:=g'])
(d ↦ κ (d)))) |
| = |
[u] ρ
(g ↦
g (_ ↦ ⊥,
(κ', g') ↦
[f] (ρ[k':=(_, d') ↦ κ (d'), f:=g']) |
| |
(f' ↦ [v] (ρ[k':=(_, d') ↦ κ (d'), f:=g'])
(d'' ↦ f' (d ↦ κ (d), d''))))) |
| = |
[u] ρ
(g ↦
g (_ ↦ ⊥,
(κ', g') ↦
(f' ↦ [v] (ρ[k':=(_, d') ↦ κ (d'), f:=g'])
(d'' ↦ f' (d ↦ κ (d), d'')))
(g'))) |
| = |
[u] ρ
(g ↦
g (_ ↦ ⊥,
(κ', g') ↦
[v] (ρ[k':=(_, d') ↦ κ (d'), f:=g'])
(d'' ↦ g' (d ↦ κ (d), d'')))) |
| = |
[u] ρ
(g ↦
g (_ ↦ ⊥,
(κ', g') ↦
[v] ρ
(d'' ↦ g' (d ↦ κ (d), d'')))) |
| |
à condition que k' et f ne soient pas libres dans v |
| = |
[u] ρ
(g ↦
g (_ ↦ ⊥,
(κ', g') ↦
[v] ρ
(d'' ↦ g' (κ, d'')))) |
| |
car (d ↦ κ (d)) = κ |
|
On a donc démontré:
Lemme 7
[ C u v] ρ κ = [ C (λ k'
⋅ u (λ f ⋅ k' (f v)))] ρ κ, où k' et
f sont deux variables nouvelles.
Notons que ceci est correct même quand v n'est pas une P-valeur.
On peut directement formaliser le comportement de l'opérateur
C par des règles de réécriture inspirées de la
sémantique:
|
|
| ( CL) |
C u v |
→ |
C (λ k' ⋅ u (λ f ⋅ k' (f v))) |
| ( CR) |
V ( C u) |
→ |
C (λ k' ⋅ u (λ x ⋅ k' (V x))) |
|
où dans la seconde, V est une P-valeur.
Exercice 41
Montrer que la règle ( CR) est valide. (On utilisera
le fait que toute P-valeur V retourne normalement, cf.
exercice 39, et en fait que [V] ρ κ =
κ (d) pour une valeur d qui ne dépend que de V et de
ρ.) Montrer que l'hypothèse selon laquelle V est une
P-valeur est essentielle.
Nous avons ignoré les problèmes de définition de domaine de
valeurs. Mais ceci se règle aisément. Nous avons besoin d'un
domaine D, les continuations κ seront des éléments de
[D → D], et les valeurs des fonctions seront des éléments de
[[D → D] × D → D]. Il suffit donc de prendre un domaine
D tel que:
D = ( N ∪ [[D → D] × D → D] )⊥
à isomorphisme près, et où N peut être remplacé par
n'importe quel autre ensemble de valeurs de base. (Noter que les
continuations ne sont pas incluses dans le domaine des valeurs, car
les continuations capturées par C sont codées comme des
fonctions dans [[D → D] × D → D].)
5.3 Ajout d'effets de bord
(
)
Nous allons maintenant voir quelques conséquences intéressantes
de cette façon de voir la sémantique des langages en appel par
valeur.
La première est qu'il est maintenant facile de donner une
sémantique à un langage enrichi d'effets de bord, sous la forme
d'affectations. Voici, dans le style de ML, les constructions que
nous voulons ajouter: certains termes dénoteront des références, c'est-à-dire des adresses en mémoire pointant
vers des valeurs; la construction !u retourne la valeur stockée
à l'adresse u, la construction u:=v stocke la valeur de v
à l'adresse u, et enfin ref u alloue une adresse
l, y stocke la valeur de u, et retourne l. Tant qu'à imiter
les langages impératifs comme Pascal ou C, nous allons aussi
introduire une construction de séquencement u;v qui évalue
u, puis évalue et retourne la valeur de v.
Pour donner une sémantique formelle à ces constructions, on peut
modifier notre fonction [_] de sorte qu'elle prenne
maintenant non seulement un environnement ρ, une continuation
κ, mais aussi une mémoire σ ∈ [L⊥→
D], où L est un ensemble d'adresses (“locations” en
anglais).
Noter que les continuations doivent maintenant non seulement prendre
en argument la valeur calculée par un terme u, mais aussi le
nouvel état de la mémoire. En résumé, on aura les
conventions de typage:
| ρ |
∈ |
V → D |
| σ |
∈ |
[L⊥→ D] |
| κ |
∈ |
[[L⊥→ D] × D → A] |
où A est un domaine de réponses. Auparavant, A
était juste le domaine D des valeurs, mais il est aussi
envisageable de vouloir prendre pour A le produit du domaine D
des valeurs avec celui, [L⊥→ D], des mémoires, par
exemple, selon ce que l'on souhaite observer à la fin du calcul.
Les valeurs de fonctions devront maintenant prendre une
continuation, une valeur pour son argument, et une mémoire
courante, et retourner une réponse. Notre domaine sémantique
doit aussi être enrichi par des adresses, et c'est pourquoi nous
posons:
| D |
=def |
( N ⊕ L ⊕ [Cont × Mem × D → A] )⊥ |
| Cont |
=def |
[Mem × D → A] |
| Mem |
=def |
[L⊥→ D] |
où N pourrait être remplacé par n'importe quel autre
ensemble de valeurs de base. On peut alors définir notre
sémantique comme en figure 7. (Exercice:
vérifier que la définition est cohérente avec le typage
donné par les équations de domaine pour D, Cont et Mem.)
| [x] ρ σ κ |
=def |
κ (σ, ρ (x)) |
| [uv] ρ σ κ |
=def |
| [u] ρ σ
|
⎛
⎜
⎝ |
(σ', f) ↦
[v] ρ σ'
|
⎛
⎜
⎝ |
(σ'', d) ↦
|
⎧
⎨
⎩ |
| f (κ, σ'', d) |
si f est une fonction |
| ⊥ |
sinon |
|
|
⎞
⎟
⎠ |
⎞
⎟
⎠ |
|
| [λ x ⋅ u] ρ σ κ |
=def |
κ (σ, (κ', σ', d) ↦ [u] (ρ[x:=d]) σ' κ') |
| [!u] ρ σ κ |
=def |
| [u] ρ σ
|
⎛
⎜
⎝ |
(σ', l) ↦
|
⎧
⎨
⎩ |
| κ (σ', σ' (l)) |
si l est dans le domaine de σ' |
| ⊥ |
sinon |
|
|
⎞
⎟
⎠ |
|
| [u:=v] ρ σ κ |
=def |
| [u] ρ σ |
⎛
⎜
⎝ |
(σ', l) ↦
[v] ρ σ' |
⎛
⎜
⎝ |
(σ'', d) ↦
|
⎧
⎨
⎩ |
| κ (σ''[l:=d], d) |
si l∈ L |
| ⊥ |
sinon |
|
|
⎞
⎟
⎠ |
⎞
⎟
⎠ |
|
| [ref u] ρ σ κ |
=def |
[u] ρ σ ((σ', d) ↦ κ (σ'[l:=d], l))
(l hors du domaine de σ') |
| [u;v] ρ σ κ |
=def |
[u] ρ σ ((σ', _) ↦ [v] ρ σ' κ) |
Figure 7: Une sémantique en passage par valeur avec affectations
Exercice 42
Commenter la sémantique de la figure 6 en
langage courant. En particulier, dire dans quel ordre cette
sémantique spécifie que doivent être évaluées les
expressions, dans quelles continuations et quelles mémoires
elles sont évaluées.
On peut bien sûr encore donner une sémantique à l'opérateur
C dans ce contexte:
[ C] ρ σ κ =def
κ (σ, (κ', σ', f) ↦ f (_ ↦ ⊥, σ',
(_, σ'', d') ↦ κ' (σ'', d')))
Exercice 43
Soit * un identificateur distingué (le handler
d'exception courant
). On définit les constructions
suivantes:
| try u with x ⇒ v |
=def |
let k0=!* in |
| |
|
C (λ k ⋅ *:=(λ x ⋅ *:=k0; k v); |
| |
|
k (let y=u in *:=k0; y)) |
| raise v |
=def |
!* v |
Alors qu'il était possible, quoique
difficile, de trouver une sémantique par réduction pour C
(les règles LL et LR), il est pratiquement
infaisable d'en trouver une satisfaisante pour les affectations.