()
Fixons un cpo (D0, ≤0), et construisons une suite de cpo (Dk, ≤k) par:
Dk+1 =def [Dk → Dk] |
avec ≤k+1 l’ordre point à point, soit: pour tous f, g ∈ [Dk → Dk], f ≤k+1 g si et seulement si f(x) ≤k g(x) pour tout x∈ Dk.
On peut construire une fonction r0 : [D0 → D0] → D0 par: r0 (f) = f (⊥0); et on peut construire une fonction i0 : D0 → [D0 → D0] par: i0 (x) = (v ↦ x) (une fonction constante). Par récurrence, on définit rk+1 : [Dk+1 → Dk+1] → Dk+1 par: rk+1 (f) =def rk ∘ f ∘ ik; et ik+1 : Dk+1 → [Dk+1 → Dk+1] par: ik+1 (x) =def ik ∘ x ∘ rk. On a donc un diagramme infini:
avec rk ∘ ik l’identité sur Dk. (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, rkl : Dl → Dk =def rk ∘ rk+1 ∘ … ∘ rl−1. Le système formé par les Dk et les rkl, k ≤ l, est appelé un système projectif de cpo. Intuitivement, ceci revient à voir les Dl se projeter via rkl dans Dk. 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 Dk via des fonctions rk∞:
|
Une caractérisation équivalente est:
D∞= { (dk)k∈ N ∣ ∀ k · dk = rk (dk+1) } |
Preuve : (D∞, ≤∞) est clairement un ordre partiel, et si (di)i∈ N est une chaîne, avec di = (dji)j∈ N, alors sa borne supérieure supi di ne peut être que d =def (supi d0i, supi d1i, …); il ne reste qu’à montrer que d ∈ D∞, autrement dit que rkl (supi dli) = supi dki pour tout k≤ l. Ceci revient à montrer que rk (supi dk+1i) = supi dki pour tout k, sachant que dki = rk (dk+1i); mais rk est continue, par l’exercice 44.
Il est pratiquement évident que rk∞ est continue: rk∞ (supi di) = rk∞ (supi d0i, supi d1i, …) = supi dki = supi rk∞ (di). Finalement, rkl ∘ rl∞ = rk∞ 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 Dk via les rk∞. Ceci prend en compte la structure formée à partir des projections rk. On peut aussi tenir compte des ik, et définir la construction duale: posons, pour k≤ l, ikl : Dk → Dl =def il−1 ∘ … ∘ ik+1 ∘ ik. (Noter que ikl va de Dk dans Dl, alors que rkl va de Dl dans Dk !) Le système formé par les Dk et les ikl, k≤ l, est appelé un système inductif de cpo. Ceci revient à voir non pas Dl se projeter dans Dk, mais Dk s’injecter dans Dl via ikl.
On pourrait calculer la limite inductive de ce système, qui est en un sens le plus grand ensemble s’injectant dans tous les Dk, et qui est construit comme le quotient de la somme directe des Dk (dont les éléments sont des couples (k, dk) avec dk ∈ Dk) par la relation d’équivalence ∼ engendrée par (k, dk) ∼ (l, dl) si k≤ l et ikl (dk) = dl. Il se trouve que dans ce cas précis, la limite inductive des Dk 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.
ik∞ (d) =def (r0k (d), r1k (d), …, r(k−1)k (d), d, ik(k+1) (d), ik(k+2) (d), …) |
Preuve : La fonction ik∞ est bien définie, au sens où ik∞ (d) est bien dans D∞, c’est-à-dire que rj (r(j+1) k (d)) = rjk (d) pour tout j≤ k−2 (par définition de rjk), r(k−1)k (d) = rk−1 (d) (par définition), d = rk (ik(k+1) (d)) (car ik(k+1) = ik et rk ∘ ik = id), et ikl (d) = rl (ik(l+1) (d)) pour tout l≥ k+1 (car rl ∘ il = id).
La continuité de ik∞ provient du fait que tous les rjk, j≤ k et tous les ikl, k≤ l, sont continus, par l’exercice 44.
Pour vérifier que il∞ ∘ ikl = ik∞ 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 rm ∘ im = id pour tout m. Alors si k≤ l, pour tout d∈ Dk on a:
|
Finalement, (rk∞ ∘ ik∞) (d) = d par construction. ♦
Il s’ensuit que l’on peut considérer que Dk est inclus dans D∞ à isomorphisme près: l’isomorphisme est ik∞ de Dk vers son image, et son inverse est la restriction de rk∞ à l’image de ik∞. En somme, D∞ est une sorte d’union de tous les Dk; pour être précis, de complété de cette union: un élément d =def (d0, d1, …, dk, …) est en effet la limite (la borne supérieure) des dk, k∈ N. C’est ce que dit le lemme suivant:
Preuve : Notons d’abord que: (a) pour tout k, pour tout f∈ Dk+1, ik (rk (f)) ≤k+1 f. En effet, ceci signifie que pour tout x∈ Dk, ik (rk (f)) (x) ≤k f (x). Montrons-le par récurrence sur k. Pour k=0, i0 (r0 (f)) (x) = i0 (f (⊥0)) (x) = f (⊥0) ≤0 f (x) puisque f est monotone. Sinon, ik+1 (rk+1 (f)) (x) = ik (rk+1 (f) (rk (x)) = ik (rk (f (ik (rk (x))))) ≤k f (ik (rk (x))) (par récurrence) ≤k f (x) (par récurrence et monotonie de f).
Soit d = (d0, d1, …, dk, …) ∈ D∞. On observe que: (b) ik (dk) ≤k+1 dk+1 pour tout k. En effet, dk = rk (dk+1) puisque d∈ D∞ et on applique (a). Donc: (c) ikl (dk) ≤l dl pour tout k≤ l. Alors:
|
par la remarque (c).
Finalement, ( ik∞ ∘ rk∞ )k∈ N est une chaîne car k≤ l implique ik∞ ∘ rk∞ ≤ il∞ ∘ rl∞. En effet:
|
par (a). ♦
On peut maintenant définir i et r sur D∞:
Soit r la fonction de [D∞→ D∞] vers D∞ qui à f associe (d0, d1, …, dk, …) défini par: d0 = r0∞ (f (i0∞ (⊥0))), dk+1 ∈ Dk+1 = [Dk → Dk] est la fonction rk∞ ∘ f ∘ ik∞.
Preuve : Pour montrer que i est bien définie, il faut montrer que pour tout y =def (y0, y1, …, yk, …) de D∞, i (y) en tant que fonction qui à x = (x0, …, xk, …) associe (y1 (x0), y2 (x1), …, yk+1 (xk), …) est bien continue. Ceci est ne présente pas de difficulté, car les bornes supérieures sont prises composante par composante et chaque yk est continue. De même, i est continue parce que (supj yk+1j) (xk) = supj (yk+1j (xk)) par définition. De même, r est bien définie car r0 (d1) = d1 (⊥0) = r0∞ (f (i0∞ (⊥0))) = d0, et rk+1 (dk+2) = rk ∘ dk+2 ∘ ik (par définition de rk+1) = rk ∘ r(k+1)∞ ∘ f ∘ i(k+1)∞ ∘ ik = rk∞ ∘ f ∘ ik∞ = dk+1, donc r (d) est bien dans D∞. De plus, r est continue parce que toutes les rk∞ et les ik∞ sont continues, et que la composition ∘ est continue.
Avant de continuer, remarquons que dans un cpo: (a) si on a une suite ajj′ telle que pour tous j, j′, il existe un k tel que ajj′ ≤ akk, alors supj,j′ ajj′ = supk akk. En effet supk akk ≤ supj,j′ ajj′ parce que tous les akk sont des ajj′, et réciproquement supj,j′ ajj′ ≤ supkjj′ akjj′ kjj′ (où kjj′ est un k tel que ajj′ ≤ akk, pour tous j, j′) ≤ supk akk.
Soit f une fonction continue f de D∞ dans D∞, d∈ D∞ et posons ajj′ =def (ij∞ ∘ rj∞) (f ((ij′∞ ∘ rj′∞) (d))). Alors comme ij∞ ∘ rj∞ forme une chaîne (lemme 10) et que f est monotone, ajj′ ≤ akk pour k = max(j,j′). Donc par (a), on a:
|
En résumé: (b) f (d) = supk ik∞ (rk∞ (f (ik∞ (rk∞ (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) = supk ik∞ (rk∞ (i (r (f)) (d)) par le lemme 10. Calculons donc rk∞ (i (r (f)) (d)). Posons r (f) =def (y0, …, yk, …); et d =def (d0, …, dk, …), autrement dit dk = rk∞ (d) (puisque rk∞ ne fait que récupérer la composant numéro k). Alors rk∞ (i (r (f)) (d)) = yk+1 (dk) (par définition de i) = yk+1 (rk∞ (d)). Or par définition yk+1 = rk∞ ∘ f ∘ ik∞, donc rk∞ (i (r (f)) (d)) = rk∞ (f (ik∞ (rk∞ (d)))). Par (c):
|
en utilisant la remarque (b). C’était la partie la plus compliquée à montrer.
Calculons maintenant r ∘ i. Fixons y =def (y0, y1, …, yk, …) dans D∞. La fonction f =def i (y) envoie tout x =def (x0, x1, …, xk, …) vers (y1 (x0), y2 (x1), …, yk+1 (xk), …). Et r (i (y)) = r (f) est alors un élément (d0, d1, …, dk, …) tel que, d’une part, d0 = r0∞ (f (i0∞ (⊥0))) = y1 (x0) avec x0 la composante 0 de i0∞ (⊥0), soit x0 = r0∞ (i0∞ (⊥0)) = ⊥0, donc d0 = y1 (⊥0) = y0; d’autre part, dk+1 est la fonction qui à xk associe rk∞ (f (ik∞ (xk))) = yk+1 (rk∞ (ik∞ (xk))) = yk+1 (xk), donc dk+1 = yk+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.