Program Semantics and Classical Logic

The Union Theorem can now be proved. It was already clear that execution
of some program P must consist in execution of some L such that L 'C P
and, conversely, that execution of any such L amounts to execution of P .
The theorem shows that this squares with the modeltheoretic interpretation
of programs which we have obtained by our translation and in this way
provides a justification for that translation.

Theorem 23 (Union Theorem) VM(P^t, a) = S{VM(L^t,a) | L 'C P} for
all models M and assignments a.

Proof. That S{V (L^t,a) | L 'C P} ⊆ V (P^t, a) follows from Proposition 17.
We prove the reverse, the statement that V (P^t, a) ⊆ S{V (L^t,a) | L 'C P},
by induction on the complexity of P. In case P is atomic the only L such
that L 'C P is P itself, so the statement is trivially true. In case P is P₁ ∪ P₂
or P is P₁ ; P₂ and the statement holds for P₁ and P₂, we can easily derive
the statement for P itself. This leaves it for us to prove that

V((<Xi ^ Pii'=ι(P_n+ι))^t, a) ⊆ [{V(L^t,a) | L 'C <Xi ^ Pi)'=ι(P,,+ι)}

under the induction hypothesis (*) that for all k (1 ≤ k ≤ n + 1) V(P_k^t, a) ⊆
^S{V(L^t, a) | L 'C Pk } for all assignments a. In fact, we shall strengthen the
statement somewhat and use the induction hypothesis to prove that

V((hXi ^ Piii=ι(Pk))^t,a) ⊆ [{V(L^t,a) | L 'C <Xi ^ Pi‰(P_k)}

for all k (1 ≤ k ≤ n + 1). To this end, define relations R_k^m for all m ∈
N by setting Rf⁰_k = 0 and Rf⁺¹ = V(Pk^t,a[Rm/X₁,..., Rf∕X_n]). Using a
subinduction on m we prove that Rf ⊆ S{V(L^t, a) | L 'C <X_i ^ P_i}f=₁(P_k)}
for all m and k (1 ≤ k ≤ n+ 1). Since this is trivially true for m = 0, suppose
(**) the statement holds for m. The induction hypothesis (*) gives us that

Rk^m+1 = V(Pk^t, a[R1^m/X1,..., Rn^m/Xn])

⊆ ^[{V(L^0t, a[R1^m/X1,..., Rn^m/Xn]) |L⁰'CPk}

On the other hand, Lemma 22 in combination with the subinduction hypoth-
esis (**) tells us that, for any linear program L⁰:

V (L^0t, a[R1^m/X1,..., Rn^m/Xn]) ⊆

[{V(L^t,a) | L 'C [<Xi ^ Piin=ι(Pj)/Xj]n=ιL⁰}
29

<<   26   27   28   29   30   31   32   >>

More intriguing information