Program Semantics and Classical Logic



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
R
0 R1 . . . Rn . . . of relations of some type, and shall write the
union
SnN 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



More intriguing information

1. Pricing American-style Derivatives under the Heston Model Dynamics: A Fast Fourier Transformation in the Geske–Johnson Scheme
2. For Whom is MAI? A theoretical Perspective on Multilateral Agreements on Investments
3. The name is absent
4. AN ECONOMIC EVALUATION OF THE COLORADO RIVER BASIN SALINITY CONTROL PROGRAM
5. The growing importance of risk in financial regulation
6. Moffett and rhetoric
7. ‘I’m so much more myself now, coming back to work’ - working class mothers, paid work and childcare.
8. Initial Public Offerings and Venture Capital in Germany
9. Weather Forecasting for Weather Derivatives
10. PROJECTED COSTS FOR SELECTED LOUISIANA VEGETABLE CROPS - 1997 SEASON
11. Credit Markets and the Propagation of Monetary Policy Shocks
12. Wage mobility, Job mobility and Spatial mobility in the Portuguese economy
13. The name is absent
14. Globalization, Divergence and Stagnation
15. The name is absent
16. The name is absent
17. The name is absent
18. Legal Minimum Wages and the Wages of Formal and Informal Sector Workers in Costa Rica
19. Empirical Calibration of a Least-Cost Conservation Reserve Program
20. The name is absent