Program Semantics and Classical Logic

Remark on notation. The sequence operator “;” is associative, both on its
intuitive interpretation (Pi; P2 meaning “do Pi and then P2”) and given the
semantics (relational composition) it gets in this paper and elsewhere. We
shall also make no syntactic distinction between (Pi; P2); P3 and Pi; (P2; P3)
and write both as P_i ; P₂; P₃. Similarly, we syntactically identify P with
skip; P and with P;skip. This is allowed because skip intuitively means
“do nothing” and will be interpreted formally as the diagonal relation {hi, ii |
i is a state}. The identification will allow us to say that the programs Pi ; P
and P; P2 , as well as the program P, have the form Pi ; P; P2: we can take
P_i or P₂ or both to be the identity element skip.

An occurrence of a program variable Y ∈ {X_i , . . . , X_n} is free in a program
P if it does not occur within a subprogram of the form hX_i ^ Piin=₁(P0) in
P . A program is closed if it contains no free program variables.

Our procedure declarations can bind a series of program variables simul-
taneously, and since procedure declarations may make mutual calls it will not
be possible to reduce this form of binding to an iteration of bindings, as it
can usually be done in logic. Since we shall also have occasion to work with
simultaneous substitutions, things threaten to get a bit complicated. The
following definition may look a bit hairy, but in fact gives a straightforward
generalisation of the usual notion of substitution.

Definition 3 (Substitution) The simultaneous substitution [P_i/X_i]_iⁿ₌₁P
of P₁ for X₁ and . . . and P_n for X_n in P (abbreviated as [P_i/X_i]_iP) is defined
as follows.

[Pi/Xi]iXk = Pk, if 1 ≤ k≤n

[Pi/Xi]iA = A, ifA∈/ {X1,...,Xn}

[Pi/Xi]i(Q1; Q2) = [Pi/Xi]i Q1; [Pi/Xi]iQ2

[Pi∕Xi]i(Qι ∪ Q₂) = [P_t∕Xi]i Qi ∪ [Pi∕Xi]i Q2

<<   3   4   5   6   7   8   9   >>

More intriguing information