the power set of Dα . The natural Boolean algebra on Dt is also turned into a
set algebra if we identify 1 with {0}, as it is usually done in set theory. Type
t and types α → t will be called relational and objects in such domains will
be called relations. We shall freely talk about unions, intersections, inclusion
etc. of relations. In fact, we shall often have occasion to talk about chains
R0 ⊆ R1 ⊆ . . . ⊆ Rn ⊆ . . . of relations of some type, and shall write the
union Sn∈N Rn of such a chain as Rω . The following definition imports some
important notions from the Scott-Strachey tradition into our modeltheoretic
setting.
Definition 15 (Continuity, Anticontinuity, Weak anticontinuity)
A term A of relational type is called (a) continuous, (b) anticontinuous, (c)
weakly anticontinuous in the variable ξ of relational type α iff it holds for
each model, each assignment a, and each chain of type α relations R0 ⊆ R1 ⊆
... ⊆ Rn ⊆ ... that
(a) U V(A,a[Rn∕ξ]) = V(A,α[Rω/ξ])
(b) ∩V(A,α[Rn∕ξ]) = V(A,α[Rω∕ξ])
(c) ∩ V(A,α[Rn∕ξ]) ⊆ V(A,a[Rω∕ξ])
It will be our aim to show that translations of programs are continuous in the
procedure calls occurring free in them and that translations of correctness
formulas are weakly anticontinuous in such procedure calls.
Related to continuity is monotonicity. We define the notion below and
state the usual lemma which says that it is weaker than continuity.
Definition 16 (Monotonicity) A term A of relational type is called mono-
tonic in ξ iff R1 ⊆ R2 implies V (A, a[R1∕ξ]) ⊆ V (A, α[R2∕ξ]).
Lemma 5 If A is continuous in ξ then A is monotonic in ξ.
Proof. Consider R1 ⊆ R2 ⊆ R2 ⊆ ... ⊆ R2 ⊆ ... □
The next two lemmas generalise the notions of continuity and anticontinuity
somewhat. These notions were defined with respect to one variable, but
the first lemma shows that that restriction was inessential in the case of
17