Program Semantics and Classical Logic

So that the value of this term is the intersection of all S such that S =
V(B, a[S₁ /X₁ , . . . , S_n/X_n]) for some S₁ , . . . , S_n which are simultaneous fix-
points in the sense that S_k = V(A_k, a[S₁/X₁, . . . , S_n/X_n]) for each k. It
follows from the continuity of the terms Ak that V (B, a [Rn/X₁,..., Rn /X_n])
is among those S , so that we have

n

V (λr. ∀Xι... Xn( ʌ Xi = Ai → B(r)), a) ⊆ V (B, a[Rn/Xι,..., R. /X_n])
i=1

To show the converse, suppose that Sk = V(Ak, a[S1/X1 , . . . , Sn/Xn]) for
1 ≤ k ≤ n. The monotonicity of the A_k readily gives us that R_k^m ⊆ S_k for all
k and m. It follows that R_k^ω ⊆ S_k for all k and hence, by B’s monotonicity,
that

V (B, a[Rω/Xι,..., Rn /Xn]) ⊆ V (B, a[Si/Xi,..., Sn/Xn]).

Since S1 , . . . , Sn were arbitrary simultaneous fixpoints, we conclude that
n

V(B, a[R1ⁿ/X1,..., Rnⁿ/Xn]) ⊆V(λr.∀X1...Xn(_i=1Xi =Ai → B(r)), a)

□

Having shown some general properties of continuity and weak anticontinu-
ity to hold, we now turn to proving that the translations we have given in
section 6 possess the desired properties. A reader who wants to prove that
translations of programs are continuous in the variables X occurring in them
will notice that one clause of the required induction cannot be proved us-
ing simple continuity properties of union and relational composition. The
required extra proof uses lemma 8 and is given below.

Lemma 9 If B and A₁ , . . . , A_n are terms of type s × s → t which are con-
tinuous in the type s × s → t variables X1 , . . . , Xn and in ξα, then

λr.∀X1...Xn(^{^n} Xi =Ai → B(r))
i=1

is also continuous in ξ.

Proof. If ξ is among {X₁ , . . . , X_n} we are done, so assume X_k 6= ξ. Let
R⁰ ⊆ R¹ ⊆ . . . ⊆ Rⁿ ⊆ . . . be an arbitrary chain of type α relations. Define,

20

<<   17   18   19   20   21   22   23   >>

More intriguing information