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
More intriguing information
1. Bargaining Power and Equilibrium Consumption2. The name is absent
3. ARE VOLATILITY EXPECTATIONS CHARACTERIZED BY REGIME SHIFTS? EVIDENCE FROM IMPLIED VOLATILITY INDICES
4. The name is absent
5. Plasmid-Encoded Multidrug Resistance of Salmonella typhi and some Enteric Bacteria in and around Kolkata, India: A Preliminary Study
6. FISCAL CONSOLIDATION AND DECENTRALISATION: A TALE OF TWO TIERS
7. Moi individuel et moi cosmique Dans la pensee de Romain Rolland
8. The name is absent
9. EMU's Decentralized System of Fiscal Policy
10. Bridging Micro- and Macro-Analyses of the EU Sugar Program: Methods and Insights