A note on substitution and renaming

A note on substitution and renaming

The formal definition of the semantics of the assignment statement $x \mathrel{\text{:=}} E$ uses the predicate denoted by

P _ {E} ^ {x} \qquad \mathrm {o r} \qquad P [ E / x ] \qquad ;

it is the predicate derived from $P$ by "replacing each occu-currence of $x$ in $P$ by $E$ ". In the context of the assignment statement the derived predicate is to be understood in the same state space as $P$ ; in other words, in general, $x$ occurs in $E$ . In the latter case, the substitution is a complicated operation in the sense that it both eliminates and reintroduces

Some time ago I wanted to separate those two aspects by restricting the substitution to sub-. stituting the fresh variable $x^{\prime}$ for $x$ . In that case, we have two alternative expressions for $P_{E}^{x}$ ..

\begin{array}{l} (E x ^ {\prime}: x ^ {\prime} = E \wedge P _ {x ^ {\prime}} ^ {x}) \ \left(\underset {x ^ {\prime}} {A} x ^ {\prime}: x ^ {\prime} ≠ E \vee P _ {x ^ {\prime}} ^ {x}\right), \ \end{array}

the two expressions being equivalent because -see EWD 834- $\left( {N{x}^{\prime } : {x}^{\prime } = E}\right) = 1$ . Formulation (1) has some preference because we normally deal with predicate transformers that distribute over conjunctions.

In the language fragment of "A Discipline of Program- ming", I avoided conditional expressions because, in my case, they would introduce "nondeterministic expressions" and I was not able to substitute them for a variable. Formulation (1), however, shows us the way how to do it.

The semantics of the above assignment statement

$x = E$ is equally well captured by the predicate

x ^ {\prime} = E

(Note that, since in general, $x$ occurs in $E$ ,this is a predicate on the Cartesian product of initial and final state space -the latter one being the primed one.) Denoting (2) by $Q$ ,(1) takes the form

\left(\underset {x ^ {\prime}} {A} x ^ {\prime}: ¬ Q \vee P _ {x ^ {\prime}} ^ {x}\right)

E being a "deterministic expression" is reflected by

But this is easily generalized. With the assignment statement $x \mathrel{\text{:=}} E$ we associate the predicate $Q$ -in $x$ and ${x}^{\prime }$ - such that the possible values of $E$ are precisely the roots of ${x}^{\prime } : Q$ (i.e. of $Q$ ,when viewed as an equation in ${x}^{\prime }$ ).

Example with if true $\rightarrow + 1$ Iff true $\rightarrow - 1$ for $E$ ,we find ${x}^{\prime } = 1 V {x}^{\prime } = - 1$ (or abs(x′)=1) for Q. (End of Example.)

With the above $Q$ , $wp("x:=E",P)$ is again given by (3). In other words, once we have decided to restrict substitution to "priming" or "renaming", "nondeterministic expressions" are in a limited sense given for free -limited only because (3) might be harder to manipulate.

Newcastle-upon-Tyne

Plataansstraat 5 5671 AL NUENEN The Netherlands

7 September 1982 prof. dr. Edsger W. Dgkstra Burroughs Research Fellow