[Pi∕Xi]ihYk ^ Qkim=ι(Q) = hZk ^ Qkim=1(Q0), where Zι,...,Zm
are fresh, Q0k abbreviates
[Pi∕Xi]i [Z'∕Y'↑m=ι Qk and Q0
abbreviates [Pi∕Xi]i [Z'/Y']m=1 Q
An alternative notation for [Pi/Xi]in=1P is [P1/X1 , . . . , Pn/Xn]P. The follow-
ing lemma is standard and has a straightforward proof.
Lemma 1 If {X1,..., Xn} ∩ {Y1,..., Ym} = 0 and Y1,..., Ym are not free
in P1 , . . . , Pn, then
[Pi/Xi]in=1[Qk/Yk]km=1P= [[Pi/Xi]in=1Qk/Yk]km=1[Pi/Xi]in=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 | L1; L2
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.
(U rule)
(ρ rule)
P1 U P2 i ∈ {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 P1 U P2 consists of executing P1 or executing
P2 and an execution of hXi ^ Pi)n=1(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 hXi ^ Piin=1. This means that we have
to substitute the Xk in P simultaneously by hXi ^ Piin=1 (Pk). Viewed in