Previous Up Next

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

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:

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 vD, 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 vD 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

DD dénote l’ensemble des fonctions de D vers D. Malheureusement:

Lemme 4   Si (DD) ⊆ D, alors D est trivial.

Preuve : D ne peut pas être vide, car sinon DD 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 DD serait αα≥ 2α> α par le théorème de Cantor, ce qui entraîne que DD ne peut pas être contenu dans D.     ♦

En fait, on veut aussi que D ⊆ (DD), 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 20, 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 (20)0 = 20.) 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 yx 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)iN d’éléments de D (soit: ij implique xixj).

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 xy 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 GR = ? 
    →*G (Y G)R = ? 
    →λ yz · y (Y G z)R = λ yz · y ? 
    →*λ yz · y (G (Y Gz)R = λ yz · y ? 
    →*λ yz · y (λ z′ · z (Y G z′))R = λ yz · y (λ z′ · z ?) 
    →*λ yz · y (λ z′ · z (λ z″ · z′ (Y G z″)))R = λ yz · y (λ z′ · z (λ z″ · z′ ?)) 
 

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 uv 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:

  λ z0z1 · 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 [DD] = D, où [DD] est l’espace des fonctions continues de D dans D. Une première observation, c’est que nous avons juste besoin que [DD] 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 ir soit l’identité sur [DD]. 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]))

ve 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:

Lemme 5 (Correction)   Si u =βv, alors [u] ρ = [v] ρ pour tout ρ.

Preuve : Il suffit de montrer le résultat lorsque uv. 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 ir 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:

  ⟨ mn ⟩ =def 
(m+n) (m+n+1) 
2
 + 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] =defi=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 xP ω, 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 finiex f (y); réciproquement, ∪y finiex f (y) ⊆ f (x) car f est monotone, donc f (y) ⊆ f (x) pour tout yx. Finalement, si x est vide, f (x) = ∪y finiex f (y) est évident.

Si: supposons que f (x) = ∪y finiex f (y), et soit (yk)kN 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 ↦ {⟨ mn⟩ ∣ 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 ir 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 (Scott)   Soit (D0, ≤0) un cpo quelconque. Alors il existe un cpo (D, ≤) contenant (D0, ≤0) et tel que D= [DD] à 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, nN. 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 [D1D2] 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 BN (un cpo plat encore). On peut alors définir:

    [T]ρ=defV 
    [F]ρ=defF 
    [0]ρ=def
    [S]ρ=defr (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 vv+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 FF = F et Vx = xV = V pour tout xB, mais qu’en est-il si x = ⊥ ?

En Pascal, le ou est strict en ses deux arguments. Autrement dit, xy 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:

  
    ||VF⊥ 
    VVVV 
    FVF⊥ 
    ⊥⊥ 
  

Il y a encore d’autres possibilités. Une qui maximise le nombre de cas où xy termine est donnée par la table de vérité:

  
    ∣VF⊥ 
    VVVV 
    FVF⊥ 
    ⊥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 xz et yz.

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 : DD 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: fs g si et seulement si xy 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]ρ=defV 
      [F]ρ=defF 
      [0]ρ=def
      [S]ρ=def
r (v ↦

          v+1si v ∈ N 
          ⊥sinon
      [if (uvw)] ρ=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”.


Previous Up Next