DM : Programmation 1

DM Programmation I

Énoncé

Younesse Kaddar

Q 1

Soit $u, v∈ {\cal I}$.

  • Cas 1 : $u = \bot$ et $v = \bot$

    clairement : $u∨v = \bot$

  • Cas 2 : $u = \bot$ et $v ≠ \bot$

    clairement : $u∨v = v$

  • Cas 3 : $u ≝ (a,b) ≠ \bot$ et $v ≝ (c, d) ≠ \bot$ (où $a, b, c, d ∈ ℤ∪\lbrace ±∞ \rbrace$) :

    Alors $u∨v = (\min(a,c), \max(b, d))$, car

    • cet élément est clairement un majorant

    • tout majorant $(e, f)$ de $u = (a, b)$ et $v = (c, d)$ vérifie :

      • $u, v ≤ (e, f) ⟹ a, c ≤ e ⟹ \min(a,c) ≤ e$
      • $u, v ≤ (e, f) ⟹ b, d ≤ f ⟹ \max(b, d)≤ f$

    Donc $(\min(a,c), \max(b, d))≤(e,f)$, et $(\min(a,c), \max(b, d))$ est bien le plus petit des majorants.

Q 2

a).

${\cal I}$ est un trellis complet, donc un DCPO, d’où

${\cal I}^n$ reste un DCPO

car un produit cartésien de DCPO est un DCPO pour l’ordre produit (d’après le cours), et on conclut par une récurrence immédiate.

b).

Lemme : Un produit cartésien fini $𝒯 ≝ 𝒯_1 × ⋯ × 𝒯_n$ de treillis complets reste un treillis complet.

Soit $A ⊆ 𝒯_1 × ⋯ × 𝒯_n$.

Pour tout $i∈⟦1, n⟧$, pour tout $n$-uplet $a ≝ (a_1, ⋯, a_n)∈ A$, on pose

\[𝜋_i(a) ≝ a_i\]

(la projection sur la $i$-ème composante des $n$-uplets de $A$)

Montrons que

\[𝒯 ∋ 𝒜 ≝ \Big(\underbrace{\sup_{a∈A} 𝜋_1(a)}_{∈ 𝒯_1},\, \, ⋯, \, \, \underbrace{\sup_{a∈A} 𝜋_n(a)}_{∈ 𝒯_n}\Big) = \sup_𝒯 A\]

(en utilisant le fait que les $𝒯_i$ sont des treillis complets)

En effet :

  • $𝒜$ majore $A$ :

    Pour tout $a ≝ (a_1, ⋯, a_n)∈ A$, pout tout $i∈⟦1, n⟧$,

    \[a_i ≤ \sup_{a∈A} 𝜋_i(a)\]

    Donc $a ≤ 𝒜$ pour l’ordre produit.

  • $𝒜$ est le plus petit des majorants :

    Pour tout majorant $m ≝ (m_1, ⋯, m_n)$ de $A$, pout tout $i∈⟦1, n⟧$,

    \[\begin{align*} &∀a ∈ A,\, \, a ≤ m \\ ⟹&∀a ∈ A,\, \, 𝜋_i(a) ≤ m_i \\ ⟹&\, \, \sup_{a∈A} 𝜋_i(a) ≤ m_i \end{align*}\]

    Donc $𝒜 ≤ m$ pour l’ordre produit.

En utilisant le lemme avec $𝒯_1 = ⋯ = 𝒯_n = {\cal I}$, on conclut que

${\cal I}^n$ est un trellis complet.

Q 3

On applique le théorème de Knaster-Tarski à la fonction

