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. How much do Educational Outcomes Matter in OECD Countries?
3. Keystone sector methodology:network analysis comparative study
4. Segmentación en la era de la globalización: ¿Cómo encontrar un segmento nuevo de mercado?
5. The name is absent
6. Getting the practical teaching element right: A guide for literacy, numeracy and ESOL teacher educators
7. Confusion and Reinforcement Learning in Experimental Public Goods Games
8. The name is absent
9. Work Rich, Time Poor? Time-Use of Women and Men in Ireland
10. APPLICATIONS OF DUALITY THEORY TO AGRICULTURE