DM : Programmation 1

DM Programmation I

Énoncé

Younesse Kaddar

Q 1

Soit $u, v \in I$ .

Cas 1 : $u = ⊥$ et $v = ⊥$

clairement : $u \lor v = ⊥$
Cas 2 : $u = ⊥$ et $v \neq ⊥$

clairement : $u \lor v = v$
Cas 3 : $u ≝ (a, b) \neq ⊥$ et $v ≝ (c, d) \neq ⊥$ (où $a, b, c, d \in ℤ \cup {\pm \infty}$ ) :

Alors $u \lor 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 \leq (e, f) ⟹ a, c \leq e ⟹ min (a, c) \leq e$
  - $u, v \leq (e, f) ⟹ b, d \leq f ⟹ max (b, d) \leq f$
Donc $(min (a, c), max (b, d)) \leq (e, f)$ , et $(min (a, c), max (b, d))$ est bien le plus petit des majorants.

Q 2

a).

$I$ est un trellis complet, donc un DCPO, d’où

$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} \times \dots \times 𝒯_{n}$ de treillis complets reste un treillis complet.

Soit $A \subseteq 𝒯_{1} \times \dots \times 𝒯_{n}$ .

Pour tout $i \in ⟦ 1, n ⟧$ , pour tout $n$ -uplet $a ≝ (a_{1}, \dots, a_{n}) \in A$ , on pose

𝜋_{i} (a) ≝ a_{i}

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

Montrons que

𝒯 ∋ 𝒜 ≝ (\underset{\in 𝒯_{1}}{\underset{⏟}{sup_{a \in A} 𝜋_{1} (a)}}, \dots, \underset{\in 𝒯_{n}}{\underset{⏟}{sup_{a \in A} 𝜋_{n} (a)}}) = sup_{𝒯} A

(en utilisant le fait que les $𝒯_{i}$ sont des treillis complets)

En effet :

$𝒜$ majore $A$ :

Pour tout $a ≝ (a_{1}, \dots, a_{n}) \in A$ , pout tout $i \in ⟦ 1, n ⟧$ ,
$a_{i} \leq sup_{a \in A} 𝜋_{i} (a)$
Donc $a \leq 𝒜$ pour l’ordre produit.
$𝒜$ est le plus petit des majorants :

Pour tout majorant $m ≝ (m_{1}, \dots, m_{n})$ de $A$ , pout tout $i \in ⟦ 1, n ⟧$ ,
$\begin{aligned} \forall a \in A, a \leq m \\ ⟹ & \forall a \in A, 𝜋_{i} (a) \leq m_{i} \\ ⟹ & sup_{a \in A} 𝜋_{i} (a) \leq m_{i} \end{aligned}$
Donc $𝒜 \leq m$ pour l’ordre produit.

En utilisant le lemme avec $𝒯_{1} = \dots = 𝒯_{n} = I$ , on conclut que

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

Q 3

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