\[F' ≝ \begin{cases} {\cal I}^n ⟶ {\cal I}^n \\ η\mapsto η_0 ∨ F(η) \end{cases}\]

Notons que

  • ${\cal I}^n$ est un trellis complet, d’après Q2.
  • $F’$ est bien à valeurs dans ${\cal I}^n$, puisque $F$ l’est, $𝜂_0∈{\cal I}^n$, et ${\cal I}^n$ est un trellis.
  • $F’$ est bien monotone, puisque $F$ l’est.

Montrons que son plus petit point fixe $lfp(F’)$ :

  1. est un point fixe de $F$ :

    En effet :

    $lfp(F’) = F’(lfp(F’)) ≝ 𝜂_0 ∨ F(lfp(F’))$, donc $lfp(F’)≥F(lfp(F’))$, et comme $F$ est inflationnaire, il vient que

    \[lfp(F') = F(lfp(F'))\]

  2. est plus grand que $𝜂_0$ :

    En effet : cela résulte de

    \[𝜂_0 ≤ 𝜂_0 ∨ F(lfp(F')) = F'(lfp(F')) = lfp(F')\]

  3. est le plus petit point fixe de $F$ supérieur à $𝜂_0$.

    En effet : Soit $𝜂$ un point fixe de $F$ supérieur à $𝜂_0$.

    Comme

    \[\begin{align*} 𝜂 &= F(𝜂) \\ &= 𝜂_0 ∨ F(𝜂) &&\text{car $𝜂_0 ≤ 𝜂 = F(𝜂)$} \\ &= F'(𝜂) \end{align*}\]

    $𝜂$ est un point fixe de $F’(𝜂)$, et donc par définition de $lfp(F’)$ :

    \[lfp(F') ≤ 𝜂\]

Donc $F$ a bien un plus petit point fixe supérieur à $𝜂_0$.

Q 4

NB : On supposera qu’à chaque fois que, dans l’énoncé, il est noté que

\[Q⟦e⟧_η ≝ k ∈ ℤ\]

(pour une expression $e$ et un environnement quotient $𝜂$) cela signfie, par convention, que :

\[Q⟦e⟧_η = (k-1, k+1)\]

On adoptera aussi cette convention.

$F_{e,c} : {\cal I}^n ⟶ {\cal I}^n$ est monotone

En effet :

Si $𝜂, 𝜂’∈{\cal I}^n$ sont tels que $𝜂≤𝜂’$.

  • Cas 1 : Si $Q⟦e⟧η, Q⟦e⟧{η’} ∈ \lbrace ⊥, 0 \rbrace$

    alors \(F_{e,c}(𝜂) = 𝜂 ≤ 𝜂' = F_{e,c}(𝜂')\)

  • Cas 2 : Si $Q⟦e⟧η, Q⟦e⟧{η’} ∉ \lbrace ⊥, 0 \rbrace$

    alors

    • $F_{e,c}(𝜂) = 𝜂∨Q⟦c⟧_𝜂$

    • $F_{e,c}(𝜂’) = 𝜂’∨Q⟦c⟧_{𝜂’}$

    Or :

    • $𝜂≤𝜂’$ par hypothèse

    • \(Q⟦c⟧_{𝜂} ≤ Q⟦c⟧_{𝜂'}\) par monotonie de $Q⟦c⟧_\bullet$

    Donc l’ensemble des majorants de \(\lbrace 𝜂', Q⟦c⟧_{𝜂'}\rbrace\) est inclus dans l’ensemble des majorants de $\lbrace 𝜂, Q⟦c⟧_{𝜂}\rbrace$, et comme la borne sup est le plus petit d’entre eux :

    \[F_{e,c}(𝜂) = 𝜂∨Q⟦c⟧_𝜂 ≤ 𝜂'∨Q⟦c⟧_{𝜂'} = F_{e,c}(𝜂')\]

    • Cas 3 : Si \(Q⟦e⟧_{𝜂} ∈ \lbrace ⊥, 0 \rbrace ∌ Q⟦e⟧_{𝜂'}\)

      alors

      • $F_{e,c}(𝜂) = 𝜂$

      • $F_{e,c}(𝜂’) = 𝜂’∨Q⟦c⟧_{𝜂’}$

      Or :

      • $F_{e,c}(𝜂) = 𝜂≤𝜂’$ par hypothèse

      • \[𝜂'≤𝜂'∨Q⟦c⟧_{𝜂'} = F_{e,c}(𝜂')\]

      Donc par transitivité :

      \[F_{e,c}(𝜂) = 𝜂 ≤ 𝜂'∨Q⟦c⟧_{𝜂'} = F_{e,c}(𝜂')\]

    • Cas 4 : Si \(Q⟦e⟧_{𝜂} ∉ \lbrace ⊥, 0 \rbrace ∋ Q⟦e⟧_{𝜂'}\)

      • Sous-Cas 1 : Si $Q⟦e⟧_{𝜂’} = \bot$

        alors \(Q⟦e⟧_{𝜂} ≤ Q⟦e⟧_{𝜂'} = \bot\) par monotonie, et

        \[Q⟦e⟧_{𝜂} = \bot\]

        ce qui est absurde (par hypothèse).

      • Sous-Cas 2 : Si $Q⟦e⟧_{𝜂’} = 0$

        alors \(Q⟦e⟧_{𝜂} ≤ Q⟦e⟧_{𝜂'} = 0\) par monotonie, d’où

        • $Q⟦e⟧_{𝜂} = 0$

        OU

        • $Q⟦e⟧_{𝜂} = \bot$

        ce qui est absurde (par hypothèse).

      Donc ce cas ne se présente pas.

Dans tous les cas :

\[F_{e,c}(𝜂) ≤ F_{e,c}(𝜂')\]

et le résultat est acquis.

$F_{e,c} : {\cal I}^n ⟶ {\cal I}^n$ est inflationnaire.

Soit $𝜂 ∈{\cal I}^n$.

  • Cas 1 : Si $Q⟦e⟧_η ∈ \lbrace ⊥, 0 \rbrace$

    alors $𝜂 ≤ 𝜂 = F_{e,c}(𝜂)$ par réflexivité.

  • Cas 2 : Si $Q⟦e⟧_η ∉ \lbrace ⊥, 0 \rbrace$

    alors \(𝜂 ≤ 𝜂∨Q⟦c⟧_𝜂 = F_{e,c}(𝜂)\) car la borne sup est un majorant.

Dans tous les cas :

\[𝜂 ≤ F_{e,c}(𝜂)\]

et le résultat est acquis.

Q 5

Si $F$ une fonction inflationnaire d’un treillis complet $L$ dans lui-même, et si $η ≤ η’$, alors

\[lfp_η(F) ≤ lfp_{𝜂'}(F)\]

En effet :

Il suffit de constater que l’ensemble $FP_{𝜂’}$ des points fixes supérieurs à $𝜂’$ est, par transitivité, inclus dans l’ensemble $FP_{𝜂}$ des points fixes supérieurs à $𝜂$.

Comme $lfp_η(F)$ minore $FP_{𝜂} \supset FP_{𝜂’}$, $lfp_η(F)$ est un minorant de $FP_{𝜂’}$, et

\[lfp_η(F) ≤ lfp_{𝜂'}(F)\]

puisque $lfp_{𝜂’}(F)$ est le plus grand des minorants de $FP_{𝜂’}$.

Q 6

La fonction $+ : {\cal I} × {\cal I} ⟶ {\cal I}$ est Scott-continue.

  1. Elle est monotone :

    Si $(u, u’), (v, v’)∈{\cal I}^2$ sont tels que $(u, u’) ≤ (v, v’)$ :

    • Cas 1 : Si $u = \bot$ ou $u’ = \bot$,

      alors $u+ u’ = \bot ≤ v+v’$

    • Cas 1 : Si $v = \bot$ ou $v’ = \bot$,

      alors comme $u ≤ v$ et $u’ ≤ v’$ : il vient que $u = \bot$ ou $u’ = \bot$, et on se ramène au cas précédent.

    • Cas 3 : Si $(u, u’) ≝ ((a,b), (a’,b’)), (v, v’) ≝ ((c,d), (c’,d’))$ (où $a, a’, b, b’, c, c’, d, d’ ∈ ℤ∪\lbrace ±∞ \rbrace$),

      alors

      • $a≥c$ et $a’≥c’$

        • donc $a+a’≥c+c’$

      • $b≤ d$ et $b’≤ d’$

        • donc $b+b’≤d+d’$

      d’où $u+ u’ = (a+a’, b+b’)≤ (c+c’, d+d’) = v+v’$

2.

Pour toute famille dirigée \((v_i, w_i)_{i∈I}\) de couples d’éléments de ${\cal I}$, \(\sup_{i∈I} (v_i + w_i) = (\sup_{i∈I} v_i) + (\sup_{i∈I} w_i)\).

Soit $(v_i, w_i)_{i∈I}$ une telle famille dirigée.

Notons que l’inégalité

\[\sup_{i∈I} (v_i + w_i) ≤ (\sup_{i∈I} v_i) + (\sup_{i∈I} w_i)\]

est acquise par monotonie de $+$ et puisque :

\[\begin{align*} &∀i∈I, v_i + w_i ≤ (\sup_{i∈I} v_i) + (\sup_{i∈I} w_i) &&\text{(monotonie de $+$)}\\ ⟺& \, \, \sup_{i∈I} (v_i + w_i) ≤ (\sup_{i∈I} v_i) + (\sup_{i∈I} w_i) \end{align*}\]

Montrons l’autre inégalité.

  • Cas 1 : $∀i∈I, v_i = \bot$ ou $∀i∈I, w_i = \bot$ :

    alors $\sup_{i∈I} v_i = \bot$ ou $\sup_{i∈I} w_i = \bot$, et on a bien

    \[\sup_{i∈I} (v_i + w_i) ≥ \bot = (\sup_{i∈I} v_i) + (\sup_{i∈I} w_i)\]

  • Cas 2 : $∃i∈I, v_i ≠ \bot$ et $∃j∈I, w_j ≠ \bot$ :

    alors en écrivant les $v_i ≠\bot$ (resp. $w_i≠\bot$) sous la forme $(a_i, b_i)$ (resp. $(c_i, d_i)$), et en utilisant le lemme de l’énoncé :

    • \[\sup_{i∈I} v_i = (\underbrace{\inf_{i∈I,v_i ≠⊥} a_i}_{≝ 𝛼}, \, \, \underbrace{\sup_{i∈I,v_i ≠⊥} b_i}_{≝ 𝛽})\]
    • \[\sup_{i∈I} w_i = (\underbrace{\inf_{i∈I,w_i ≠⊥} c_i}_{≝ 𝛾},\, \, \underbrace{\sup_{i∈I,w_i ≠⊥} d_i}_{≝ 𝛿})\]

    et

    \[(\sup_{i∈I} v_i) + (\sup_{i∈I} w_i) = (𝛼+𝛾, 𝛽+𝛿)\]

    Par ailleurs, comme la famille est dirigée : $∀i,j ∈I, ∃k∈I;$

    \[\begin{cases} (v_k, w_k) ≥ (v_i, w_i) ⟺ v_k ≥ v_i ∧ w_k ≥ w_i\\ (v_k, w_k) ≥ (v_j, w_j) ⟺ v_k ≥ v_j ∧ w_k ≥ w_j \end{cases}\]

    donc $∀i,j ∈I, ∃k∈I;$

    \[(v_k, w_k) ≥ (v_i, w_j)\]

    donc par monotonie de $+$ : $∀i,j ∈I, ∃k∈I;$

    \[\sup_{l∈I} (v_l + w_l) ≥ v_k + w_k ≥ v_i + w_j\]

    et $∀i, j∈I; v_i ≝ (a_i, b_i) ≠ \bot ∧ w_j ≝ (c_j, d_j) ≠ \bot$,

    \[\sup_{l∈I} (v_l + w_l) ≥ v_i + w_j = (a_i+c_j, b_i+d_j) ≥ (𝛼+𝛾, b_i+d_j)\]

    Il vient alors que $∀i∈I; v_i ≝ (a_i, b_i) ≠ \bot$,

    \[\sup_{l∈I} (v_l + w_l) ≥ (𝛼+𝛾, b_i +𝛿)\]

    et enfin :

    \[\sup_{l∈I} (v_l + w_l) ≥ (𝛼+𝛾, 𝛽 +𝛿) = (\sup_{i∈I} v_i) + (\sup_{i∈I} w_i)\]

Donc $+$ est bien Scott-continue.

Q 7

La fonction $- : {\cal I} ⟶ {\cal I}$ est Scott-continue.

  1. Elle est monotone :

    Si $u, v ∈{\cal I}$ sont tels que $u ≤ v$ :

    • Cas 1 : Si $u = \bot$,

      alors clairement $-u = \bot ≤ -v$

    • Cas 1 : Si $v = \bot$,

      alors comme $u ≤ v$ : il vient que $u = \bot$ et on se ramène au cas précédent.

    • Cas 3 : Si $u ≝ (a,b), v ≝ (c,d)$ (où $a, b, c, d ∈ ℤ∪\lbrace ±∞ \rbrace$),

      alors

      • $a≥c$

        • donc $-a≤-c$

      • $b≤ d$

        • donc $-d≤-b$

      d’où $-u = (-b, -a)≤ (-d, -c) = -v$

2.

Pour toute famille dirigée \((v_i)_{i∈I}\) d’éléments de \({\cal I}$, $-\sup_{i∈I} (v_i) = \sup_{i∈I} (-v_i)\).

Soit $(v_i)_{i∈I}$ une telle famille dirigée.

De même qu’auparavant, l’inégalité

\[-\sup_{i∈I} (v_i) ≥ \sup_{i∈I} (-v_i)\]

est acquise par monotonie de $-$.

Montrons l’autre inégalité.

  • Cas 1 : $∀i∈I, v_i = \bot$ :

    alors $\sup_{i∈I} v_i = \bot$, et on a bien

    \[\sup_{i∈I} (-v_i) ≥ \bot = -(\sup_{i∈I} v_i)\]

  • Cas 2 : $∃i∈I, v_i ≠ \bot$ :

    alors en écrivant les $v_i ≠\bot$ sous la forme $(a_i, b_i)$, et en utilisant le lemme de l’énoncé :

    \[\sup_{i∈I} v_i = (\underbrace{\inf_{i∈I,v_i ≠⊥} a_i}_{≝ 𝛼}, \, \, \underbrace{\sup_{i∈I,v_i ≠⊥} b_i}_{≝ 𝛽})\]

    Par ailleurs, $∀i∈I; v_i ≝ (a_i, b_i) ≠ \bot$,

    \[\sup_{l∈I} (- v_l) ≥ -v_i = (-b_i, -a_i) ≥ (-𝛽, -a_i)\]

    donc $∀i∈I; v_i ≝ (a_i, b_i) ≠ \bot$,

    \[\sup_{l∈I} (-v_l) ≥ (-𝛽, -a_i)\]

    d’où l’opposé de la deuxième composante de $\sup_{l∈I} (-v_l)$ est inférieur à $a_i$ pour tout $i∈I$, et est donc inférieur à $𝛼$.

    Il vient alors que la deuxième composante de $\sup_{l∈I} (-v_l)$ est supérieure à $-𝛼$, d’où enfin :

    \[\sup_{l∈I} (-v_l) ≥ (-𝛽, -𝛼) = -(\sup_{i∈I} v_i)\]

Donc $-$ est bien Scott-continue.

Q 8

Si $F : {\cal I}^n ⟶ {\cal I}^n$ est une fonction inflationnaire et Scott-continue, alors la fonction $g_F : {\cal I}^n ⟶ {\cal I}^n, 𝜂 \mapsto lfp_η(F)$ est encore Scott-continue.

  1. La monotonie de $g_F$ a été montrée en Q 5.

2.

Pour toute famille dirigée \((𝜂_{i})_{i∈I}\) d’éléments de ${\cal I}^n$, \(lfp_{\sup_{i∈I} 𝜂_i}(F) = \sup_{i∈I} lfp_{𝜂_{i}}(F)\).

Soit $(𝜂_{i})_{i∈I}$ une telle famille dirigée.

De même qu’auparavant, l’inégalité

\[lfp_{\sup_{i∈I} 𝜂_{i}}(F) ≥ \sup_{i∈I} \, lfp_{𝜂_{i}}(F)\]

est acquise par monotonie de $g_F$.

Montrons l’autre inégalité : $lfp_{\sup_{i∈I} 𝜂_{i}}(F) ≤ \sup_{i∈I} \, lfp_{𝜂_{i}}(F)$.

Méthode 1

\[\begin{align*} \sup_{i∈I} \, lfp_{𝜂_{i}}(F) &= \sup_{i∈I} \,F(lfp_{𝜂_{i}}(F)) \\ &= F(\sup_{i∈I} \,lfp_{𝜂_{i}}(F)) &&\text{(⊛)} \\ &≥ lfp_{\sup_{i∈I} 𝜂_{i}}(F) &&\text{(⊛⊛)} \end{align*}\]

  • $⊛$ : par Scott-continuité de $F$, et car la famille $(lfp_{𝜂_{i}}(F))_{i∈I}$ reste dirigée.

    • en effet : pour tous $i, j∈I$, il existe $k$ tel que $𝜂_{k} ≥ 𝜂_{i}, 𝜂_{j}$. Donc

      \[lfp_{𝜂_{k}}(F) ≥ lfp_{𝜂_{i}}(F), lfp_{𝜂_{j}}(F)\]

      par monotonie de $g_F$.

  • $⊛⊛$ : $\sup_{i∈I} \, lfp_{𝜂_{i}}(F)$ est un point fixe de $F$ (voir l’égalité qui précède) supérieur à tous à les $lfp_{𝜂_{i}}(F)$ (pour tout $i∈I$), donc (par transitivité) à tous les $𝜂_{i}$ (pour tout $i∈I$), donc à $\sup_{i∈I} 𝜂_{i}$. Par définition de $lfp_{\sup_{i∈I} 𝜂_{i}}(F)$, la minoration s’ensuit.

Méthode 2

NB : J’ai trouvé la méthode 1 après avoir rédigé la méthode 2 : je n’ai pu me résoudre à effacer cette dernière, que je laisse ici à titre alternatif.

Lemme : Si $f: {\cal I}^n ⟶ {\cal I}^n$ est Scott-continue : pour tout $𝜂∈ {\cal I}^n$, la fonction $𝜂’ \mapsto 𝜂 ∨ f(𝜂’)$ reste Scott-continue.

En effet :

  • sa monotonie est héritée de celle de $f$

  • toute famille dirigée \((𝜂'_{i})_{i∈I}\) vérifie :

    \[\sup_{i∈I} (𝜂 ∨ f(𝜂'_i)) = 𝜂 ∨ \sup_{i∈I} f(𝜂'_i)\]

    car

    • \[∀i∈I, 𝜂 ∨ f(𝜂'_i) ≤ 𝜂 ∨ \sup_{i∈I} f(𝜂'_i) \\ ⟹ \sup_{i∈I} (𝜂 ∨ f(𝜂'_i)) ≤ 𝜂 ∨ \sup_{i∈I} f(𝜂'_i)\]
    • \[\sup_{i∈I} (𝜂 ∨ f(𝜂'_i)) ≥𝜂$ et $\sup_{i∈I} (𝜂 ∨ f(𝜂'_i)) ≥ \sup_{i∈I} f(𝜂'_i)$, donc $\sup_{i∈I} (𝜂 ∨ f(𝜂'_i)) ≥ 𝜂 ∨ \sup_{i∈I} f(𝜂'_i)\]

      Par suite :

      \[\sup_{i∈I} (𝜂 ∨ f(𝜂'_i)) = 𝜂 ∨ \sup_{i∈I} f(𝜂'_i) \\ = 𝜂 ∨ f(\sup_{i∈I} 𝜂'_i)\]

      par Scott-continuité de $f$, et la Scott continuité de $𝜂’ \mapsto 𝜂 ∨ f(𝜂’)$ est acquise.

On a vu en Q3 que :

\[∀𝜂∈{\cal I}^n, lfp_𝜂(F) = lfp(𝜂' \mapsto 𝜂∨F(𝜂'))\]

Donc en appliquant le théorème du point fixe de Kleene à la fonction Scott-continue $𝜂’ \mapsto (\sup_{i∈I} 𝜂_i)∨F(𝜂’)$ (d’après le lemme):

\[lfp_{\sup_{i∈I} 𝜂_{i}}(F) = \sup_{m∈ℕ} ((\sup_{i∈I} 𝜂_i)∨F)^m(\bot_n)\]

en notant

  • $\bot_n$ le $n$-uplet $(\bot, ⋯, \bot)∈{\cal I}^n$.
  • $(\sup_{i∈I} 𝜂_i)∨F$ la fonction $𝜂’ \mapsto (\sup_{i∈I} 𝜂_i)∨F(𝜂’)$

On veut donc montrer que :

\[\begin{align*} &\, \, lfp_{\sup_{i∈I} 𝜂_{i}}(F) &≤ \sup_{i∈I} \, lfp_{𝜂_{i}}(F) \\ ⟺&\, \, \sup_{m∈ℕ} ((\sup_{i∈I} 𝜂_i)∨F)^m(\bot_n) &≤ \underbrace{\sup_{i∈I} \sup_{m∈ℕ} (𝜂_i∨F)^m(\bot_n)}_{ = \sup_{m∈ℕ} \sup_{i∈I} (𝜂_i∨F)^m(\bot_n)} \end{align*}\]

et il suffit pour cela de montrer que, pour tout entier $m$ :

\[((\sup_{i∈I} 𝜂_i)∨F)^m(\bot_n) ≤ \sup_{i∈I} (𝜂_i∨F)^m(\bot_n)\]

Or : $∀ i_1, ⋯, i_m ∈ I$,

\[\prod\limits_{r=1}^m (𝜂_{i_r}∨F) (\bot_n) = (𝜂_{i_1}∨F) \circ ⋯ \circ (𝜂_{i_m}∨F) (\bot_n) ≤ (𝜂_{k}∨F)^m(\bot_n) \\ ≤ ((\sup_{j∈I} 𝜂_j)∨F)^m(\bot_n)\]

où

  • $𝜂_{i_1}, ⋯, 𝜂_{i_m} ≤ 𝜂_k$ : un tel majorant existe car la famille est dirigée

    • c’est la définition pour $m=2$, et on conclut par une récurrence immédiate pour $m≥2$, en utilisant la transitivité de $≤$.

  • on a utilisé la monotonie (pour l’ordre point à point) de $𝜂’ \mapsto 𝜂’ ∨ F$ (qui découle de la monotonie de $F$) et le fait qu’une composée de fonctions montones reste monotone :

    • $(𝜂_{i_1}∨F) \Big((𝜂_{i_2}∨F) ⋯ \circ (𝜂_{i_m}∨F) (\bot_n)\Big)
      ≤ (𝜂_{k}∨F)\Big((𝜂_{i_2}∨F) \circ ⋯ \circ (𝜂_{i_m}∨F) (\bot_n)\Big)$

    • $(𝜂_{k}∨F) \circ (𝜂_{i_2}∨F)\Big( (𝜂_{i_3}∨F) ⋯ \circ (𝜂_{i_m}∨F) (\bot_n)\Big)
      ≤ (𝜂_{k}∨F) \circ (𝜂_{k}∨F) \Big((𝜂_{i_3}∨F) \circ ⋯ \circ (𝜂_{i_m}∨F) (\bot_n)\Big)$

      • car $(𝜂_{i_2}∨F)\Big( (𝜂_{i_3}∨F) ⋯ \circ (𝜂_{i_m}∨F) (\bot_n)\Big)
        ≤ (𝜂_{k}∨F) \Big((𝜂_{i_3}∨F) \circ ⋯ \circ (𝜂_{i_m}∨F) (\bot_n)\Big)$

        et $(𝜂_{k}∨F)$ est monotone

    • on conclut par une récurrence immédiate, par monotonie de $𝜂’ \mapsto 𝜂’ ∨ F$ et de $(𝜂_{k}∨F)^l$ pour tout $l∈⟦1, m⟧$ (par composition de fonctions monotones).

Or : $∀ i_1, ⋯, i_m ∈ I$,

\[\prod\limits_{r=1}^m (𝜂_{i_r}∨F) (\bot_n) ≤ ((\sup_{j∈I} 𝜂_j)∨F)^m(\bot_n)\]

implique que

\[((\sup_{i∈I} 𝜂_i)∨F)^m(\bot_n) = \prod\limits_{r=1}^m (\sup_{i_r∈I} 𝜂_{i_r}∨F) (\bot_n)≤ \sup_{i∈I} (𝜂_i∨F)^m(\bot_n)\]

car :

  • Pour tous $x, y∈{\cal I}^n$ : $∀i∈I, (𝜂_i∨F)(x) ≤ y ⟹ ((\sup_{i∈I} 𝜂_i)∨F)(x) ≤ y$

    • En effet :

      $∀i∈I, (𝜂_i∨F)(x) = 𝜂_i ∨ F(x) ≤ y$ implique que $y$ majore les $𝜂_i$, donc $y≥\sup_{i∈I} 𝜂_i$, et comme $y ≥ F(x)$, le résultat s’ensuit.

  • on conclut par une récurrence immédiate en utilisant le résultat précédent et la monotonie de $(\sup_{i∈I} 𝜂_i) ∨ F$.

Donc le résultat est acquis.

Q 9

La fonction $filt: {\cal E}’ ⟶ \lbrace ρ ∈ {\cal E}’ \vert ⟦e⟧_ρ ≠ 0 \rbrace$ est Scott-continue.

  1. Elle est monotone :

    Si ${\cal E}, {\cal E}’ ∈ℙ(Env)$ sont tels que ${\cal E} ⊆ {\cal E}’$ : il est clair que

    \[filt({\cal E}) ≝ \lbrace ρ ∈ {\cal E} ⊆ {\cal E}' \vert ⟦e⟧_ρ ≠ 0 \rbrace ⊆ \lbrace ρ ∈ {\cal E}' \vert ⟦e⟧_ρ ≠ 0 \rbrace ≝ filt({\cal E}')\]

2.

Pour toute famille dirigée \(({\cal E}_{i})_{i∈I}\) d’éléments de $ℙ(Env)$,

\[filt({\sup_{i∈I} {\cal E}_i}) = filt(\bigcup\limits_{i∈I} {\cal E}_i) =\sup_{i∈I} filt({\cal E}_i)\]

Soit $(𝜂_{i})_{i∈I}$ une telle famille dirigée.

L’inégalité

\[filt({\sup_{i∈I} {\cal E}_i}) ≥ \sup_{i∈I} filt({\cal E}_i)\]

est acquise par monotonie.

Montrons que :

\[filt({\sup_{i∈I} {\cal E}_i}) = filt(\bigcup\limits_{i∈I} {\cal E}_i) \\ = \lbrace ρ ∈ \bigcup\limits_{i∈I} {\cal E}_i \, \, \vert ⟦e⟧_ρ ≠ 0 \rbrace ≤ \sup_{i∈I} filt({\cal E}_i) \\ = \sup_{i∈I} \lbrace ρ ∈ {\cal E}_i \, \, \vert ⟦e⟧_ρ ≠ 0 \rbrace \\ = \bigcup\limits_{i∈I} \lbrace ρ ∈ {\cal E}_i \, \, \vert ⟦e⟧_ρ ≠ 0 \rbrace\]

C’est clair, car pour tout $ρ ∈ \bigcup\limits_{i∈I} {\cal E}_i$ tel que $⟦e⟧_ρ ≠ 0$, il existe $i∈I$ tel que

\[𝜌∈{\cal E}_i\]

donc

\[𝜌∈\lbrace ρ' ∈ {\cal E}_i \, \, \vert ⟦e⟧_{ρ'} ≠ 0 \rbrace\]

et

\[𝜌∈\bigcup\limits_{j∈I} \lbrace ρ' ∈ {\cal E}_j \, \, \vert ⟦e⟧_{ρ'} ≠ 0 \rbrace\]

Ainsi, on a montré que

\[\lbrace ρ ∈ \bigcup\limits_{i∈I} {\cal E}_i \, \, \vert ⟦e⟧_ρ ≠ 0 \rbrace ⊆ \bigcup\limits_{i∈I} \lbrace ρ ∈ {\cal E}_i \, \, \vert ⟦e⟧_ρ ≠ 0 \rbrace\]

Q 10

On note $f$ la fonction Scott-continue ${\cal E}’ \mapsto {\cal E}∪𝛷_{e,c}({\cal E}’)$.

Lemme : $∀m∈ℕ$,

\[{\cal E}_m = f^{m+1}(∅)\]

En effet : par récurrence sur $m∈ℕ$ :

  • Initialisation : pour $m=0$, le résultat est acquis :

    \[{\cal E}_0 = {\cal E} = {\cal E} ∪ ∅ \\ = {\cal E} ∪ 𝛷_{e,c}(∅) = f(∅)\]

    car $X⟦c⟧∅ = ∅$ (aucun environnement n’est accessible depuis $c$ et $∅$ car il n’existe aucun environnement dans $∅$).

  • Hérédité : pour $m≥1$ :

    \[\begin{align*} {\cal E}_m &= {\cal E} ∪ {\cal E}_m &&\text{(car $({\cal E}_m)_{m∈ℕ}$ croît, et ${\cal E}⊆{\cal E}_m$ ($m≥1$))}\\ &={\cal E} ∪ {\cal E}_{m-1} ∪ X⟦c⟧\lbrace ρ∈{\cal E}_{m-1} \, \, \vert \, \, e⟦𝜌⟧≠0\rbrace) \\ &= f({\cal E}_{m-1}) \\ &= f^{m+1}(∅) &&\text{(par hypothèse de récurrence)} \\ \end{align*}\]

    Le résultat est donc acquis.

Donc

\[\begin{align*} X⟦\textsf{while $e$ do $c$}⟧{\cal E} &= \bigcup\limits_{m≥0} {\cal E}_m \\ &= \bigcup\limits_{m≥1} f^m(∅) &&\text{(d'après le lemme)} \\ &= \bigcup\limits_{m≥0} f^m(∅) \\ &= \sup_{m≥0} f^m(∅) \\ &= lfp(f) &&\text{(par le théorème du point fixe de Kleene ($f$ est Scott-continue))} \\ &= lfp({\cal E}' \mapsto {\cal E}∨𝛷_{e,c}({\cal E}')) \\ &= lfp_{ {\cal E} }(𝛷_{e,c}) &&\text{(d'après Q3)} \end{align*}\]

ce qui conclut.

Q 11

NB : les intervalles considérés sont des intervalles entiers.

Pour tout $v∈{\cal I}$, pour tout $E∈ℙ(ℤ)$,

\[α(E)≤v ⟺ E⊆γ(v)\]

En effet : Soient $v∈{\cal I}$, $E∈ℙ(ℤ)$.

  • Cas 1 : $v=\bot$

    \[α(E)≤v=\bot ⟺ α(E)=\bot \\ ⟺ E = ∅ ⟺ E⊆γ(v)=∅\]

  • Cas 2 : $v ≝ (a, b)$ (où $a,b ∈ ℤ ∪ \lbrace ±∞ \rbrace$ et $a + 1 < b$) :

    • $⟹$ :

      Si $α(E) = (\inf E − 1, \sup E + 1)≤v =(a,b)$, alors

      • $\inf E ≥ a+1$
      • $\sup E ≤ b-1$

      et on a bien

      \[E⊆ [\inf E, \sup E] ⊆ ]a, b[ = γ(v)\]

    • $⟸$ :

      Si $E⊆γ(v) = ]a, b[$ , alors

      • Comme $∀e∈E, e≥a+1$, il vient que $\inf E ≥ a+1$
      • Comme $∀e∈E, e≤b-1$, il vient que $\sup E ≤ b-1$

      et on a bien

      \[α(E) = (\inf E − 1, \sup E + 1)≤v =(a,b)\]

Q 12

Soit $c$ une commande.

On suppose que pour tout environnement quotient $η’$ et tout ensemble ${\cal E}’∈ℙ(Env)$ que $η’$ représente correctement, $Q⟦c⟧{𝜂’}$ représente correctement $X⟦c⟧{\cal E’}$.

Pour tous $𝜂∈{\cal I}^n$ et ${\cal E}∈ℙ(Env)$, si $η$ représente correctement ${\cal E}$, alors $Q⟦\textsf{while } e \textsf{ do } c⟧𝜂$ représente correctement $X⟦\textsf{while } e \textsf{ do } c⟧{\cal E}$.

En effet :

Soit $𝜂∈{\cal I}^n$ représentant correctement ${\cal E}∈ℙ(Env)$, i.e $𝛼(\lbrace ρ(x) \vert ρ ∈ {\cal E} \rbrace) ≤ η(x)$, ce qui équivaut à $\lbrace ρ(x) \vert ρ ∈ {\cal E} \rbrace ⊆ 𝛾(η(x))$ pour toute variable $x$.

Montrons que : pour toute variable $x$,

\[\lbrace ρ(x) \vert ρ ∈ lfp_{\cal E} (Φ_{e,c}) \rbrace ⊆ 𝛾(lfp_η(F_{e,c})(x))\]

Lemme 1 : Soit $X$ est un DCPO pointé, $f: X ⟶ X$ une fonction inflationnaire Scott-continue, $x∈X$ :

\[lfp_x(f) ≝ \sup_{m∈ℕ} f^m(x)\]

$(f^m(x))_m$ est une chaîne, et est donc dirigée.

Posons

\[y ≝ \sup_{m∈ℕ} f^m(x)\]

Alors :

\[\begin{align*} f(y) &= f(\sup_{m∈ℕ} f^m(x)) \\ &= \sup_{m∈ℕ} f^{m+1}(x) &&\text{(par Scott-continuité de $f$)}\\ &= \sup_{m∈ℕ} f^{m}(x) &&\text{(car $f$ est inflationnaire ($f(x)≥x$))} \end{align*}\]

Donc :

\(y = f(y)\) et $y$ est un point fixe.

Montrons que c’est le plus petit point fixe supérieur à $x$ :

Si $z$ est un autre point fixe supérieur à $x$ :

\[\begin{align*} &\, \, x ≤ z \\ ⟹&\, \, f(x) ≤ f(z)=z &&\text{(par monotonie de $f$)}\\ ⟹&\, \, ∀m∈ℕ, f^m(x) ≤ z &&\text{(par une récurrence immédiate)}\\ ⟹&\, \, y ≤ z \end{align*}\]

En appliquant le lemme précédent, il vient que :

  • $lfp_η(F_{e,c}) = \sup_{m∈ℕ}F_{e,c}^m(η)$
  • $lfp_{\cal E}(Φ_{e,c}) = \bigcup\limits_{m≥0} Φ_{e,c}^m({\cal E})$

Scolie 1 : Pour tous environnements quotients $𝜂’, 𝜂’’$ et tous ensembles ${\cal E}’, {\cal E}’‘∈ℙ(Env)$ représentés correctement respectivement par $𝜂’, 𝜂’’$ : $𝜂’ ∨ 𝜂’’$ représente correctement ${\cal E}’ ∪ {\cal E}’’$

En effet :

pour toute variable $x$, il suffit de remarquer que :

\[\begin{cases} \lbrace ρ(x) \vert ρ ∈ {\cal E}' \rbrace ⊆ 𝛾(𝜂'(x)) \\ \lbrace ρ(x) \vert ρ ∈ {\cal E}'' \rbrace ⊆ 𝛾(𝜂''(x)) \end{cases} ⟹ \lbrace ρ(x) \vert ρ ∈ {\cal E}'∪{\cal E}'' \rbrace ⊆ 𝛾(𝜂'(x)) ∪ 𝛾(𝜂''(x)) ⊆ 𝛾((𝜂' ∨ 𝜂'')(x))\]

la dernière inclusion venant du fait que :

  • $𝛾(𝜂’(x)) ⊆ 𝛾((𝜂’ ∨ 𝜂’’)(x))$ et $𝛾(𝜂’‘(x)) ⊆ 𝛾((𝜂’ ∨ 𝜂’’)(x))$ car $𝛾$ est monotone
  • ce qui impique que $𝛾(𝜂’(x)) ∪ 𝛾(𝜂’‘(x)) ⊆ 𝛾((𝜂’ ∨ 𝜂’’)(x))$

Scolie 2 : Pour tout environnement quotient $η’$ et tout ensemble ${\cal E}’∈ℙ(Env)$ que $η’$ représente correctement :

$F_{e,c}(η’)$ représente correctement $Φ_{e,c}({\cal E}’)$

En effet :

  • Cas 1 : Si $Q⟦e⟧η’ =⊥$ ou $Q⟦e⟧η’ = 𝛼(\lbrace 0 \rbrace)$ :

    alors

    • $Φ_{e,c}({\cal E}’) = {\cal E}’ ∪ X⟦c⟧ \lbrace ρ ∈ {\cal E}’ \, \vert \, \, e⟦ρ⟧ ≠ 0 \rbrace$
    • $F_{e,c}(η’) = η’$

    mais comme $Q⟦e⟧η’$ représente correctement $\lbrace ⟦e⟧𝜌 \, \vert \, 𝜌∈{\cal E}’ \rbrace$, il vient que :

    \[\lbrace ⟦e⟧𝜌 \, \vert \, 𝜌∈{\cal E}' \rbrace ⊆ 𝛾(Q⟦e⟧η') ⊆ \lbrace 0 \rbrace\]

    Donc $\lbrace ρ ∈ {\cal E}’ \, \vert \, \, e⟦ρ⟧ ≠ 0 \rbrace = ∅$, et :

    \[X⟦c⟧ \lbrace ρ ∈ {\cal E}' \, \vert \, \, e⟦ρ⟧ ≠ 0 \rbrace = X⟦c⟧∅ = ∅\]

    (cf. l’initialisation du lemme de Q10)

    Par suite :

    \[Φ_{e,c}({\cal E}') = {\cal E}'\]

    et le résultat est acquis (par hypothèse).

  • Cas 2 : Sinon, si $Q⟦e⟧η’ ≠ ⊥$ et $Q⟦e⟧η’ ≠ 𝛼(\lbrace 0 \rbrace)$ :

    alors

    • $Φ_{e,c}({\cal E}’) = {\cal E}’ ∪ X⟦c⟧ \lbrace ρ ∈ {\cal E}’ \, \vert \, \, e⟦ρ⟧ ≠ 0 \rbrace$
    • $F_{e,c}(η’) = η’ ∨ Q⟦c⟧η’$

    et :

    \[\lbrace ⟦e⟧𝜌 \, \vert \, 𝜌∈{\cal E}' \rbrace ⊆ 𝛾(Q⟦e⟧η') ≠ ∅, \lbrace 0 \rbrace\]

    (car $𝛼\circ 𝛾 = id$)

    D’où :

    \[∅≠\lbrace ρ ∈ {\cal E}' \, \vert \, \, e⟦ρ⟧ ≠ 0 \rbrace ⊆ {\cal E}'\]

    et pour toute variable $x$ :

    \[\lbrace ρ(x) \vert ρ ∈ \lbrace ρ ∈ {\cal E}' \, \vert \, \, e⟦ρ⟧ ≠ 0 \rbrace \rbrace ⊆ \lbrace ρ(x) \vert ρ ∈ {\cal E}' \rbrace ⊆ 𝛾(𝜂'(x))\]

    donc $𝜂’$ représente correctement $\lbrace ρ ∈ {\cal E}’ \, \vert \, \, e⟦ρ⟧ ≠ 0 \rbrace$, donc $Q⟦c⟧{𝜂’}$ représente correctement $X⟦c⟧\lbrace ρ ∈ {\cal E}’ \, \vert \, \, e⟦ρ⟧ ≠ 0 \rbrace$ (d’après le résultat admis rappelé au début).

    On conclut avec la scolie 1 : $F_{e,c}(η’)$ représente correctement $Φ_{e,c}({\cal E}’)$.

Lemme 2 : Pour tout $m∈ℕ$, $F_{e,c}^m(η)$ représente correctement $Φ_{e,c}^m({\cal E})$

En effet : par récurrence sur $m∈ℕ$ :

  • Initialisation : pour $m=0$, le résultat est acquis.

  • Hérédité : pour $m≥1$ :

    On utilise la scolie 2 avec $F_{e,c}^{m-1}(η)$ qui, par hypothèse de récurrence, représente correctement $Φ_{e,c}^{m-1}({\cal E})$, pour en déduire que $F_{e,c}^m(η)$ représente correctement $Φ_{e,c}^m({\cal E})$.

On montre ainsi, par une récurrence immédiate avec la scolie 2 et le lemme 2, que :

Pour tout $N∈ℕ$,

$\sup_{0≤m≤N} F_{e,c}^m(η)$ représente correctement $\bigcup\limits_{m=0}^N Φ_{e,c}^m({\cal E})$

Donc pour tout $N∈ℕ$, pour toute variable $x$ :

\[\lbrace ρ(x) \vert ρ ∈ \bigcup\limits_{m=0}^N Φ_{e,c}^m({\cal E}) \rbrace ⊆ 𝛾\bigg(\sup_{0≤m≤N} F_{e,c}^m(η)(x)\bigg) ⊆ 𝛾\bigg(\sup_{m∈ℕ}F_{e,c}^m(η)(x)\bigg) = 𝛾\big(lfp_η(F_{e,c})(x)\big)\]

par monotonie de $𝛾$, et :

$lfp_η(F_{e,c})$ représente correctement $\bigcup\limits_{m=0}^N Φ_{e,c}^m({\cal E})$ pour tout $N∈ℕ$.

Par l’absurde :

Si $lfp_η(F_{e,c})$ ne représentait pas correctement $lfp_{\cal E}(Φ_{e,c}) = \bigcup\limits_{m≥0} Φ_{e,c}^m({\cal E})$ : il existerait une variable $x$ et un environnement (réel) $𝜌∈\bigcup\limits_{m≥0} Φ_{e,c}^m({\cal E})$ tels que $𝜌(x)∈\Big(\lbrace ρ’(x) \vert ρ’ ∈ \bigcup\limits_{m≥0} Φ_{e,c}^m({\cal E}) \rbrace \Big)\big\backslash 𝛾(lfp_η(F_{e,c})(x))$.

Or, il existerait un $N∈ℕ$ tel que $𝜌∈Φ_{e,c}^N({\cal E})⊆\bigcup\limits_{m=0}^N Φ_{e,c}^m({\cal E})$, d’où

\[𝜌(x)∈\Big(\lbrace ρ'(x) \vert ρ' ∈ \bigcup\limits_{m=0}^N Φ_{e,c}^m({\cal E}) \rbrace \Big)\big\backslash 𝛾(lfp_η(F_{e,c})(x))\]

ce qui est absurde, car $\lbrace ρ’(x) \vert ρ’ ∈ \bigcup\limits_{m=0}^N Φ_{e,c}^m({\cal E}) \rbrace ⊆ 𝛾(lfp_η(F_{e,c})(x))$.

Ainsi :

$lfp_η(F_{e,c}) = \sup_{m∈ℕ}F_{e,c}^m(η)$ représente correctement $lfp_{\cal E}(Φ_{e,c}) = \bigcup\limits_{m≥0} Φ_{e,c}^m({\cal E})$.

Q 13

La démonstration se fait par induction structurelle sur la commande (ou : par récurrence sur la structure de la commande).

En Q12, on avait $c’=\textsf{while } e \textsf{ do } c$, et on a utilisé l’hypothèse d’induction, supposée acquise, sur $c$, pour en déduire le résultat pour $c’$.

Q 14 / 15

Pour tous $𝜂∈{\cal I}^n$ et ${\cal E}∈ℙ(Env)$, si $η$ représente correctement ${\cal E}$, alors $Q⟦x:=e⟧𝜂 = η ∨ η[x → Q⟦e⟧η]$ représente correctement $X⟦x:=e⟧{\cal E} = {\cal E}∪\lbrace ρ[x → ⟦e⟧ρ] \, \, \vert \, \, ρ∈{\cal E} \rbrace$.

En effet :

Il suffira, en utilisant la scolie 2 de Q12, de montrer que $η[x \mapsto Q⟦e⟧η]$ représente correctement $\lbrace ρ[x \mapsto ⟦e⟧ρ] \, \, \vert \, \, ρ∈{\cal E} \rbrace$.

i.e pour toute variable $y$,

\[\lbrace ρ'(y) \vert ρ' ∈ \lbrace ρ[x \mapsto ⟦e⟧ρ] \, \, \vert \, \, ρ∈{\cal E} \rbrace \rbrace ⊆ 𝛾\Big(η[x \mapsto Q⟦e⟧η](y)\Big)\]

Soit $y$ une variable.

On sait par ailleurs que $Q⟦e⟧η$ représente correctement $\lbrace ⟦e⟧ρ \, \, \vert \, \, ρ ∈ {\cal E}\rbrace$, i.e :

\[\lbrace ⟦e⟧ρ \, \, \vert \, \, ρ ∈ {\cal E}\rbrace ⊆ 𝛾(Q⟦e⟧η) \hspace{1em}⊛\]

Soit $ρ’ ∈ \lbrace ρ[x \mapsto ⟦e⟧ρ] \, \, \vert \, \, ρ∈{\cal E} \rbrace$.

Montrons que \(ρ'(y)∈𝛾\Big(η[x \mapsto Q⟦e⟧η](y)\Big)\)

  • Cas 1 : Si $y≠x$

    alors

    \[𝜌'(y)∈ \lbrace ρ(y) \, \, \vert \, \, ρ∈{\cal E} \rbrace ⊆ 𝛾\big(\underbrace{𝜂(y)}_{= η[x \mapsto Q⟦e⟧η](y)}\big) = 𝛾\Big(η[x \mapsto Q⟦e⟧η](y)\Big)\]

    (car $𝜂$ représente correctement ${\cal E}$).

  • Cas 2 : Si $y=x$

    alors

    \[𝜌'(y) = 𝜌'(x) = ⟦e⟧𝜌' ∈ \lbrace ⟦e⟧ρ \, \, \vert \, \, ρ ∈ {\cal E}\rbrace ⊆ 𝛾(\underbrace{Q⟦e⟧η}_{= η[x \mapsto Q⟦e⟧η](y)})\]

    (d’après $⊛$).

Donc le résultat est acquis.

Q 16

NB : on utilisera les notations usuelles pour dénoter la relation binaire “stricte” $>$ obtenue à partir de $≥$ : $> \, ≝ \, \, ≥ \text{ et } ≠$

Soit $x$ une variable telle que $∅≠𝛾(𝜂(x))⊆ℤ$ (donc si $𝜂(x) ≝(a,b)$ : $a, b ∈ℤ$)

Avec \(\textsf{while } \underbrace{1}_{≝ e} \textsf{ do } \underbrace{x:=x+1}_{≝ c}\) :

comme

\[F_{e,c}(η) ≝ \begin{cases} η \text{ si } Q⟦e⟧η =⊥ \text{ ou } Q⟦e⟧η = 0 \\ η ∨ Q⟦c⟧η \text{ sinon.} \end{cases}\]

ici :

\[\begin{align*} F_{e,c}(η) &= η ∨ Q⟦x:=x+1⟧η \\ &= η ∨ η[x \mapsto Q⟦x+1⟧η] \\ &= η ∨ η[x \mapsto η(x)+(0,2)] \\ \end{align*}\]

Or

\[η[x \mapsto η(x)+(0,2)] > η\]

(pour l’ordre point à point : il y a seulement à remarquer que $η(x)+(0,2) > η(x)$)

donc

\[F_{e,c}(η) = η[x \mapsto η(x)+(0,2)] > η\]

En rétiréant avec $𝜂_1 ≝ F_{e,c}(η)$, on montre de la même manière que :

\[F_{e,c}(η_1) = η_1[x \mapsto η_1(x)+(0,2)] > η_1\]

et par une récurrence immédiate :

\[∀m∈ℕ^\ast, 𝜂_m ≝ F_{e,c}(η_{m-1}) = η_{m-1}[x \mapsto η_{m-1}(x)+(0,2)] > η_{m-1}\]

Donc la suite $(𝜂_m)_{m∈ℕ}$ n’est pas stationnaire, et la procédure décrite ne termine pas.

Q 17

Cette fois :

\[F'_{e,c}(η') = \begin{cases} η' \text{ si } Q⟦e⟧η' =⊥ \text{ ou } Q⟦e⟧η' = 0 \\ η' \nabla Q⟦c⟧η' \text{ sinon.} \end{cases}\]

On remarque que : pour tout environnement quotient $𝜂’$, $F’_{e,c}(𝜂’)≥𝜂’$ (car $η’ \nabla Q⟦c⟧η’ ≥ 𝜂’$).

Donc pour tout $m∈ℕ^\ast$ :

  • Cas 1 : \(𝜂_m = F'_{e,c}(η_{m-1}) = η_{m-1} (\text{ si } Q⟦e⟧{𝜂_{m-1}}∈\lbrace \bot, (-1, 1) \rbrace \text{ ou } Q⟦c⟧{𝜂_{m-1}}≤𝜂_{m-1}\))

OU

  • Cas 2 : \(𝜂_m = F'_{e,c}(η_{m-1}) > η_{m-1}\)

Dans le dernier cas, il existe une variable $x$ telle que $𝜂_m(x)$ est de la forme

  • $(a,b)$ si $𝜂_{m-1}(x) = \bot$
  • $(-∞,b)$ ou $(a, +∞)$ sinon

d’où il existe $i∈⟦0,2⟧$ indices $p_1 > ⋯ > p_i >m$ tels que

\(∀j∈⟦1, i⟧, 𝜂_{p_j}(x)> 𝜂_{p_j-1}(x)\) (si $i≥1$, $𝜂_{p_1}(x)$ vaut alors $(-∞, +∞)$, d’où $(𝜂_q(x))_{q≥p_1}$ est constante de valeur $(-∞, +∞)$)

Donc

la suite $(𝜂_m)_{m∈ℕ}$ ne peut croître strictement qu’un nombre fini de fois.$\hspace{1em}⊛$

(au plus $3n$ fois, pour être précis)

On remarque par ailleurs que

si $∃m∈ℕ; 𝜂_{m+1} = 𝜂_m$, alors $∀p≥m, 𝜂_p = 𝜂_m$ $\hspace{1em}⊛⊛$

(car \(𝜂_{m+2} = F'_{e,c}(𝜂_{m+1}) = F'_{e,c}(𝜂_m) = 𝜂_{m+1} = 𝜂_m\), et on conclut par une récurrence immédiate sur $q≥1$ que \(∀q≥1, 𝜂_{m+q} = 𝜂_m\))

Avec $⊛$ et $⊛⊛$, on conclut que donc que la suite croissante $(𝜂_m)_{m∈ℕ}$ est stationnaire, et la procédure décrite termine.

Montrons que $Q⟦c⟧η$ représente toujours correctement $X⟦c⟧{\cal E}$ pour toute commande $c$.

On remarque que, pour tout environnement quotient $𝜂$ et pour toute commande $c$ :

\[𝜂 ∨ Q⟦c⟧η ≤ 𝜂 \nabla Q⟦c⟧η\]

  • en effet : pour toute variable $x$ :

    • Si $Q⟦c⟧η(x)≤𝜂(x)$, alors $(𝜂 \nabla Q⟦c⟧η)(x) = (𝜂 ∨ Q⟦c⟧η)(x) = 𝜂(x)$

    • Sinon :

      • si $𝜂(x) = \bot$ : $(𝜂 \nabla Q⟦c⟧η)(x) = (𝜂 ∨ Q⟦c⟧η)(x) = Q⟦c⟧η(x)$

      • si $𝜂(x) ≝ (a,b), Q⟦c⟧η(x)≝ (c, d)$ (où $a, b, c, d ∈ ℤ∪\lbrace ±∞ \rbrace$) :

        \[(𝜂 ∨ Q⟦c⟧η)(x) = (\min(a, c),\max(b, d))\]

        et en posant

        • $𝛼 ≝ \begin{cases} \min(a, c) \text{ si } \min(a, c)=a
          -∞ \text{ sinon}\end{cases}$
        • $𝛽 ≝ \begin{cases} \max(b, d) \text{ si } \max(b, d)=b
          +∞ \text{ sinon}\end{cases}$
        \[(𝜂 ∨ Q⟦c⟧η)(x) = (\min(a, c),\max(b, d)) ≤ (𝛼, 𝛽) ≝ (𝜂 \nabla Q⟦c⟧η)(x)\]

Il s’ensuit que :

\[F_{e,c} ≤ F'_{e,c}\]

(pour l’ordre point à point)

Il vient que, pour toute commande $c$, $Q⟦c⟧η$

  • est soit resté inchangé

  • a soit augmenté au sens large

    • c’est le cas pour les commandes de la forme $\textsf{while } e \textsf{ do } c’$, car \(F_{e,c'} ≤ F'_{e,c'}\) et par monotonie (pour l’ordre point à point) de la fonction $𝛹_{𝜂’} : f \mapsto lfp_{𝜂’}(f)$ pour tout environnement quotient $𝜂’$

      • en effet: la monotonie de $𝛹_{𝜂’} : f \mapsto lfp_{𝜂’}(f)$ vient du lemme 1 de Q12 :

        si $f≤g$,

        \[lfp_{𝜂'}(f) = \sup_{m∈ℕ} \underbrace{f^m(𝜂')}_{≤ g^m(𝜂')} ≤ \sup_{m∈ℕ} g^m(𝜂') = lfp_{𝜂'}(g)\]

Scolie : Si $η’’$ et $𝜂’$ sont des environnements tels que

  • $𝜂’≤𝜂’’$
  • $𝜂’$ représente correctement un ensemble ${\cal E}’$ d’environnements (réels)

alors $𝜂’’$ représente correctement ${\cal E}’$.

En effet :

pour toute variable $x$, il suffit de remarquer que :

\[\begin{cases} \lbrace ρ(x) \vert ρ ∈ {\cal E}' \rbrace ⊆ 𝛾(𝜂'(x)) \\ 𝛾(𝜂'(x)) ⊆ 𝛾(𝜂''(x)) \text{ (par monotonie de $𝛾$)} \end{cases} ⟹ \lbrace ρ(x) \vert ρ ∈ {\cal E}' \rbrace ⊆ 𝛾(𝜂''(x))\]

Donc d’après la scolie :

$Q⟦c⟧η$ représente toujours correctement $X⟦c⟧{\cal E}$ pour toute commande $c$.

Leave a comment