Program Semantics and Classical Logic

Lemma 20 If Q 'c Q⁰ then [Pk/Xk]_fe Q 'c [Pk/Xk]_fe Q⁰.

Proof. Let Q₁ , . . . , Q_n be a derivation of Q⁰ from Q. It follows immediately
from the previous lemma that, for 1 ≤ i ≤ n, [P_k/X_k]_k Q_i+1 is an immediate
consequence of [Pk/Xk]k Qi. Hence [Pk/Xk]k Q1, . . . , [Pk/Xk]k Qn is a deriva-
tion of [Pk/Xk]k Q⁰ from [Pk/Xk]_fc Q. □

The next two lemmas establish properties of the union of the denotations of
all linear programs deriving a given program.

Lemma 21 If Ri ⊆ S{V (L^j₁ ,α) | Li 'c Qi} and R2 ⊆ S{V (L2,α) | L2 'c
Q2} then Ri ◦ R2 ⊆ S{V(L^t, a) | L 'c Qi; Q2}

Proof. From the assumptions and the translation of Li ; L2 it follows that

Ri ◦ R2 ⊆ [{V(L1,α) ◦V(L1,a) | Li 'c Qi,Li 'c Q2}

= ^[{V((L_i; L₂)^t, a) | L_i '_c Q_i, L_i '_c Q₂}

But since Lemma 18 tells us that L 'c Q_i; Q₂ iff there are L_i and L₂ such
that L = Li; L2 while Li 'c Qi and L2 'c Q2, the latter term is equal to
^S{V(L^t, a) | L 'c Qi;Q2}.    □

Lemma 22 Suppose Rk ⊆ ^S{V (L^t , a) | L 'c Qk} for all k (1 ≤ k ≤ n).
Then for all linear programs L:

V(L^t,a[Ri/Xi,...,Rn/Xn]) ⊆^[{V(L^0t,a) | L⁰ 'c [Qi/Xi,..., Qn/Xn]L}

Proof. This follows by induction on the number m of occurrences of the
variables X_i , . . . , X_n in L. If m = 0 the statement reduces to V (L^t , a) ⊆
^S{V (L^0t, a) | L⁰ '_c L}, which is obviously true. If m > 0 then L has the
form Li ; Xk; L2, with fewer than m occurrences of Xi , . . . , Xn in Li and L2.

Write a⁰ for a[Ri/Xi , . . . , Rn/Xn]. Then

V(L^t, a⁰) = V(Li, a⁰) ◦ Rk ◦ V(l2, a⁰).

From the induction hypothesis it follows that

V(Li^t,a⁰) ⊆ ^[{V(L^0t,a) | L⁰ 'c [Qi/Xi,..., Qn/Xn]Li}

for i ∈ {1, 2}. This, together with the assumption R_k ⊆ ^S{V (L^t, a) | L '_c
Q_k} and Lemma 21 allows us to draw the desired conclusion that

V(L^t,a⁰) ⊆ ^[{V(L^0t,a) | L⁰ 'c [Qi/Xi,..., Qn/Xn]Li; Xk; L2}

□

28

<<   25   26   27   28   29   30   31   >>

More intriguing information