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 par exemple 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.
Avant de passer à plus compliqué, observons qu’il y a au moins deux modèles très simples du λ-calcul:
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:
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.
La solution de Scott est de considérer des domaines D qui sont des cpo, ou ordres partiels complets (cpo signifie “complete partial order”):
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:
|
où les points d’interrogation dénotent des termes encore inconnus. (Noter qu’il s’agit d’isoler la partie du terme à chaque ligne qui est en forme normale de tête, cf. théorème 3). On peut ordonner les “termes partiels” contenant des points d’interrogation par une relation ≤ telle que u ≤ v si et seulement si v résulte de u par le remplacement de points d’interrogations par des termes partiels. La colonne de droite définit alors bien une chaîne dans l’espace des termes partiels , où ?=⊥. Pour que de telles chaînes aient des bornes supérieures, on est obligé d’enrichir l’espace des termes partiels par des termes infinis. Par exemple, la borne supérieure de la chaîne ci-dessus est:
| λ 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.
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:
|
où v ↦ e dénote la fonction qui à la valeur v associe la valeur e (pour ne pas provoquer de confusions avec la notation des λ-termes, nous ne l’écrivons pas λ v · e).
On a alors:
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. ♦
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 ⊆.
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:
| ⟨ m, n ⟩ =def |
| + m |
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}.
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:
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} |
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.
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.
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:
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.
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:
|
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:
|
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é:
|
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:
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).
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
r (v ↦ ⎧
⎨
⎩
v+1 si v ∈ N ⊥ sinon ) [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:
|
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”.