A  Modèles D_∞

()

Fixons un cpo (D₀, ≤₀), et construisons une suite de cpo (D_k, ≤_k) par:

avec ≤_k+1 l’ordre point à point, soit: pour tous f, g ∈ [D_k → D_k], f ≤_k+1 g si et seulement si f(x) ≤_k g(x) pour tout x∈ D_k.

On peut construire une fonction r₀ : [D₀ → D₀] → D₀ par: r₀ (f) = f (⊥₀); et on peut construire une fonction i₀ : D₀ → [D₀ → D₀] par: i₀ (x) = (v ↦ x) (une fonction constante). Par récurrence, on définit r_k+1 : [D_k+1 → D_k+1] → D_k+1 par: r_k+1 (f) =_def r_k ∘ f ∘ i_k; et i_k+1 : D_k+1 → [D_k+1 → D_k+1] par: i_k+1 (x) =_def i_k ∘ x ∘ r_k. On a donc un diagramme infini:

avec r_k ∘ i_k l’identité sur D_k. (On remarquera que cette composition est dans le mauvais sens, vu qu’on vu obtenir i ∘ r = id au final. On verra plus tard comment ceci se résout.)

Posons, pour k ≤ l, r_kl : D_l → D_k =_def r_k ∘ r_k+1 ∘ … ∘ r_l−1. Le système formé par les D_k et les r_kl, k ≤ l, est appelé un système projectif de cpo. Intuitivement, ceci revient à voir les D_l se projeter via r_kl dans D_k. On peut alors calculer la limite projective de ce système, qui est un ensemble le plus petit possible D_∞ se projetant sur tous les D_k via des fonctions r_k∞:

Une caractérisation équivalente est:

Preuve : (D_∞, ≤_∞) est clairement un ordre partiel, et si (dⁱ)_{i∈ N} est une chaîne, avec dⁱ = (d_jⁱ)_{j∈ N}, alors sa borne supérieure sup_i dⁱ ne peut être que d =_def (sup_i d₀ⁱ, sup_i d₁ⁱ, …); il ne reste qu’à montrer que d ∈ D_∞, autrement dit que r_kl (sup_i d_lⁱ) = sup_i d_kⁱ pour tout k≤ l. Ceci revient à montrer que r_k (sup_i d_k+1ⁱ) = sup_i d_kⁱ pour tout k, sachant que d_kⁱ = r_k (d_k+1ⁱ); mais r_k est continue, par l’exercice 44.

Il est pratiquement évident que r_k∞ est continue: r_k∞ (sup_i dⁱ) = r_k∞ (sup_i d₀ⁱ, sup_i d₁ⁱ, …) = sup_i d_kⁱ = sup_i r_k∞ (dⁱ). Finalement, r_kl ∘ r_l∞ = r_k∞ pour tout k≤ l par les propriétés générales des limites projectives (mais vous pouvez le vérifier directement).     ♦

Donc D_∞ se projette sur chaque D_k via les r_k∞. Ceci prend en compte la structure formée à partir des projections r_k. On peut aussi tenir compte des i_k, et définir la construction duale: posons, pour k≤ l, i_kl : D_k → D_l =_def i_l−1 ∘ … ∘ i_k+1 ∘ i_k. (Noter que i_kl va de D_k dans D_l, alors que r_kl va de D_l dans D_k !) Le système formé par les D_k et les i_kl, k≤ l, est appelé un système inductif de cpo. Ceci revient à voir non pas D_l se projeter dans D_k, mais D_k s’injecter dans D_l via i_kl.

On pourrait calculer la limite inductive de ce système, qui est en un sens le plus grand ensemble s’injectant dans tous les D_k, et qui est construit comme le quotient de la somme directe des D_k (dont les éléments sont des couples (k, d_k) avec d_k ∈ D_k) par la relation d’équivalence ∼ engendrée par (k, d_k) ∼ (l, d_l) si k≤ l et i_kl (d_k) = d_l. Il se trouve que dans ce cas précis, la limite inductive des D_k est exactement la même que la limite projective D_∞ (ce n’est en général pas le cas des limites injectives et projectives); c’est pourquoi nous n’étudierons pas cette limite inductive en tant que telle.

