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(Pt, a) = S{VM(Lt,a) | L 'C P} for
all models
M and assignments a.

Proof. That S{V (Lt,a) | L 'C P} V (Pt, a) follows from Proposition 17.
We prove the reverse, the statement that
V (Pt, a) S{V (Lt,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 P1 P2
or P is P1 ; P2 and the statement holds for P1 and P2, we can easily derive
the statement for P itself. This leaves it for us to prove that

V((<Xi ^ Pii'(Pn))t, a) [{V(Lt,a) | L 'C <Xi ^ Pi)'(P,,)}

under the induction hypothesis (*) that for all k (1 k n + 1) V(Pkt, a)
S{V
(Lt, 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(Lt,a) | L 'C <Xi ^ Pi‰(Pk)}

for all k (1 k n + 1). To this end, define relations Rkm for all m
N
by setting Rf0k = 0 and Rf+1 = V(Pkt,a[Rm/X1,..., Rf∕Xn]). Using a
subinduction on m we prove that
Rf S{V(Lt, a) | L 'C <Xi ^ Pi}f=1(Pk)}
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

Rkm+1 = V(Pkt, a[R1m/X1,..., Rnm/Xn])

[{V(L0t, a[R1m/X1,..., Rnm/Xn]) |L0'CPk}

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

V (L0t, a[R1m/X1,..., Rnm/Xn])

[{V(Lt,a) | L 'C [<Xi ^ Piin(Pj)/Xj]nL0}
29



More intriguing information

1. The name is absent
2. Optimal Vehicle Size, Haulage Length, and the Structure of Transport Costs
3. Natural hazard mitigation in Southern California
4. The name is absent
5. Social Cohesion as a Real-life Phenomenon: Exploring the Validity of the Universalist and Particularist Perspectives
6. SOME ISSUES IN LAND TENURE, OWNERSHIP AND CONTROL IN DISPERSED VS. CONCENTRATED AGRICULTURE
7. The name is absent
8. Credit Market Competition and Capital Regulation
9. NATIONAL PERSPECTIVE
10. Tax systems and tax reforms in Europe: Rationale and open issue for more radical reforms