F^{'} ≝ {\begin{cases} I^{n} ⟶ I^{n} \\ η \mapsto η_{0} \lor F (η) \end{cases}

Notons que

$I^{n}$ est un trellis complet, d’après Q2.
$F^{'}$ est bien à valeurs dans $I^{n}$ , puisque $F$ l’est, $𝜂_{0} \in I^{n}$ , et $I^{n}$ est un trellis.
$F^{'}$ est bien monotone, puisque $F$ l’est.

Montrons que son plus petit point fixe $l f p (F^{'})$ :

est un point fixe de $F$ :

En effet :

$l f p (F^{'}) = F^{'} (l f p (F^{'})) ≝ 𝜂_{0} \lor F (l f p (F^{'}))$ , donc $l f p (F^{'}) \geq F (l f p (F^{'}))$ , et comme $F$ est inflationnaire, il vient que
$l f p (F^{'}) = F (l f p (F^{'}))$
est plus grand que $𝜂_{0}$ :

En effet : cela résulte de
$𝜂_{0} \leq 𝜂_{0} \lor F (l f p (F^{'})) = F^{'} (l f p (F^{'})) = l f p (F^{'})$
est le plus petit point fixe de $F$ supérieur à $𝜂_{0}$ .

En effet : Soit $𝜂$ un point fixe de $F$ supérieur à $𝜂_{0}$ .

Comme
$\begin{aligned} 𝜂 & = F (𝜂) \\ = 𝜂_{0} \lor F (𝜂) & car 𝜂_{0} \leq 𝜂 = F (𝜂) \\ = F^{'} (𝜂) \end{aligned}$
$𝜂$ est un point fixe de $F^{'} (𝜂)$ , et donc par définition de $l f p (F^{'})$ :
$l f p (F^{'}) \leq 𝜂$

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 \in ℤ

(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} : I^{n} ⟶ I^{n}$ est monotone

En effet :

Si $𝜂, 𝜂^{'} \in I^{n}$ sont tels que $𝜂 \leq 𝜂^{'}$ .

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

alors $F_{e, c} (𝜂) = 𝜂 \leq 𝜂^{'} = F_{e, c} (𝜂^{'})$
Cas 2 : Si $Q⟦e⟧η, Q⟦e⟧{η’} ∉ \lbrace ⊥, 0 \rbrace$

alors
- $F_{e, c} (𝜂) = 𝜂 \lor Q ⟦ c ⟧_{𝜂}$
- $F_{e, c} (𝜂^{'}) = 𝜂^{'} \lor Q ⟦ c ⟧_{𝜂^{'}}$
Or :
- $𝜂 \leq 𝜂^{'}$ par hypothèse
- $Q ⟦ c ⟧_{𝜂} \leq Q ⟦ c ⟧_{𝜂^{'}}$ par monotonie de $Q ⟦ c ⟧_{∙}$
Donc l’ensemble des majorants de ${𝜂^{'}, Q ⟦ c ⟧_{𝜂^{'}}}$ est inclus dans l’ensemble des majorants de ${𝜂, Q ⟦ c ⟧_{𝜂}}$ , et comme la borne sup est le plus petit d’entre eux :
$F_{e, c} (𝜂) = 𝜂 \lor Q ⟦ c ⟧_{𝜂} \leq 𝜂^{'} \lor Q ⟦ c ⟧_{𝜂^{'}} = F_{e, c} (𝜂^{'})$
- Cas 3 : Si $Q ⟦ e ⟧_{𝜂} \in {⊥, 0} ∌ Q ⟦ e ⟧_{𝜂^{'}}$
  
  alors
  - $F_{e, c} (𝜂) = 𝜂$
  - $F_{e, c} (𝜂^{'}) = 𝜂^{'} \lor Q ⟦ c ⟧_{𝜂^{'}}$
  Or :
  - $F_{e, c} (𝜂) = 𝜂 \leq 𝜂^{'}$ par hypothèse
  - $𝜂^{'} \leq 𝜂^{'} \lor Q ⟦ c ⟧_{𝜂^{'}} = F_{e, c} (𝜂^{'})$
  Donc par transitivité :
  $F_{e, c} (𝜂) = 𝜂 \leq 𝜂^{'} \lor Q ⟦ c ⟧_{𝜂^{'}} = F_{e, c} (𝜂^{'})$
- Cas 4 : Si $Q ⟦ e ⟧_{𝜂} \notin {⊥, 0} ∋ Q ⟦ e ⟧_{𝜂^{'}}$
  - Sous-Cas 1 : Si $Q ⟦ e ⟧_{𝜂^{'}} = ⊥$
    
    alors $Q ⟦ e ⟧_{𝜂} \leq Q ⟦ e ⟧_{𝜂^{'}} = ⊥$ par monotonie, et
    $Q ⟦ e ⟧_{𝜂} = ⊥$
    ce qui est absurde (par hypothèse).
  - Sous-Cas 2 : Si $Q ⟦ e ⟧_{𝜂^{'}} = 0$
    
    alors $Q ⟦ e ⟧_{𝜂} \leq Q ⟦ e ⟧_{𝜂^{'}} = 0$ par monotonie, d’où
    - $Q ⟦ e ⟧_{𝜂} = 0$
    OU
    - $Q ⟦ e ⟧_{𝜂} = ⊥$
    ce qui est absurde (par hypothèse).
  Donc ce cas ne se présente pas.

Dans tous les cas :

F_{e, c} (𝜂) \leq F_{e, c} (𝜂^{'})

et le résultat est acquis.

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

Soit $𝜂 \in I^{n}$ .

Cas 1 : Si $Q ⟦ e ⟧_{η} \in {⊥, 0}$

alors $𝜂 \leq 𝜂 = F_{e, c} (𝜂)$ par réflexivité.
Cas 2 : Si $Q ⟦ e ⟧_{η} \notin {⊥, 0}$

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

Dans tous les cas :

𝜂 \leq 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 $η \leq η^{'}$ , alors
$l f p_{η} (F) \leq l f p_{𝜂^{'}} (F)$

En effet :

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

Comme $l f p_{η} (F)$ minore $F P_{𝜂} \supset F P_{𝜂^{'}}$ , $l f p_{η} (F)$ est un minorant de $F P_{𝜂^{'}}$ , et

l f p_{η} (F) \leq l f p_{𝜂^{'}} (F)

puisque $l f p_{𝜂^{'}} (F)$ est le plus grand des minorants de $F P_{𝜂^{'}}$ .

Q 6

La fonction $+ : I \times I ⟶ I$ est Scott-continue.

Elle est monotone :

Si $(u, u^{'}), (v, v^{'}) \in I^{2}$ sont tels que $(u, u^{'}) \leq (v, v^{'})$ :
- Cas 1 : Si $u = ⊥$ ou $u^{'} = ⊥$ ,
  
  alors $u + u^{'} = ⊥ \leq v + v^{'}$
- Cas 1 : Si $v = ⊥$ ou $v^{'} = ⊥$ ,
  
  alors comme $u \leq v$ et $u^{'} \leq v^{'}$ : il vient que $u = ⊥$ ou $u^{'} = ⊥$ , 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^{'} \in ℤ \cup {\pm \infty}$ ),
  
  alors
  - $a \geq c$ et $a^{'} \geq c^{'}$
    - donc $a + a^{'} \geq c + c^{'}$
  - $b \leq d$ et $b^{'} \leq d^{'}$
    - donc $b + b^{'} \leq d + d^{'}$
  d’où $u + u^{'} = (a + a^{'}, b + b^{'}) \leq (c + c^{'}, d + d^{'}) = v + v^{'}$

Pour toute famille dirigée $(v_{i}, w_{i})_{i \in I}$ de couples d’éléments de $I$ , $sup_{i \in I} (v_{i} + w_{i}) = (sup_{i \in I} v_{i}) + (sup_{i \in I} w_{i})$ .

Soit $(v_{i}, w_{i})_{i \in I}$ une telle famille dirigée.

Notons que l’inégalité

sup_{i \in I} (v_{i} + w_{i}) \leq (sup_{i \in I} v_{i}) + (sup_{i \in I} w_{i})

est acquise par monotonie de $+$ et puisque :

\begin{aligned} \forall i \in I, v_{i} + w_{i} \leq (sup_{i \in I} v_{i}) + (sup_{i \in I} w_{i}) & (monotonie de +) \\ ⟺ & sup_{i \in I} (v_{i} + w_{i}) \leq (sup_{i \in I} v_{i}) + (sup_{i \in I} w_{i}) \end{aligned}

Montrons l’autre inégalité.

Cas 1 : $\forall i \in I, v_{i} = ⊥$ ou $\forall i \in I, w_{i} = ⊥$ :

alors $sup_{i \in I} v_{i} = ⊥$ ou $sup_{i \in I} w_{i} = ⊥$ , et on a bien
$sup_{i \in I} (v_{i} + w_{i}) \geq ⊥ = (sup_{i \in I} v_{i}) + (sup_{i \in I} w_{i})$
Cas 2 : $\exists i \in I, v_{i} \neq ⊥$ et $\exists j \in I, w_{j} \neq ⊥$ :

alors en écrivant les $v_{i} \neq ⊥$ (resp. $w_{i} \neq ⊥$ ) sous la forme $(a_{i}, b_{i})$ (resp. $(c_{i}, d_{i})$ ), et en utilisant le lemme de l’énoncé :
- $sup_{i \in I} v_{i} = (\underset{≝ 𝛼}{\underset{⏟}{inf_{i \in I, v_{i} \neq⊥} a_{i}}}, \underset{≝ 𝛽}{\underset{⏟}{sup_{i \in I, v_{i} \neq⊥} b_{i}}})$
- $sup_{i \in I} w_{i} = (\underset{≝ 𝛾}{\underset{⏟}{inf_{i \in I, w_{i} \neq⊥} c_{i}}}, \underset{≝ 𝛿}{\underset{⏟}{sup_{i \in I, w_{i} \neq⊥} d_{i}}})$
et
$(sup_{i \in I} v_{i}) + (sup_{i \in I} w_{i}) = (𝛼 + 𝛾, 𝛽 + 𝛿)$
Par ailleurs, comme la famille est dirigée : $\forall i, j \in I, \exists k \in I;$
${\begin{cases} (v_{k}, w_{k}) \geq (v_{i}, w_{i}) ⟺ v_{k} \geq v_{i} \land w_{k} \geq w_{i} \\ (v_{k}, w_{k}) \geq (v_{j}, w_{j}) ⟺ v_{k} \geq v_{j} \land w_{k} \geq w_{j} \end{cases}$
donc $\forall i, j \in I, \exists k \in I;$
$(v_{k}, w_{k}) \geq (v_{i}, w_{j})$
donc par monotonie de $+$ : $\forall i, j \in I, \exists k \in I;$
$sup_{l \in I} (v_{l} + w_{l}) \geq v_{k} + w_{k} \geq v_{i} + w_{j}$
et $\forall i, j \in I; v_{i} ≝ (a_{i}, b_{i}) \neq ⊥ \land w_{j} ≝ (c_{j}, d_{j}) \neq ⊥$ ,
$sup_{l \in I} (v_{l} + w_{l}) \geq v_{i} + w_{j} = (a_{i} + c_{j}, b_{i} + d_{j}) \geq (𝛼 + 𝛾, b_{i} + d_{j})$
Il vient alors que $\forall i \in I; v_{i} ≝ (a_{i}, b_{i}) \neq ⊥$ ,
$sup_{l \in I} (v_{l} + w_{l}) \geq (𝛼 + 𝛾, b_{i} + 𝛿)$
et enfin :
$sup_{l \in I} (v_{l} + w_{l}) \geq (𝛼 + 𝛾, 𝛽 + 𝛿) = (sup_{i \in I} v_{i}) + (sup_{i \in I} w_{i})$

Donc $+$ est bien Scott-continue.

Q 7

La fonction $- : I ⟶ I$ est Scott-continue.

Elle est monotone :

Si $u, v \in I$ sont tels que $u \leq v$ :
- Cas 1 : Si $u = ⊥$ ,
  
  alors clairement $- u = ⊥ \leq - v$
- Cas 1 : Si $v = ⊥$ ,
  
  alors comme $u \leq v$ : il vient que $u = ⊥$ et on se ramène au cas précédent.
- Cas 3 : Si $u ≝ (a, b), v ≝ (c, d)$ (où $a, b, c, d \in ℤ \cup {\pm \infty}$ ),
  
  alors
  - $a \geq c$
    - donc $- a \leq - c$
  - $b \leq d$
    - donc $- d \leq - b$
  d’où $- u = (- b, - a) \leq (- d, - c) = - v$

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

Soit $(v_{i})_{i \in I}$ une telle famille dirigée.

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

- sup_{i \in I} (v_{i}) \geq sup_{i \in I} (- v_{i})

est acquise par monotonie de $-$ .

Montrons l’autre inégalité.

Cas 1 : $\forall i \in I, v_{i} = ⊥$ :

alors $sup_{i \in I} v_{i} = ⊥$ , et on a bien
$sup_{i \in I} (- v_{i}) \geq ⊥ = - (sup_{i \in I} v_{i})$
Cas 2 : $\exists i \in I, v_{i} \neq ⊥$ :

alors en écrivant les $v_{i} \neq ⊥$ sous la forme $(a_{i}, b_{i})$ , et en utilisant le lemme de l’énoncé :
$sup_{i \in I} v_{i} = (\underset{≝ 𝛼}{\underset{⏟}{inf_{i \in I, v_{i} \neq⊥} a_{i}}}, \underset{≝ 𝛽}{\underset{⏟}{sup_{i \in I, v_{i} \neq⊥} b_{i}}})$
Par ailleurs, $\forall i \in I; v_{i} ≝ (a_{i}, b_{i}) \neq ⊥$ ,
$sup_{l \in I} (- v_{l}) \geq - v_{i} = (- b_{i}, - a_{i}) \geq (- 𝛽, - a_{i})$
donc $\forall i \in I; v_{i} ≝ (a_{i}, b_{i}) \neq ⊥$ ,
$sup_{l \in I} (- v_{l}) \geq (- 𝛽, - a_{i})$
d’où l’opposé de la deuxième composante de $sup_{l \in I} (- v_{l})$ est inférieur à $a_{i}$ pour tout $i \in I$ , et est donc inférieur à $𝛼$ .

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

Donc $-$ est bien Scott-continue.

Q 8

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

La monotonie de $g_{F}$ a été montrée en Q 5.

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

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

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

l f p_{sup_{i \in I} 𝜂_{i}} (F) \geq sup_{i \in I} l f p_{𝜂_{i}} (F)

est acquise par monotonie de $g_{F}$ .

Montrons l’autre inégalité : $l f p_{sup_{i \in I} 𝜂_{i}} (F) \leq sup_{i \in I} l f p_{𝜂_{i}} (F)$ .

Méthode 1

\begin{aligned} sup_{i \in I} l f p_{𝜂_{i}} (F) & = sup_{i \in I} F (l f p_{𝜂_{i}} (F)) \\ = F (sup_{i \in I} l f p_{𝜂_{i}} (F)) & (⊛) \\ \geq l f p_{sup_{i \in I} 𝜂_{i}} (F) & (⊛⊛) \end{aligned}

$⊛$ : par Scott-continuité de $F$ , et car la famille $(l f p_{𝜂_{i}} (F))_{i \in I}$ reste dirigée.
- en effet : pour tous $i, j \in I$ , il existe $k$ tel que $𝜂_{k} \geq 𝜂_{i}, 𝜂_{j}$ . Donc
  $l f p_{𝜂_{k}} (F) \geq l f p_{𝜂_{i}} (F), l f p_{𝜂_{j}} (F)$
  par monotonie de $g_{F}$ .
$⊛ ⊛$ : $sup_{i \in I} l f p_{𝜂_{i}} (F)$ est un point fixe de $F$ (voir l’égalité qui précède) supérieur à tous à les $l f p_{𝜂_{i}} (F)$ (pour tout $i \in I$ ), donc (par transitivité) à tous les $𝜂_{i}$ (pour tout $i \in I$ ), donc à $sup_{i \in I} 𝜂_{i}$ . Par définition de $l f p_{sup_{i \in 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 : I^{n} ⟶ I^{n}$ est Scott-continue : pour tout $𝜂 \in I^{n}$ , la fonction $𝜂^{'} \mapsto 𝜂 \lor f (𝜂^{'})$ reste Scott-continue.

En effet :

sa monotonie est héritée de celle de $f$
toute famille dirigée $(𝜂_{i}^{'})_{i \in I}$ vérifie :
$sup_{i \in I} (𝜂 \lor f (𝜂_{i}^{'})) = 𝜂 \lor sup_{i \in I} f (𝜂_{i}^{'})$
car
- $\begin{matrix} \forall i \in I, 𝜂 \lor f (𝜂_{i}^{'}) \leq 𝜂 \lor sup_{i \in I} f (𝜂_{i}^{'}) \\ ⟹ sup_{i \in I} (𝜂 \lor f (𝜂_{i}^{'})) \leq 𝜂 \lor sup_{i \in I} f (𝜂_{i}^{'}) \end{matrix}$
- $sup_{i \in I} (𝜂 \lor f (𝜂_{i}^{'})) \geq 𝜂 $ e t $ sup_{i \in I} (𝜂 \lor f (𝜂_{i}^{'})) \geq sup_{i \in I} f (𝜂_{i}^{'}) $, d o n c $ sup_{i \in I} (𝜂 \lor f (𝜂_{i}^{'})) \geq 𝜂 \lor sup_{i \in I} f (𝜂_{i}^{'})$
  Par suite :
  $\begin{matrix} sup_{i \in I} (𝜂 \lor f (𝜂_{i}^{'})) = 𝜂 \lor sup_{i \in I} f (𝜂_{i}^{'}) \\ = 𝜂 \lor f (sup_{i \in I} 𝜂_{i}^{'}) \end{matrix}$
  par Scott-continuité de $f$ , et la Scott continuité de $𝜂^{'} \mapsto 𝜂 \lor f (𝜂^{'})$ est acquise.

On a vu en Q3 que :

\forall 𝜂 \in I^{n}, l f p_{𝜂} (F) = l f p (𝜂^{'} \mapsto 𝜂 \lor F (𝜂^{'}))

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

l f p_{sup_{i \in I} 𝜂_{i}} (F) = sup_{m \in ℕ} ((sup_{i \in I} 𝜂_{i}) \lor F)^{m} (⊥_{n})

en notant

$⊥_{n}$ le $n$ -uplet $(⊥, \dots, ⊥) \in I^{n}$ .
$(sup_{i \in I} 𝜂_{i}) \lor F$ la fonction $𝜂^{'} \mapsto (sup_{i \in I} 𝜂_{i}) \lor F (𝜂^{'})$

On veut donc montrer que :

\begin{aligned} l f p_{sup_{i \in I} 𝜂_{i}} (F) & \leq sup_{i \in I} l f p_{𝜂_{i}} (F) \\ ⟺ & sup_{m \in ℕ} ((sup_{i \in I} 𝜂_{i}) \lor F)^{m} (⊥_{n}) & \leq \underset{= sup_{m \in ℕ} sup_{i \in I} (𝜂_{i} \lor F)^{m} (⊥_{n})}{\underset{⏟}{sup_{i \in I} sup_{m \in ℕ} (𝜂_{i} \lor F)^{m} (⊥_{n})}} \end{aligned}

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

((sup_{i \in I} 𝜂_{i}) \lor F)^{m} (⊥_{n}) \leq sup_{i \in I} (𝜂_{i} \lor F)^{m} (⊥_{n})

Or : $\forall i_{1}, \dots, i_{m} \in I$ ,

\begin{matrix} \prod_{r = 1}^{m} (𝜂_{i_{r}} \lor F) (⊥_{n}) = (𝜂_{i_{1}} \lor F) \circ \dots \circ (𝜂_{i_{m}} \lor F) (⊥_{n}) \leq (𝜂_{k} \lor F)^{m} (⊥_{n}) \\ \leq ((sup_{j \in I} 𝜂_{j}) \lor F)^{m} (⊥_{n}) \end{matrix}

où

$𝜂_{i_{1}}, \dots, 𝜂_{i_{m}} \leq 𝜂_{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 \geq 2$ , en utilisant la transitivité de $\leq$ .
on a utilisé la monotonie (pour l’ordre point à point) de $𝜂^{'} \mapsto 𝜂^{'} \lor F$ (qui découle de la monotonie de $F$ ) et le fait qu’une composée de fonctions montones reste monotone :
- $(𝜂_{i_{1}} \lor F) ((𝜂_{i_{2}} \lor F) \dots \circ (𝜂_{i_{m}} \lor F) (⊥_{n})) \leq (𝜂_{k} \lor F) ((𝜂_{i_{2}} \lor F) \circ \dots \circ (𝜂_{i_{m}} \lor F) (⊥_{n}))$
- $(𝜂_{k} \lor F) \circ (𝜂_{i_{2}} \lor F) ((𝜂_{i_{3}} \lor F) \dots \circ (𝜂_{i_{m}} \lor F) (⊥_{n})) \leq (𝜂_{k} \lor F) \circ (𝜂_{k} \lor F) ((𝜂_{i_{3}} \lor F) \circ \dots \circ (𝜂_{i_{m}} \lor F) (⊥_{n}))$
  - car $(𝜂_{i_{2}} \lor F) ((𝜂_{i_{3}} \lor F) \dots \circ (𝜂_{i_{m}} \lor F) (⊥_{n})) \leq (𝜂_{k} \lor F) ((𝜂_{i_{3}} \lor F) \circ \dots \circ (𝜂_{i_{m}} \lor F) (⊥_{n}))$
    
    et $(𝜂_{k} \lor F)$ est monotone
- on conclut par une récurrence immédiate, par monotonie de $𝜂^{'} \mapsto 𝜂^{'} \lor F$ et de $(𝜂_{k} \lor F)^{l}$ pour tout $l \in ⟦ 1, m ⟧$ (par composition de fonctions monotones).

Or : $\forall i_{1}, \dots, i_{m} \in I$ ,

\prod_{r = 1}^{m} (𝜂_{i_{r}} \lor F) (⊥_{n}) \leq ((sup_{j \in I} 𝜂_{j}) \lor F)^{m} (⊥_{n})

implique que

((sup_{i \in I} 𝜂_{i}) \lor F)^{m} (⊥_{n}) = \prod_{r = 1}^{m} (sup_{i_{r} \in I} 𝜂_{i_{r}} \lor F) (⊥_{n}) \leq sup_{i \in I} (𝜂_{i} \lor F)^{m} (⊥_{n})

car :

Pour tous $x, y \in I^{n}$ : $\forall i \in I, (𝜂_{i} \lor F) (x) \leq y ⟹ ((sup_{i \in I} 𝜂_{i}) \lor F) (x) \leq y$
- En effet :
  
  $\forall i \in I, (𝜂_{i} \lor F) (x) = 𝜂_{i} \lor F (x) \leq y$ implique que $y$ majore les $𝜂_{i}$ , donc $y \geq sup_{i \in I} 𝜂_{i}$ , et comme $y \geq 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 \in I} 𝜂_{i}) \lor F$ .

Donc le résultat est acquis.

Q 9

La fonction $f i l t : E^{'} ⟶ {ρ \in E^{'} | ⟦ e ⟧_{ρ} \neq 0}$ est Scott-continue.

Elle est monotone :

Si $E, E^{'} \in ℙ (E n v)$ sont tels que $E \subseteq E^{'}$ : il est clair que
$f i l t (E) ≝ {ρ \in E \subseteq E^{'} | ⟦ e ⟧_{ρ} \neq 0} \subseteq {ρ \in E^{'} | ⟦ e ⟧_{ρ} \neq 0} ≝ f i l t (E^{'})$

Pour toute famille dirigée $(E_{i})_{i \in I}$ d’éléments de $ℙ (E n v)$ ,
$f i l t (sup_{i \in I} E_{i}) = f i l t (⋃_{i \in I} E_{i}) = sup_{i \in I} f i l t (E_{i})$

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

L’inégalité

f i l t (sup_{i \in I} E_{i}) \geq sup_{i \in I} f i l t (E_{i})

est acquise par monotonie.

Montrons que :

\begin{matrix} f i l t (sup_{i \in I} E_{i}) = f i l t (⋃_{i \in I} E_{i}) \\ = {ρ \in ⋃_{i \in I} E_{i} | ⟦ e ⟧_{ρ} \neq 0} \leq sup_{i \in I} f i l t (E_{i}) \\ = sup_{i \in I} {ρ \in E_{i} | ⟦ e ⟧_{ρ} \neq 0} \\ = ⋃_{i \in I} {ρ \in E_{i} | ⟦ e ⟧_{ρ} \neq 0} \end{matrix}

C’est clair, car pour tout $ρ \in ⋃_{i \in I} E_{i}$ tel que $⟦ e ⟧_{ρ} \neq 0$ , il existe $i \in I$ tel que

𝜌 \in E_{i}

donc

𝜌 \in {ρ^{'} \in E_{i} | ⟦ e ⟧_{ρ^{'}} \neq 0}

𝜌 \in ⋃_{j \in I} {ρ^{'} \in E_{j} | ⟦ e ⟧_{ρ^{'}} \neq 0}

Ainsi, on a montré que

{ρ \in ⋃_{i \in I} E_{i} | ⟦ e ⟧_{ρ} \neq 0} \subseteq ⋃_{i \in I} {ρ \in E_{i} | ⟦ e ⟧_{ρ} \neq 0}

Q 10

On note $f$ la fonction Scott-continue $E^{'} \mapsto E \cup 𝛷_{e, c} (E^{'})$ .

Lemme : $\forall m \in ℕ$ ,
$E_{m} = f^{m + 1} (\emptyset)$

En effet : par récurrence sur $m \in ℕ$ :

Initialisation : pour $m = 0$ , le résultat est acquis :
$\begin{matrix} E_{0} = E = E \cup \emptyset \\ = E \cup 𝛷_{e, c} (\emptyset) = f (\emptyset) \end{matrix}$
car $X ⟦ c ⟧ \emptyset = \emptyset$ (aucun environnement n’est accessible depuis $c$ et $\emptyset$ car il n’existe aucun environnement dans $\emptyset$ ).
Hérédité : pour $m \geq 1$ :
$\begin{aligned} E_{m} & = E \cup E_{m} & (car (E_{m})_{m \in ℕ} croît, et E \subseteq E_{m} (m \geq 1)) \\ = E \cup E_{m - 1} \cup X ⟦ c ⟧ {ρ \in E_{m - 1} | e ⟦ 𝜌 ⟧ \neq 0}) \\ = f (E_{m - 1}) \\ = f^{m + 1} (\emptyset) & (par hypothèse de récurrence) \end{aligned}$
Le résultat est donc acquis.

Donc

\begin{aligned} X ⟦ while e do c ⟧ E & = ⋃_{m \geq 0} E_{m} \\ = ⋃_{m \geq 1} f^{m} (\emptyset) & (d’après le lemme) \\ = ⋃_{m \geq 0} f^{m} (\emptyset) \\ = sup_{m \geq 0} f^{m} (\emptyset) \\ = l f p (f) & (par le théorème du point fixe de Kleene (f est Scott-continue)) \\ = l f p (E^{'} \mapsto E \lor 𝛷_{e, c} (E^{'})) \\ = l f p_{E} (𝛷_{e, c}) & (d’après Q3) \end{aligned}

ce qui conclut.

Q 11

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

Pour tout $v \in I$ , pour tout $E \in ℙ (ℤ)$ ,
$α (E) \leq v ⟺ E \subseteq γ (v)$

En effet : Soient $v \in I$ , $E \in ℙ (ℤ)$ .

Cas 1 : $v = ⊥$
$\begin{matrix} α (E) \leq v = ⊥ ⟺ α (E) = ⊥ \\ ⟺ E = \emptyset ⟺ E \subseteq γ (v) = \emptyset \end{matrix}$
Cas 2 : $v ≝ (a, b)$ (où $a, b \in ℤ \cup {\pm \infty}$ et $a + 1 < b$ ) :
- $⟹$ :
  
  Si $α (E) = (inf E - 1, sup E + 1) \leq v = (a, b)$ , alors
  - $inf E \geq a + 1$
  - $sup E \leq b - 1$
  et on a bien
  $E \subseteq [inf E, sup E] \subseteq] a, b [= γ (v)$
- $⟸$ :
  
  Si $E \subseteq γ (v) =] a, b [$ , alors
  - Comme $\forall e \in E, e \geq a + 1$ , il vient que $inf E \geq a + 1$
  - Comme $\forall e \in E, e \leq b - 1$ , il vient que $sup E \leq b - 1$
  et on a bien
  $α (E) = (inf E - 1, sup E + 1) \leq v = (a, b)$

Q 12

Soit $c$ une commande.

On suppose que pour tout environnement quotient $η^{'}$ et tout ensemble $E^{'} \in ℙ (E n v)$ que $η^{'}$ représente correctement, $Q ⟦ c ⟧ 𝜂^{'}$ représente correctement $X ⟦ c ⟧ E^{'}$ .

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

En effet :

Soit $𝜂 \in I^{n}$ représentant correctement $E \in ℙ (E n v)$ , i.e $𝛼 ({ρ (x) | ρ \in E}) \leq η (x)$ , ce qui équivaut à ${ρ (x) | ρ \in E} \subseteq 𝛾 (η (x))$ pour toute variable $x$ .

Montrons que : pour toute variable $x$ ,

{ρ (x) | ρ \in l f p_{E} (Φ_{e, c})} \subseteq 𝛾 (l f p_{η} (F_{e, c}) (x))

Lemme 1 : Soit $X$ est un DCPO pointé, $f : X ⟶ X$ une fonction inflationnaire Scott-continue, $x \in X$ :
$l f p_{x} (f) ≝ sup_{m \in ℕ} f^{m} (x)$

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

Posons

y ≝ sup_{m \in ℕ} f^{m} (x)

Alors :

\begin{aligned} f (y) & = f (sup_{m \in ℕ} f^{m} (x)) \\ = sup_{m \in ℕ} f^{m + 1} (x) & (par Scott-continuité de f) \\ = sup_{m \in ℕ} f^{m} (x) & (car f est inflationnaire (f (x) \geq x)) \end{aligned}

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{aligned} x \leq z \\ ⟹ & f (x) \leq f (z) = z & (par monotonie de f) \\ ⟹ & \forall m \in ℕ, f^{m} (x) \leq z & (par une récurrence immédiate) \\ ⟹ & y \leq z \end{aligned}

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

$l f p_{η} (F_{e, c}) = sup_{m \in ℕ} F_{e, c}^{m} (η)$
$l f p_{E} (Φ_{e, c}) = ⋃_{m \geq 0} Φ_{e, c}^{m} (E)$

Scolie 1 : Pour tous environnements quotients $𝜂^{'}, 𝜂^{″}$ et tous ensembles $E^{'}, E^{'} ‘ \in ℙ (E n v)$ représentés correctement respectivement par $𝜂^{'}, 𝜂^{″}$ : $𝜂^{'} \lor 𝜂^{″}$ représente correctement $E^{'} \cup E^{″}$

En effet :

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

{\begin{cases} {ρ (x) | ρ \in E^{'}} \subseteq 𝛾 (𝜂^{'} (x)) \\ {ρ (x) | ρ \in E^{″}} \subseteq 𝛾 (𝜂^{″} (x)) \end{cases} ⟹ {ρ (x) | ρ \in E^{'} \cup E^{″}} \subseteq 𝛾 (𝜂^{'} (x)) \cup 𝛾 (𝜂^{″} (x)) \subseteq 𝛾 ((𝜂^{'} \lor 𝜂^{″}) (x))

la dernière inclusion venant du fait que :

$𝛾 (𝜂^{'} (x)) \subseteq 𝛾 ((𝜂^{'} \lor 𝜂^{″}) (x))$ et $𝛾 (𝜂^{'} ‘ (x)) \subseteq 𝛾 ((𝜂^{'} \lor 𝜂^{″}) (x))$ car $𝛾$ est monotone
ce qui impique que $𝛾 (𝜂^{'} (x)) \cup 𝛾 (𝜂^{'} ‘ (x)) \subseteq 𝛾 ((𝜂^{'} \lor 𝜂^{″}) (x))$

Scolie 2 : Pour tout environnement quotient $η^{'}$ et tout ensemble $E^{'} \in ℙ (E n v)$ que $η^{'}$ représente correctement :

$F_{e, c} (η^{'})$ représente correctement $Φ_{e, c} (E^{'})$

En effet :

Cas 1 : Si $Q ⟦ e ⟧ η^{'} =⊥$ ou $Q ⟦ e ⟧ η^{'} = 𝛼 ({0})$ :

alors
- $Φ_{e, c} (E^{'}) = E^{'} \cup X ⟦ c ⟧ {ρ \in E^{'} | e ⟦ ρ ⟧ \neq 0}$
- $F_{e, c} (η^{'}) = η^{'}$
mais comme $Q ⟦ e ⟧ η^{'}$ représente correctement ${⟦ e ⟧ 𝜌 | 𝜌 \in E^{'}}$ , il vient que :
${⟦ e ⟧ 𝜌 | 𝜌 \in E^{'}} \subseteq 𝛾 (Q ⟦ e ⟧ η^{'}) \subseteq {0}$
Donc ${ρ \in E^{'} | e ⟦ ρ ⟧ \neq 0} = \emptyset$ , et :
$X ⟦ c ⟧ {ρ \in E^{'} | e ⟦ ρ ⟧ \neq 0} = X ⟦ c ⟧ \emptyset = \emptyset$
(cf. l’initialisation du lemme de Q10)

Par suite :
$Φ_{e, c} (E^{'}) = E^{'}$
et le résultat est acquis (par hypothèse).
Cas 2 : Sinon, si $Q ⟦ e ⟧ η^{'} \neq⊥$ et $Q ⟦ e ⟧ η^{'} \neq 𝛼 ({0})$ :

alors
- $Φ_{e, c} (E^{'}) = E^{'} \cup X ⟦ c ⟧ {ρ \in E^{'} | e ⟦ ρ ⟧ \neq 0}$
- $F_{e, c} (η^{'}) = η^{'} \lor Q ⟦ c ⟧ η^{'}$
et :
${⟦ e ⟧ 𝜌 | 𝜌 \in E^{'}} \subseteq 𝛾 (Q ⟦ e ⟧ η^{'}) \neq \emptyset, {0}$
(car $𝛼 \circ 𝛾 = i d$ )

D’où :
$\emptyset \neq {ρ \in E^{'} | e ⟦ ρ ⟧ \neq 0} \subseteq E^{'}$
et pour toute variable $x$ :
${ρ (x) | ρ \in {ρ \in E^{'} | e ⟦ ρ ⟧ \neq 0}} \subseteq {ρ (x) | ρ \in E^{'}} \subseteq 𝛾 (𝜂^{'} (x))$
donc $𝜂^{'}$ représente correctement ${ρ \in E^{'} | e ⟦ ρ ⟧ \neq 0}$ , donc $Q ⟦ c ⟧ 𝜂^{'}$ représente correctement $X ⟦ c ⟧ {ρ \in E^{'} | e ⟦ ρ ⟧ \neq 0}$ (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} (E^{'})$ .

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

En effet : par récurrence sur $m \in ℕ$ :

Initialisation : pour $m = 0$ , le résultat est acquis.
Hérédité : pour $m \geq 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} (E)$ , pour en déduire que $F_{e, c}^{m} (η)$ représente correctement $Φ_{e, c}^{m} (E)$ .

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

Pour tout $N \in ℕ$ ,

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

Donc pour tout $N \in ℕ$ , pour toute variable $x$ :

{ρ (x) | ρ \in ⋃_{m = 0}^{N} Φ_{e, c}^{m} (E)} \subseteq 𝛾 (sup_{0 \leq m \leq N} F_{e, c}^{m} (η) (x)) \subseteq 𝛾 (sup_{m \in ℕ} F_{e, c}^{m} (η) (x)) = 𝛾 (l f p_{η} (F_{e, c}) (x))

par monotonie de $𝛾$ , et :

$l f p_{η} (F_{e, c})$ représente correctement $⋃_{m = 0}^{N} Φ_{e, c}^{m} (E)$ pour tout $N \in ℕ$ .

Par l’absurde :

Si $l f p_{η} (F_{e, c})$ ne représentait pas correctement $l f p_{E} (Φ_{e, c}) = ⋃_{m \geq 0} Φ_{e, c}^{m} (E)$ : il existerait une variable $x$ et un environnement (réel) $𝜌 \in ⋃_{m \geq 0} Φ_{e, c}^{m} (E)$ tels que $𝜌 (x) \in ({ρ^{'} (x) | ρ^{'} \in ⋃_{m \geq 0} Φ_{e, c}^{m} (E)}) \ 𝛾 (l f p_{η} (F_{e, c}) (x))$ .

Or, il existerait un $N \in ℕ$ tel que $𝜌 \in Φ_{e, c}^{N} (E) \subseteq ⋃_{m = 0}^{N} Φ_{e, c}^{m} (E)$ , d’où

𝜌 (x) \in ({ρ^{'} (x) | ρ^{'} \in ⋃_{m = 0}^{N} Φ_{e, c}^{m} (E)}) \ 𝛾 (l f p_{η} (F_{e, c}) (x))

ce qui est absurde, car ${ρ^{'} (x) | ρ^{'} \in ⋃_{m = 0}^{N} Φ_{e, c}^{m} (E)} \subseteq 𝛾 (l f p_{η} (F_{e, c}) (x))$ .

Ainsi :

$l f p_{η} (F_{e, c}) = sup_{m \in ℕ} F_{e, c}^{m} (η)$ représente correctement $l f p_{E} (Φ_{e, c}) = ⋃_{m \geq 0} Φ_{e, c}^{m} (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^{'} = while e 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 $𝜂 \in I^{n}$ et $E \in ℙ (E n v)$ , si $η$ représente correctement $E$ , alors $Q ⟦ x := e ⟧ 𝜂 = η \lor η [x \to Q ⟦ e ⟧ η]$ représente correctement $X ⟦ x := e ⟧ E = E \cup {ρ [x \to ⟦ e ⟧ ρ] | ρ \in E}$ .

En effet :

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

i.e pour toute variable $y$ ,

{ρ^{'} (y) | ρ^{'} \in {ρ [x \mapsto ⟦ e ⟧ ρ] | ρ \in E}} \subseteq 𝛾 (η [x \mapsto Q ⟦ e ⟧ η] (y))

Soit $y$ une variable.

On sait par ailleurs que $Q ⟦ e ⟧ η$ représente correctement ${⟦ e ⟧ ρ | ρ \in E}$ , i.e :

{⟦ e ⟧ ρ | ρ \in E} \subseteq 𝛾 (Q ⟦ e ⟧ η) ⊛

Soit $ρ^{'} \in {ρ [x \mapsto ⟦ e ⟧ ρ] | ρ \in E}$ .

Montrons que $ρ^{'} (y) \in 𝛾 (η [x \mapsto Q ⟦ e ⟧ η] (y))$

Cas 1 : Si $y \neq x$

alors
$𝜌^{'} (y) \in {ρ (y) | ρ \in E} \subseteq 𝛾 (\underset{= η [x \mapsto Q ⟦ e ⟧ η] (y)}{\underset{⏟}{𝜂 (y)}}) = 𝛾 (η [x \mapsto Q ⟦ e ⟧ η] (y))$
(car $𝜂$ représente correctement $E$ ).
Cas 2 : Si $y = x$

alors
$𝜌^{'} (y) = 𝜌^{'} (x) = ⟦ e ⟧ 𝜌^{'} \in {⟦ e ⟧ ρ | ρ \in E} \subseteq 𝛾 (\underset{= η [x \mapsto Q ⟦ e ⟧ η] (y)}{\underset{⏟}{Q ⟦ e ⟧ η}})$
(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 $\geq$ : $> ≝ \geq et \neq$

Soit $x$ une variable telle que $\emptyset \neq 𝛾 (𝜂 (x)) \subseteq ℤ$ (donc si $𝜂 (x) ≝ (a, b)$ : $a, b \in ℤ$ )

Avec $while \underset{≝ e}{\underset{⏟}{1}} do \underset{≝ c}{\underset{⏟}{x := x + 1}}$ :

comme

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

ici :

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

η [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 :

\forall m \in ℕ^{*}, 𝜂_{m} ≝ F_{e, c} (η_{m - 1}) = η_{m - 1} [x \mapsto η_{m - 1} (x) + (0, 2)] > η_{m - 1}

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

Q 17

Cette fois :

F_{e, c}^{'} (η^{'}) = {\begin{cases} η^{'} si Q ⟦ e ⟧ η^{'} =⊥ ou Q ⟦ e ⟧ η^{'} = 0 \\ η^{'} \nabla Q ⟦ c ⟧ η^{'} sinon. \end{cases}

On remarque que : pour tout environnement quotient $𝜂^{'}$ , $F_{e, c}^{'} (𝜂^{'}) \geq 𝜂^{'}$ (car $η^{'} \nabla Q ⟦ c ⟧ η^{'} \geq 𝜂^{'}$ ).

Donc pour tout $m \in ℕ^{*}$ :

Cas 1 : $𝜂_{m} = F_{e, c}^{'} (η_{m - 1}) = η_{m - 1} (si Q ⟦ e ⟧ 𝜂_{m - 1} \in {⊥, (- 1, 1)} ou Q ⟦ c ⟧ 𝜂_{m - 1} \leq 𝜂_{m - 1}$ )

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) = ⊥$
$(- \infty, b)$ ou $(a, + \infty)$ sinon

d’où il existe $i \in ⟦ 0, 2 ⟧$ indices $p_{1} > \dots > p_{i} > m$ tels que

$\forall j \in ⟦ 1, i ⟧, 𝜂_{p_{j}} (x) > 𝜂_{p_{j} - 1} (x)$ (si $i \geq 1$ , $𝜂_{p_{1}} (x)$ vaut alors $(- \infty, + \infty)$ , d’où $(𝜂_{q} (x))_{q \geq p_{1}}$ est constante de valeur $(- \infty, + \infty)$ )

Donc

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

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

On remarque par ailleurs que

si $\exists m \in ℕ; 𝜂_{m + 1} = 𝜂_{m}$ , alors $\forall p \geq m, 𝜂_{p} = 𝜂_{m}$ $⊛ ⊛$

(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 \geq 1$ que $\forall q \geq 1, 𝜂_{m + q} = 𝜂_{m}$ )

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

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

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

𝜂 \lor Q ⟦ c ⟧ η \leq 𝜂 \nabla Q ⟦ c ⟧ η

en effet : pour toute variable $x$ :
- Si $Q ⟦ c ⟧ η (x) \leq 𝜂 (x)$ , alors $(𝜂 \nabla Q ⟦ c ⟧ η) (x) = (𝜂 \lor Q ⟦ c ⟧ η) (x) = 𝜂 (x)$
- Sinon :
  - si $𝜂 (x) = ⊥$ : $(𝜂 \nabla Q ⟦ c ⟧ η) (x) = (𝜂 \lor Q ⟦ c ⟧ η) (x) = Q ⟦ c ⟧ η (x)$
  - si $𝜂 (x) ≝ (a, b), Q ⟦ c ⟧ η (x) ≝ (c, d)$ (où $a, b, c, d \in ℤ \cup {\pm \infty}$ ) :
    $(𝜂 \lor Q ⟦ c ⟧ η) (x) = (min (a, c), max (b, d))$
    et en posant
    - $𝛼 ≝ {\begin{cases} min (a, c) si min (a, c) = a - \infty sinon \end{cases}$
    - $𝛽 ≝ {\begin{cases} max (b, d) si max (b, d) = b + \infty sinon \end{cases}$
    $(𝜂 \lor Q ⟦ c ⟧ η) (x) = (min (a, c), max (b, d)) \leq (𝛼, 𝛽) ≝ (𝜂 \nabla Q ⟦ c ⟧ η) (x)$

Il s’ensuit que :

F_{e, c} \leq 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 $while e do c^{'}$ , car $F_{e, c^{'}} \leq F_{e, c^{'}}^{'}$ et par monotonie (pour l’ordre point à point) de la fonction $𝛹_{𝜂^{'}} : f \mapsto l f p_{𝜂^{'}} (f)$ pour tout environnement quotient $𝜂^{'}$
  - en effet: la monotonie de $𝛹_{𝜂^{'}} : f \mapsto l f p_{𝜂^{'}} (f)$ vient du lemme 1 de Q12 :
    
    si $f \leq g$ ,
    $l f p_{𝜂^{'}} (f) = sup_{m \in ℕ} \underset{\leq g^{m} (𝜂^{'})}{\underset{⏟}{f^{m} (𝜂^{'})}} \leq sup_{m \in ℕ} g^{m} (𝜂^{'}) = l f p_{𝜂^{'}} (g)$

Scolie : Si $η^{″}$ et $𝜂^{'}$ sont des environnements tels que

$𝜂^{'} \leq 𝜂^{″}$

$𝜂^{'}$ représente correctement un ensemble $E^{'}$ d’environnements (réels)

alors $𝜂^{″}$ représente correctement $E^{'}$ .

En effet :

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

{\begin{cases} {ρ (x) | ρ \in E^{'}} \subseteq 𝛾 (𝜂^{'} (x)) \\ 𝛾 (𝜂^{'} (x)) \subseteq 𝛾 (𝜂^{″} (x)) (par monotonie de 𝛾) \end{cases} ⟹ {ρ (x) | ρ \in E^{'}} \subseteq 𝛾 (𝜂^{″} (x))

Donc d’après la scolie :

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

Share on

Twitter Facebook Google+ LinkedIn

DM Programmation I

Q 1

Q 2

a).

b).

Q 3

Q 4

Q 5

Q 6

Q 7

Q 8

Méthode 1

Méthode 2

Q 9

Q 10

Q 11

Q 12

Q 13

Q 14 / 15

Q 16

Q 17

Share on

Leave a comment