So that the value of this term is the intersection of all S such that S =
V(B, a[S1 /X1 , . . . , Sn/Xn]) for some S1 , . . . , Sn which are simultaneous fix-
points in the sense that Sk = V(Ak, a[S1/X1, . . . , Sn/Xn]) for each k. It
follows from the continuity of the terms Ak that V (B, a [Rn/X1,..., Rn /Xn])
is among those S , so that we have
n
V (λr. ∀Xι... Xn( ʌ Xi = Ai → B(r)), a) ⊆ V (B, a[Rn/Xι,..., R. /Xn])
i=1
To show the converse, suppose that Sk = V(Ak, a[S1/X1 , . . . , Sn/Xn]) for
1 ≤ k ≤ n. The monotonicity of the Ak readily gives us that Rkm ⊆ Sk for all
k and m. It follows that Rkω ⊆ Sk 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[R1n/X1,..., Rnn/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 A1 , . . . , An 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 {X1 , . . . , Xn} we are done, so assume Xk 6= ξ. Let
R0 ⊆ R1 ⊆ . . . ⊆ Rn ⊆ . . . be an arbitrary chain of type α relations. Define,
20