Preuve : La fonction i_k∞ est bien définie, au sens où i_k∞ (d) est bien dans D_∞, c’est-à-dire que r_j (r_{(j+1) k} (d)) = r_jk (d) pour tout j≤ k−2 (par définition de r_jk), r_(k−1)k (d) = r_k−1 (d) (par définition), d = r_k (i_k(k+1) (d)) (car i_k(k+1) = i_k et r_k ∘ i_k = id), et i_kl (d) = r_l (i_k(l+1) (d)) pour tout l≥ k+1 (car r_l ∘ i_l = id).

La continuité de i_k∞ provient du fait que tous les r_jk, j≤ k et tous les i_kl, k≤ l, sont continus, par l’exercice 44.

Pour vérifier que i_l∞ ∘ i_kl = i_k∞ pour tout k≤ l, on remarque d’abord que pour tous j≤ k≤ l:

Les deux équations du milieu se démontrent en utilisant que r_m ∘ i_m = id pour tout m. Alors si k≤ l, pour tout d∈ D_k on a:

Finalement, (r_k∞ ∘ i_k∞) (d) = d par construction.     ♦

Il s’ensuit que l’on peut considérer que D_k est inclus dans D_∞ à isomorphisme près: l’isomorphisme est i_k∞ de D_k vers son image, et son inverse est la restriction de r_k∞ à l’image de i_k∞. En somme, D_∞ est une sorte d’union de tous les D_k; pour être précis, de complété de cette union: un élément d =_def (d₀, d₁, …, d_k, …) est en effet la limite (la borne supérieure) des d_k, k∈ N. C’est ce que dit le lemme suivant:

