Program Semantics and Classical Logic

Proposition 10 For every program P and procedure call X in P, P^ is
continuous in X.

Proof. By induction on the complexity of P, using the previous lemma for
the case that P = hXi ^ Piii(Q).   □

We can prove a similar connection between correctness formulae and weak
anticontinuity. First we note that there are certain syntactic features which
will guarantee a type logical term to be continuous or anticontinuous in a
given variable.

Lemma 11

1. If φ is continuous in ξ then -φ is anticontinuous in ξ;

2. If φ is anticontinuous in ξ then -φ is continuous in ξ;

3. If φ,ψ are (anti-)continuous in ξ then φ ∧ ψ is (anti-)continuous in ξ;

4. If A_α→t is (anti-)continuous in ξ and ξ does not occur in δ_α then A(δ)
is (anti-)continuous in ξ;

5. If φ is (anti-)continuous in ξ then λζ_α.φ is (anti-)continuous in ξ;

6. If φ is anticontinuous in ξ then ∀ζ φ is anticontinuous in ξ;

7. If φ is continuous in ξ then ∃ζ φ is continuous in ξ.

Proof. By inspection of the various cases. To prove the first case, for example,
assume that φ is continuous in ξ, and let R⁰ ⊆ R¹ ⊆ ... ⊆ Rⁿ ⊆ ... be a
chain. Then T_n V(-φ,a[Rⁿ/ξ]) = 1 iff, for all n, V(-φ, a[Rⁿ∕ξ]) = 1 iff (by
Definition 10), for all n, V(φ, a[Rⁿ∕ξ]) = 0 iff S_n V(φ, a[Rⁿ∕ξ]) = 0 iff (by
continuity of φ) V(φ, a[R^ω/ξ]) = 0 iff (by Definition 10) V(-φ, a[R^ω/ξ]) = 1.

The other cases are equally simple and are left to the reader. □

The relation between correctness formulas and weak anticontinuity that was
promised is stated and proved as follows.

Proposition 12 For every correctness formula C and procedure call X in
C, C t is weakly anticontinuous in X .

22

<<   19   20   21   22   23   24   25   >>

More intriguing information