Program Semantics and Classical Logic



for each ` N {ω}, each m N and each k (1 k n) the relation
R. by setting R0,k = 0 and Rmk+1 = V(Ak, α[Rm√Xι,..., Rmn∕Xn, R'∕ξ])•
Then R
0k R'k ... Rnk ... for each k and '. Moreover, it
,,     ,

is easily proved by induction on m, using the monotonicity of the Ak and
the definition of R
mk that Rmk Rm+1,k if ' N, so that we also have
chains R
mk Rmk ... Rmk .... We prove by induction on m that
S' Rmk = Rmk. This is trivial for m = 0. Suppose the statement holds for
m. Then, using the continuity of the
Ak and the induction hypothesis, we
find that

R'm,k+1  =

'

[ V(Ak, a[Rm1∕X1,..., Rm/Xn, R'∕ξ]) =
'

V(Ak,a


U Rm1∕X1,... , Rmn/Xn, U R'∕ξ ) =

'   ''

V(Ak, a Rωm,1∕X1,..., Rωm,n∕Xn, Rω ∕ξ ) =

Rωm,+k 1

Since Rωω,k = m  ' R'm,k = '  m R'm,k it follows that (*) Rωω,k =  'R'ω,k. Now

we reason as follows, using Lemma 8 twice and using (*) and the continuity
of
B in ξ

[V(λr.X1 .. .Xn(^n Xi = Ai → B(r)), a[R'∕ξ]) =

'                        i=1

[ V(B, a[R'ω,1∕X1,..., R'ω,n∕Xn, R'∕ξ]) =
'

V(B, a


R'ω,1∕X1,...,   R'ω,n∕Xn,   R'∕ξ

)=


'   ''

V(B,a Rωω,1∕X1,..., Rωω,n∕Xn, Rω∕ξ ) =

V(λr.X1...Xn(^n Xi =Ai → B(r)), a[Rω ∕ξ])

i=1

This concludes the proof

That translations of programs are continuous is now easily proved. The
proposition will allow us to apply the Knaster-Tarski theorem to those trans-
lations.

21



More intriguing information

1. An Empirical Analysis of the Curvature Factor of the Term Structure of Interest Rates
2. Spatial patterns in intermunicipal Danish commuting
3. The fundamental determinants of financial integration in the European Union
4. Markets for Influence
5. AN IMPROVED 2D OPTICAL FLOW SENSOR FOR MOTION SEGMENTATION
6. Benchmarking Regional Innovation: A Comparison of Bavaria, Northern Ireland and the Republic of Ireland
7. The name is absent
8. Changing spatial planning systems and the role of the regional government level; Comparing the Netherlands, Flanders and England
9. The name is absent
10. The name is absent