Preuve : Notons d’abord que: (a) pour tout k, pour tout f∈ D_k+1, i_k (r_k (f)) ≤_k+1 f. En effet, ceci signifie que pour tout x∈ D_k, i_k (r_k (f)) (x) ≤_k f (x). Montrons-le par récurrence sur k. Pour k=0, i₀ (r₀ (f)) (x) = i₀ (f (⊥₀)) (x) = f (⊥₀) ≤₀ f (x) puisque f est monotone. Sinon, i_k+1 (r_k+1 (f)) (x) = i_k (r_k+1 (f) (r_k (x)) = i_k (r_k (f (i_k (r_k (x))))) ≤_k f (i_k (r_k (x))) (par récurrence) ≤_k f (x) (par récurrence et monotonie de f).

Soit d = (d₀, d₁, …, d_k, …) ∈ D_∞. On observe que: (b) i_k (d_k) ≤_k+1 d_k+1 pour tout k. En effet, d_k = r_k (d_k+1) puisque d∈ D_∞ et on applique (a). Donc: (c) i_kl (d_k) ≤_l d_l pour tout k≤ l. Alors:

par la remarque (c).

Finalement, ( i_k∞ ∘ r_k∞ )_{k∈ N} est une chaîne car k≤ l implique i_k∞ ∘ r_k∞ ≤ i_l∞ ∘ r_l∞. En effet:

par (a).     ♦

On peut maintenant définir i et r sur D_∞:

Preuve : Pour montrer que i est bien définie, il faut montrer que pour tout y =_def (y₀, y₁, …, y_k, …) de D_∞, i (y) en tant que fonction qui à x = (x₀, …, x_k, …) associe (y₁ (x₀), y₂ (x₁), …, y_k+1 (x_k), …) est bien continue. Ceci est ne présente pas de difficulté, car les bornes supérieures sont prises composante par composante et chaque y_k est continue. De même, i est continue parce que (sup_j y_k+1^j) (x_k) = sup_j (y_k+1^j (x_k)) par définition. De même, r est bien définie car r₀ (d₁) = d₁ (⊥₀) = r_0∞ (f (i_0∞ (⊥₀))) = d₀, et r_k+1 (d_k+2) = r_k ∘ d_k+2 ∘ i_k (par définition de r_k+1) = r_k ∘ r_(k+1)∞ ∘ f ∘ i_(k+1)∞ ∘ i_k = r_k∞ ∘ f ∘ i_k∞ = d_k+1, donc r (d) est bien dans D_∞. De plus, r est continue parce que toutes les r_k∞ et les i_k∞ sont continues, et que la composition ∘ est continue.

Avant de continuer, remarquons que dans un cpo: (a) si on a une suite a_jj′ telle que pour tous j, j′, il existe un k tel que a_jj′ ≤ a_kk, alors sup_j,j′ a_jj′ = sup_k a_kk. En effet sup_k a_kk ≤ sup_j,j′ a_jj′ parce que tous les a_kk sont des a_jj′, et réciproquement sup_j,j′ a_jj′ ≤ sup_kjj′ a_{kjj′ kjj′} (où k_jj′ est un k tel que a_jj′ ≤ a_kk, pour tous j, j′) ≤ sup_k a_kk.

Soit f une fonction continue f de D_∞ dans D_∞, d∈ D_∞ et posons a_jj′ =_def (i_j∞ ∘ r_j∞) (f ((i_j′∞ ∘ r_j′∞) (d))). Alors comme i_j∞ ∘ r_j∞ forme une chaîne (lemme 10) et que f est monotone, a_jj′ ≤ a_kk pour k = max(j,j′). Donc par (a), on a:

En résumé: (b) f (d) = sup_k i_k∞ (r_k∞ (f (i_k∞ (r_k∞ (d)))).

Calculons maintenant i ∘ r. Pour toute f ∈ [D_∞→ D_∞], montrons que i (r (f)) = f. Pour ceci, il suffit de montrer que i (r (f)) (d) = f (d) pour tout d∈ D_∞. Remarquons d’abord que: (c) i (r (f)) (d) = sup_k i_k∞ (r_k∞ (i (r (f)) (d)) par le lemme 10. Calculons donc r_k∞ (i (r (f)) (d)). Posons r (f) =_def (y₀, …, y_k, …); et d =_def (d₀, …, d_k, …), autrement dit d_k = r_k∞ (d) (puisque r_k∞ ne fait que récupérer la composant numéro k). Alors r_k∞ (i (r (f)) (d)) = y_k+1 (d_k) (par définition de i) = y_k+1 (r_k∞ (d)). Or par définition y_k+1 = r_k∞ ∘ f ∘ i_k∞, donc r_k∞ (i (r (f)) (d)) = r_k∞ (f (i_k∞ (r_k∞ (d)))). Par (c):

en utilisant la remarque (b). C’était la partie la plus compliquée à montrer.

Calculons maintenant r ∘ i. Fixons y =_def (y₀, y₁, …, y_k, …) dans D_∞. La fonction f =_def i (y) envoie tout x =_def (x₀, x₁, …, x_k, …) vers (y₁ (x₀), y₂ (x₁), …, y_k+1 (x_k), …). Et r (i (y)) = r (f) est alors un élément (d₀, d₁, …, d_k, …) tel que, d’une part, d₀ = r_0∞ (f (i_0∞ (⊥₀))) = y₁ (x₀) avec x₀ la composante 0 de i_0∞ (⊥₀), soit x₀ = r_0∞ (i_0∞ (⊥₀)) = ⊥₀, donc d₀ = y₁ (⊥₀) = y₀; d’autre part, d_k+1 est la fonction qui à x_k associe r_k∞ (f (i_k∞ (x_k))) = y_k+1 (r_k∞ (i_k∞ (x_k))) = y_k+1 (x_k), donc d_k+1 = y_k+1. Donc (r ∘ i) (y) = y, pour tout y.     ♦

Ce dernier résultat peut aussi se montrer en prouvant que la βη-réduction est confluente, et en remarquant ensuite qu’Ω et λ x · x n’ont aucun rédex commun.