*Yesterday was Turing's 99th birthday. By coincidence, we had a treat at Queen Mary — a talk by C.A.R. Hoare. This is a very brief summary of what was said.*

Consider an algebra whose variables range over (possibly non-deterministic) programs:

- $p;q$ denotes the sequential composition of $p$ and $q$
- $p*q$ denotes the parallel composition of $p$ and $q$

- $p \le q$ means that all possible executions of $p$ are also possible executions of $q$

Several obvious properties follow from our intuition of what programs are, so we choose to make them axioms.

- $*$ is commutative: $p*q=q*p$
- $*$ and $;$ are associative: $(p\circ q)\circ r = p\circ(q\circ r)$, where $\circ$ stands for $*$ or $;$
- $\le$ is a partial order
- $*$ and $;$ are monotonic: if $p\le p'$ and $q\le q'$, then $p\circ q\le p'\circ q'$
- the exchange law: $(p*q);(r*s) \le (p;r)*(q;s)$
- the empty program $\varepsilon$ is an identity for both $*$ and $;$

Now it is possible to *define* Hoare triples as follows.
$$\{p\}\,q\,\{r\} \;\;=\;\; p;q \le r$$
The fun begins: Several axioms of Hoare triples follow from the algebra. For example, the rule of consequence
$$p'\le p\quad\text{and}\quad\{p\}\,q\,\{r\}\quad\text{and}\quad r\le r'\qquad\text{imply}\qquad \{p'\}\,q\,\{r'\}$$
is true because
$$
\begin{align}
&\{p'\}\,q\,\{r'\}\\
=& p';q \le r'\\
\Leftarrow& p';q \le r \land r \le r' \\
\Leftarrow& p' \le p \land p;q \le r \land r \le r' \\
=& p' \le p \land \{p\}\,q\,\{r\} \land r \le r'
\end{align}
$$

By symmetry, there are other triples one might wish to define. $$\begin{align} &p\le q;r \\ &p;q\ge r \\ &p\ge q;r \end{align}$$ It turns out that two of these lead to laws associated with Plotkin triples (reduction in structural operational semantics) and, respectively, Dijkstra triples (`going backwards'). The other triple is new.

In summary, this algebra acts as a meeting point for various approaches to defining semantics for languages.

To see what are the consequences of the exchange law, how weakening the axioms allows various useful models, and a lot more see: C.A.R. Hoare, A. Hussain, B. Moller, P.W. O'Hearn, R.L. Petersen, Struth, *On Locality and the Exchange Law for Concurrent Processes*.

## No comments:

## Post a Comment

Note: (1) You need to have third-party cookies enabled in order to comment on Blogger. (2) Better to copy your comment before hitting publish/preview. Blogger sometimes eats comments on the first try, but the second works. Crazy Blogger.