Program Semantics and Classical Logic

We shall refer to UA as to the Update Axiom . The axiom is related to the
‘Update Postulate’ of [10] and to the ‘Having Enough States’ axiom of [5].
We write Γ =AX φ if Γ, UA, PA² =_s φ.

This ends the list of axioms we wish to impose. To see that they are
consistent, it suffices to construct a model in which De consists of the set N
of natural numbers, where Ds is the set of all functions f : N → N, and
where I(V ) is the function such that I(V )(n)(f) = f(n) for all n ∈ D_e and
all f ∈ D_s . We can obtain a model with denumerable basic domains if we
let Ds be the set of all functions f : N → N such that f (n) 6= 0 for finitely
many n and define De and I(V ) as before.

6 The Translation

We are now in the position to define the promised translation of our pro-
gramming language into the second-order part of classical type logic. We
shall give it in three installments, translating terms and formulas first and
programs and correctness formulas afterwards. We assume that V AR_e is
enumerated by the natural numbers. In the following definition arithmetical
terms N translate as terms of type s → e and formulas F translate as terms
of type s → t.

Definition 12 (Translation of Terms and Formulas)

Most clauses in this definition are self-explanatory; but note that in (3)
variables x are translated as the values of registers and that quantification

14

<<   11   12   13   14   15   16   17   >>

More intriguing information