Program Semantics and Classical Logic

[Pi∕Xi]ihYk ^ Qkim=ι(Q) = hZk ^ Qkim=1(Q⁰), where Zι,...,Zm
are fresh, Q⁰_k abbreviates

[Pi∕Xi]i [Z'∕Y'↑m=ι Qk and Q⁰
abbreviates [Pi∕Xi]i [Z'/Y']m=₁ Q

An alternative notation for [Pi/Xi]_iⁿ₌₁P is [P1/X1 , . . . , Pn/Xn]P. The follow-
ing lemma is standard and has a straightforward proof.

Lemma 1 If {X₁,..., X_n} ∩ {Y₁,..., Y_m} = 0 and Y₁,..., Y_m are not free
in P₁ , . . . , P_n, then

[Pi/Xi]iⁿ=1[Qk/Yk]k^m=1P= [[Pi/Xi]iⁿ=1Qk/Yk]k^m=1[Pi/Xi]iⁿ=1P

3 A Computational Calculus

Let us call a program which consists only of a sequence of assignments x :=
N , tests B ? and program variables X linear, so that the class L of linear
programs is given by

L ::= A |   L₁; L₂

We present a simple calculus C characterising a derivability relation 'C on
the set of programs. The idea is that if L 'C P holds for some closed L, then
an execution of the deterministic L will count as one possible execution of
the possibly indeterministic P. Conversely, any execution of P will be an
execution of some L such that L 'C P. The rules of the calculus are the
following.

P₁ U P₂ ⁱ ∈ ^{{1, 2}}

[hXi ^ Piin=ι(Pι)∕Xι,..., hXi ^ Piin=ι(Pn)∕Xn]P
hXi ^ Piin=ι(P)

The idea behind these rules is that bottom-up they can be read as rules for
executing a program. Executing P₁ U P₂ consists of executing P₁ or executing
P₂ and an execution of hX_i ^ Pi)n=₁(P) consists of replacing all procedure
calls Xk in P by their bodies Pk , but so that further procedure calls in Pk
are still bound by the delarations in hX_i ^ Piin=₁. This means that we have
to substitute the X_k in P simultaneously by hX_i ^ Piin=₁ (P_k). Viewed in

<<   4   5   6   7   8   9   10   >>

More intriguing information