4 Modèles, sémantique dénotationelle
La sémantique qu'on a donnée du λ-calcul est par
réduction. Que ce soit la sémantique générale de la
β-réduction ou la sémantique de la stratégie interne
faible, cette sémantique est donnée par un ensemble de règles,
plus la condition que la réduction est la plus petite relation
binaire obéissant aux règles. On dit qu'il s'agit d'une
sémantique opérationnelle.
Il arrive que l'on ait envie d'un autre style de sémantique, plus
synthétique. Intuitivement, on aimerait pouvoir définir la
sémantique du λ-calcul par une fonction u ↦ [u] qui à tout terme u associe un vrai objet mathématique, dans
un domaine D de valeurs. Par exemple, si u = λ x⋅ x,
on aimerait dire que [u] est la fonction identité (sur un
sous-ensemble de D).
[_] sera alors un modèle s'il fournit une
interprétation saine de la β-conversion, autrement
dit si:
u =βv ⇒ [u] = [v]
L'intérêt d'une telle approche, c'est qu'elle va simplifier les
preuves, dans la plupart des cas. Par exemple, on pourra montrer
que deux termes u et v ne sont pas convertibles en exhibant un
modèle du λ-calcul suffisamment simple dans lequel [u] ≠ [v]. De façon plus subtile, on utilisera des
modèles dans lesquels une valeur spéciale ⊥ sera
réservée pour représenter la valeur des programmes qui ne
terminent pas, et on pourra alors assurer qu'un λ-terme u
termine rien qu'en calculant [u] et en vérifiant que le
résultat est différent de ⊥, c'est-à-dire sans avoir à
réduire u pendant un temps indéterminé.
L'autre intérêt d'exhiber des modèles, c'est que souvent ils
seront trop riches, et contiendront des valeurs qui ne sont des
valeurs d'aucun λ-terme. Ceci permet soit de montrer que
certaines constructions sémantiquement saines ne sont pas
réalisables par programme dans le λ-calcul. Par
contrecoup, ceci permettra de suggérer des extensions du
λ-calcul, permettant de réaliser ces constructions, tout
en garantissant à la fois que ces extensions sont cohérentes
avec le λ-calcul et nécessaires pour réaliser la
construction visée.
4.1 Quelques remarques liminaires
Avant de passer à plus compliqué, observons qu'il y a au moins
deux modèles très simples du λ-calcul:
-
le modèle trivial: D est un singleton {*}, et [u] = * pour tout u. Un tel modèle n'apportant pas grand-chose
à notre compréhension, nous nous efforcerons de trouver des
modèles non triviaux.
- Le modèle de termes Λ/=β: ses
éléments sont les classes d'équivalence de λ-termes
modulo β-équivalence. Celui-ci est exactement celui qui
nous intéresse, mais il n'apporte aucune facilité de calcul:
pour raisonner dessus, on est obligé de passer par l'analyse des
propriétés de → (confluence, standardisation, etc., sont
les outils de base).
Nous allons donc essayer de trouver des modèles intermédiaires,
qui soient non triviaux et sur lesquels on peut calculer.
Une première idée est la suivante: on prend un ensemble D de
valeurs (sémantiques, à ne pas confondre avec la notion de
valeurs de la section 3), et on essaie d'interpréter
les termes dans D.
Commençons par les variables: que doit valoir [x] ? Tout
choix étant arbitraire, on va supposer qu'on se donne toujours en
paramètre une valuation ρ qui à toute variable
associe sa valeur. On définira donc non pas [u] pour tout
terme u, mais [u] ρ comme une fonction de u et de
ρ. Clairement, on posera [x] ρ =def ρ (x).
Grâce aux valuations, on va pouvoir définir facilement la valeur
des abstractions. Pour toute valuation ρ, pour toute variable
x et toute valeur v∈ D, définissons ρ [x:=v] comme
étant la valuation qui à x associe v, et à toute autre
variable y associe la valeur qu'elle avait par ρ, soit ρ
(y). En somme, ρ [x:=v] c'est “ρ, sauf que x vaut
maintenant v”. Le valeur [λ x⋅ u] ρ est
alors juste la fonction1
qui prend une valeur v∈ D et retourne [u] (ρ[x:=v]).
Il y a juste un problème ici, c'est que la valeur de λ
x⋅ u est une fonction de D vers D. Mais comme c'est
censé être aussi une valeur, elle doit être dans D aussi.
En clair, on veut trouver un domaine D suffisamment gros pour
que:
(D → D) ⊆ D
où D → D dénote l'ensemble des fonctions de D vers D.
Malheureusement:
Lemme 4
Si (D → D) ⊆ D, alors D est trivial.
Preuve :
D ne peut pas être vide, car sinon D → D contiendrait un
élément (la fonction vide) qui n'est pas dans D. Si D
n'était pas trivial, alors son cardinal α serait donc au
moins 2. Mais alors le cardinal de D → D serait
αα≥ 2α> α par le théorème de
Cantor, ce qui entraîne que D → D ne peut pas être
contenu dans D.
♦
En fait, on veut aussi que D ⊆ (D → D), mais c'est plus
facile à obtenir. La raison est que l'on veut pouvoir
interpréter [uv] ρ comme l'application de [u]
ρ à [v] ρ, mais pour cela il faut que toute valeur
possible pour [u] ρ (dans D) puisse être vue comme une
fonction de D dans D.
Il faut donc trouver d'autres solutions. Une idée due à Dana
Scott est de se restreindre à des domaines D munie d'une
structure supplémentaire, et à demander à ce que l'espace de
fonctions de D vers D préserve la structure. Ceci permet de
court-circuiter l'argument de circularité. Par exemple, si on
prend D = R avec sa structure d'espace topologique, et qu'on
ne garde que les fonctions continues de R vers R, alors
il n'y a pas plus de fonctions continues que de réels. (La raison
est que le cardinal des réels est 2ℵ0, et que les
fonctions continues de R vers R sont déterminées de
façon unique comme les prolongements par continuité de leurs
restriction à Q. Il n'y en a donc pas plus que de fonctions
de Q vers R, soit pas plus que
(2ℵ0)ℵ0 = 2ℵ0.) Malheureusement,
même si le problème de cardinalité est ainsi vaincu, ça ne
suffit pas pour résoudre le problème entièrement.
4.2 Les ordres partiels complets (cpo)
La solution de Scott est de considérer des domaines D qui sont
des cpo, ou ordres partiels complets (cpo signifie
“complete partial order”):
Définition 4
Un ordre partiel
est un couple (D, ≤), où ≤
est une relation d'ordre sur D.
Un majorant d'une partie E de D est un élément x de D
tel que y ≤ x pour tout y dans E. Une borne
supérieure
de E est un majorant minimal supE; si
elle existe, elle est unique.
Une chaîne
dans (D, ≤) est une suite infinie
croissante (xi)i∈N d'éléments de D (soit:
i≤ j implique xi ≤ xj).
On dira qu'un tel ordre partiel est complet
si et
seulement si D a un élément minimum ⊥ et si tout
chaîne a une borne supérieure.
Une fonction f de (D, ≤) vers (D', ≤') est dite monotone
si et seulement si x≤ y implique f (x) ≤' f
(y). Elle est continue
si et seulement si elle
préserve les bornes supérieures de chaînes:
f (supC) = sup{f (c) ∣ c ∈ C}
pour toute chaîne C dans D.
L'idée est qu'une chaîne est une suite d'approximations de la
valeur que l'on souhaite calculer, et l'ordre ≤ est l'ordre
“est moins précis que”. L'élément ⊥ représente alors
l'absence totale d'information, et la borne supérieure d'une
chaîne représente la valeur finale d'un calcul.
Précisément, on peut voir les chaînes émerger à partir
de l'analyse de la réduction d'un terme. Par exemple, si on prend
le terme J =def Y G, avec G =def λ x, y, z ⋅ y (x z), on
a les réductions suivantes, avec à chaque étape ce qu'on peut
conclure sur le résultat final R du calcul, s'il existe:
|
|
| J = |
Y G |
R = ? |
| →* |
G (Y G) |
R = ? |
| → |
λ y, z ⋅ y (Y G z) |
R = λ y, z ⋅ y ? |
| →* |
λ y, z ⋅ y (G (Y G) z) |
R = λ y, z ⋅ y ? |
| →* |
λ y, z ⋅ y (λ z' ⋅ z (Y G z')) |
R = λ y, z ⋅ y (λ z' ⋅ z ?) |
| →* |
λ y, z ⋅ y (λ z' ⋅ z (λ z'' ⋅ z' (Y G z''))) |
R = λ y, z ⋅ y (λ z' ⋅ z (λ z'' ⋅ z' ?)) |
| |
… |
|
λ z0, z1 ⋅ z0 (λ z2 ⋅ z1 (λ z3 ⋅ z2 (…
(λ zk+1 ⋅ zk (λ zk+2 ⋅ zk+1 ( …
après un α-renommage adéquat. On note en général
plutôt Ω le point d'interrogation, et l'espace des arbres
finis ou infinis ainsi obtenus s'appelle l'espace des arbres de
Böhm.
Exercice 24
Construire la suite d'arbres de Böhm associée à la
réduction standard de λ x ⋅ x. Quelle est sa borne
supérieure ?
Exercice 25
Construire la suite d'arbres de Böhm associée à la
réduction standard de (λ x ⋅ xx) (λ x ⋅
xx). Quelle est sa borne supérieure ? Justifier pourquoi on
appelle ce terme Ω.
Le modèle des arbres de Böhm — pour vérifier qu'il s'agit
effectivement d'un modèle, on consultera
[Bar84] — est relativement peu informatif
encore: il code essentiellement la syntaxe et la réduction,
modulo le théorème de standardisation.
On va maintenant construire quelques modèles (D, ≤), donc
quelques cpo tels que [D → D] = D, où [D → D] est l'espace
des fonctions continues de D dans D. Une première
observation, c'est que nous avons juste besoin que [D → D] et
D soient isomorphes, en fait même seulement qu'il existe deux
fonctions continues:
i : D → [D → D] r : [D → D] → D
telles que i ∘ r soit l'identité sur [D → D]. Un tel
domaine D est appelé un domaine réflexif.
En effet, on définira alors:
|
|
| [x] ρ = |
ρ (x) |
| [uv] ρ = |
i ([u] ρ) ([v] ρ) |
| [λ x⋅ u] ρ = |
r (v ↦ [u] (ρ[x:=v])) |
|
On a alors:
Lemme 5
Si u =βv, alors [u] ρ = [v] ρ pour tout
ρ.
Preuve :
Il suffit de montrer le résultat lorsque u → v. On le
montre alors par récurrence sur la profondeur du rédex
contracté dans u pour obtenir v. Le cas inductif, où
cette profondeur est non nulle, est trivial. Dans le cas de base,
on doit démontrer que [(λ x ⋅ s) t] ρ =
[s [x:=t]] ρ. Mais [(λ x ⋅ s) t] ρ =
i ([λ x ⋅ s] ρ) ([t] ρ) = i (r (v
↦ [s] (ρ[x:=v])) ([t] ρ) = (v ↦ [s]
(ρ[x:=v]) ([t] ρ) (puisque i ∘ r est
l'identité) = [s] (ρ [x:=[t] ρ]), et il ne reste
plus qu'à montrer que ce dernier vaut [s [x:=t]] ρ.
Ceci se fait par une récurrence structurelle facile sur s.
♦
4.3 Le modèle Pω
Une première construction d'un modèle, due à Plotkin et Scott,
et qui est très concrète, est le modèle P ω des
parties de l'ensemble N des entiers naturels (on note aussi
N = ω, d'où le nom), avec l'ordre ⊆.
Figure 1: Codage des couples d'entiers
La construction du modèle P ω est fondée sur quelques
remarques. D'abord, on peut représenter tout couple ⟨ m,
n⟩ d'entiers par un entier, par exemple par la formule:
La valeur de ⟨ m, n⟩ en fonction de m en abscisse,
et de n en ordonnée, est donnée en figure 1.
Ensuite, on peut représenter tout ensemble fini e =def {n1,
…, nk} d'entiers par le nombre binaire [e] =def Σi=1k
2ni. Réciproquement, tout entier m peut être écrit en
binaire, et représente l'ensemble fini em de tous les entiers
n tels que le bit numéro n de m est à 1: cf.
figure 2, où l'on a écrit l'ensemble {1, 3, 4,
7, 9, 10} sous la forme du nombre binaire 11010011010, soit
1690 en décimal — autrement dit, [{1, 3, 4, 7, 9, 10}] =
1690 et e1690 = {1, 3, 4, 7, 9, 10}.
Figure 2: Codage des ensembles finis
Exercice 26
Trouver une formule pour π1 : ⟨ m, n⟩ ↦ m
et pour π2 : ⟨ m, n⟩ ↦ n.
L'astuce principale dans la construction de P ω est que
la continuité des fonctions de P ω dans P ω
permet de les représenter comme limites d'objets finis:
Lemme 6
Pour toute fonction f de P ω dans P ω, f
est continue si et seulement si pour tout x∈ P ω, f
(x) est l'union de tous les f (y), y partie finie de x.
Preuve :
Seulement si: supposons f continue, et soit x un ensemble non
vide. Énumérons ses éléments, par exemple en ordre
croissant n1, n2, ..., nk, ...(si la suite
s'arrête à l'indice k, on poserait nk = nk+1 = nk+2
= …); posons yk =def {n1, n2, …, nk} pour tout
k, ceci définit une chaîne dont la borne supérieure est
x. Comme f est continue, f (x) = ∪k f (yk) ⊆
∪y finie ⊆ x f (y); réciproquement,
∪y finie ⊆ x f (y) ⊆ f (x)
car f est monotone, donc f (y) ⊆ f (x) pour tout y
⊆ x. Finalement, si x est vide, f (x) =
∪y finie ⊆ x f (y) est évident.
Si: supposons que f (x) = ∪y finie ⊆
x f (y), et soit (yk)k∈N une chaîne, x =
∪k yk. Donc f (x) est l'union des f (y), y finie
partie de x, et contient en particulier tous les f (yk), donc
f (x) ⊇ ∪k f (yk); réciproquement, f (x)
⊆ ∪k f (yk) car toute partie finie y de x est
incluse dans un yk.
♦
L'idée est alors que toute fonction continue est définie par ses
valeurs sur les ensembles finis, et que les ensembles finis sont
codables par des entiers. On définit donc:
r : [Pω → Pω] → Pω
f ↦ {⟨ m, n⟩ ∣ n ∈ f (em)}
et son inverse à gauche:
i : Pω → [Pω → Pω]
e ↦ (x ↦ {n ∈ N ∣ ∃ y fini ⊆ x ⋅
⟨ [y], n⟩ ∈ e}
Théorème 4
La fonction i ∘ r est l'identité sur [Pω →
Pω], i et r sont continues. De plus, la fonction
(u, ρ) ↦ [u] ρ est bien définie.
Autrement dit, on a bien défini un modèle. Le fait que la
fonction (u, ρ) ↦ [u] ρ soit bien définie signifie
notamment que, dans la définition de [λ x ⋅ u]
ρ, la fonction v ↦ [u] (ρ[x:=v]) est bien
continue — ce qui n'est pas totalement immédiat. Finalement, il
est clair que Pω est non trivial.
Exercice 27
Démontrer le théorème 4. (En cas de
panne, se référer à [Bar84], pp.469–476.)
Exercice 28
Calculer [λ x ⋅ x] ρ dans Pω, et
montrer qu'il est non vide.
Exercice 29
Calculer [λ x,y ⋅ xy] ρ dans Pω,
et montrer qu'il est différent de [λ x ⋅ x]
ρ. En déduire que la règle (η) n'est pas
déductible de la (β)-équivalence, autrement dit λ
x ⋅ ux ≠βu en général.
On peut aussi montrer ce dernier résultat syntaxiquement:
λ x, y ⋅ xy et λ x ⋅ x sont
η-équivalents mais normaux et différents, donc par
β-équivalents, par la confluence du λ-calcul. La
preuve sémantique via Pω remplace la démonstration
combinatoire de la confluence du λ-calcul par la
démonstration sémantique que Pω est un modèle.
4.4 Sémantiques d'un λ-calcul enrichi
Une famille plus générale de modèles, due à Scott, est
présentée en annexe A. Elle permet de montrer le
résultat suivant:
Théorème 5
Soit (D0, ≤0) un cpo quelconque. Alors il existe un cpo
(D∞, ≤∞) contenant (D0, ≤0) et tel que
D∞= [D∞→ D∞] à isomorphisme près.
Un intérêt que l'on peut avoir dans les cpo ne tient pas tant au
fait qu'on puisse fabriquer des domaines D réflexifs, mais au
fait que finalement ils modélisent une notion de calcul par approximations successives.
On peut alors fabriquer des cpo non nécessairement réflexifs
pour modéliser des concepts informatiques intéressants. Par
exemple, le cpo des booléens est B⊥ =def {F,
V, ⊥}, avec l'ordre ⊥ ≤ F, ⊥ ≤ V,
mais F et V incomparables. En clair, et pour
paraphraser l'exemple des arbres de Böhm plus haut, un programme
qui doit calculer un booléen soit n'a pas encore répondu (sa
valeur courante est ⊥) soit a répondu F (et on sait
tout sur la valeur retournée, donc F doit être un
élément maximal), soit a répondu V (de même). Comme
F et V sont deux valeurs différentes, et maximales en
termes de précision, elles doivent être incomparables.
Le cpo des entiers, de même, est N⊥ =def N ∪
{⊥}, avec l'ordre dont les seules instances non triviales sont
⊥ ≤ n, n∈ N. Les entiers sont incomparables entre
eux pour les mêmes raisons que les booléens, et son diagramme de
Hasse est donné en figure 3. Un tel cpo, dont la
hauteur est inférieure ou égale à 1, est dit plat.
Figure 3: Le cpo plat des entiers naturels
Exercice 30
Si D1 et D2 sont deux cpo, montrer que [D1 → D2] n'est
jamais plat, sauf si D1 = {⊥} et D2 est plat.
On peut alors construire sémantiquement un langage plus riche que
le λ-calcul pur, mais qui contienne toujours le
λ-calcul. Par exemple, on peut décider d'ajouter à la
syntaxe des termes du λ-calcul des constantes F et
V, la constante 0 et un symbole S
représentant le successeur.
Sémantiquement, on a besoin d'un domaine réflexif (pour avoir
les fonctions i et r) contenant l'union de B⊥ et
N⊥. C'est facile: appliquer le
théorème 5 à D0 =def B⊥∪ N⊥
(un cpo plat encore). On peut alors définir:
| [T]ρ |
=def |
V |
| [F]ρ |
=def |
F |
| [0]ρ |
=def |
0 |
| [S]ρ |
=def |
r (v ↦ v+1) |
Il y a quand même un problème dans cette définition, à
savoir que v+1 n'est défini que quand v est un entier, et donc
la fonction v ↦ v+1 n'est pas définie. Si v = ⊥,
c'est-à-dire que typiquement v est le “résultat” d'un
programme qui ne termine pas, intuitivement on va prendre v+1 =
⊥, autrement dit le calcul de v+1 ne terminera pas non plus:
une telle fonction, qui envoie ⊥ sur ⊥, est dite stricte.
Si v n'est pas dans N⊥, alors une convention possible est
de considérer que v+1 est un programme absurde, qui ne termine
pas, autrement dit v+1 = ⊥. En pratique, un tel programme
absurde plante, ou s'interrompt sur un message d'erreur, et c'est en
ce sens qu'il ne termine pas: il n'arrive jamais au bout du calcul.
Regardons maintenant les fonctions que l'on peut définir sur les
booléens. Le “ou” ∨ doit avoir la propriété que
F ∨ F = F et V ∨ x = x ∨ V =
V pour tout x∈ B, mais qu'en est-il si x = ⊥ ?
En Pascal, le ou est strict en ses deux arguments. Autrement dit,
x ∨ y est calculé en calculant x, y, puis en en prenant
la disjonction. En C, le ou est strict en son premier argument mais
pas en son second: x || y est calculé en calculant
x; si x vaut V, alors V est retourné comme valeur,
sinon c'est celle de y qui est calculée. En particulier, V
∨ ⊥ = V. La table de vérité complète est:
|
|
|| |
V |
F |
⊥ |
| V |
V |
V |
V |
| F |
V |
F |
⊥ |
| ⊥ |
⊥ |
⊥ |
⊥ |
|
Il y a encore d'autres possibilités. Une qui maximise le nombre
de cas où x ∨ y termine est donnée par la table de
vérité:
|
|
| ∣ |
V |
F |
⊥ |
| V |
V |
V |
V |
| F |
V |
F |
⊥ |
| ⊥ |
V |
⊥ |
⊥ |
|
Cette fonction ∣ est en effet continue, donc sémantiquement
acceptable. Elle est connue sous le nom de “ou parallèle”, car
on peut la réaliser en évaluant x sur un processeur 1, y sur
un processeur 2. Le premier des deux qui répond V
interrompt l'autre, et V est retourné. Si les deux
répondent F, alors F est retourné. Sinon, rien
n'est retourné, autrement dit la valeur finale est ⊥.
Il est remarquable que, alors que le ou de Pascal et le || de
C étaient simulables en λ-calcul, le ou parallèle ne
l'est pas. La raison est que le λ-calcul est intrinsèquement séquentiel. Ceci ce manifeste
mathématiquement par le fait que les valeurs sémantiques des
fonctions définissables par des λ-termes sont non
seulement continues, mais stables:
Définition 5
Deux éléments x et y d'un cpo sont dits compatibles
si et seulement s'il existe z dans le cpo tel
que x≤ z et y≤ z.
Supposons que le cpo D ait la propriété que pour tous
éléments compatibles x et y, il existe une borne
inférieure inf(x, y). Une fonction f : D → D' est stable
si et seulement si elle est continue, et pour tous
x, y compatibles dans D la borne inférieure inf(f (x), f (y)) existe et est égale à f (inf(x, y)).
On munit l'espace des fonctions stables de D vers D' de l'ordre de Berry
: f ≤s g si et seulement si x≤ y
implique que inf(f (y), g (x)) existe et égale f (x).
Exercice 31
Montrer que le ou parallèle n'est pas stable. En déduire
qu'on ne peut pas le coder en λ-calcul enrichi avec
T, F, 0, S.
On peut coder le test “if ...then ...else ...”.
Sémantiquement, c'est la fonction if (x, y, z) telle que if
(V, y, z) = y, if (F, y, z) = z, et si x n'est pas un
booléen alors if (x, y, z) = ⊥. Noter que cette fonction est
stricte en son premier argument, mais pas en son deuxième et en
son troisième.
Par contre, des fonctions comme + et × seront strictes en
tous les arguments. Même × est en général choisie
stricte, ce qui signifie que 0 × ⊥ = ⊥ et non 0. On
remarquera qu'une fonction appelée par valeur (+, ×) est
nécessairement stricte, car cette fonction attend que ses
arguments soient évalués avant de continuer le calcul; alors
qu'une fonction en appel par nom peut être non stricte. (Le cpo
que nous choisissons pour comprendre ces notions dans un cadre
d'analyse des réductions est celui dont les valeurs sont les
arbres de Böhm.) Le cadre sémantique est plus souple et
accomode les deux notions dans une seule définition. De plus, les
détails réels des réductions importent peu, finalement, du
moment que les équations sémantiques sont respectées.
Par exemple, un λ-calcul avec booléens et entiers, en
appel par valeur sauf sur le “if ...then ...else ...”,
serait défini comme suit. On prend un cpo D tel que:
D = (N ⊕ B ⊕ [D → D])⊥
modulo un isomorphisme qui sera laissé implicite dans la suite,
où ⊕ dénote l'union disjointe d'ensembles ordonnés, et
D⊥ dénote l'ensemble ordonné obtenu à partir de D en
ajoutant un élément ⊥ plus bas que tous les éléments de
D, et on définit [_] comme en figure 4.
| [x] ρ |
=def |
ρ (x) |
| [λ x ⋅ u] ρ |
=def |
| (v ↦
|
⎧
⎨
⎩ |
| ⊥ |
si v=⊥ |
| [u] (ρ[x:=v]) |
sinon |
|
|
) |
|
| [uv] ρ |
=def |
⎧
⎨
⎩ |
| f ([v] ρ) |
si f =def [u] ρ ∈ [D → D] |
| ⊥ |
sinon |
|
|
|
| [T]ρ |
=def |
V |
| [F]ρ |
=def |
F |
| [0]ρ |
=def |
0 |
| [S]ρ |
=def |
|
| [if (u, v, w)] ρ |
=def |
⎧
⎨
⎩ |
| [v] ρ |
si [u] ρ = V |
| [w] ρ |
si [u] ρ = F |
| ⊥ |
sinon |
|
|
|
Figure 4: Sémantique dénotationnelle de l'appel par valeur
Dans les langages dits paresseux, comme Miranda ou Haskell,
qui simule un appel par nom d'une façon un peu plus efficace
(voir partie 3), la seule différence serait qu'il n'attend pas
d'évaluer l'argument, et donc on aurait juste:
| [λ x ⋅ u] ρ |
=def |
(v ↦ [u] (ρ[x:=v])) |
On voit alors qu'on peut réaliser une fonction λ x ⋅ u
qui est normalement en appel par nom par une stratégie d'appel par
valeur exactement quand les deux définitions de sa sémantique
coïncident, autrement dit quand cette fonction est stricte. L'appel par valeur étant dans ce cas moins coûteux
en temps et en espace, un bon compilateur pourra compiler les
fonctions détectées comme strictes par une stratégie d'appel
par valeur. Cette détection de fonctions strictes est appelée
en anglais la “strictness analysis”.