In Praise of Algebra

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$

and

• $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.

1. $*$ is commutative: $p*q=q*p$
2. $*$ and $;$ are associative: $(p\circ q)\circ r = p\circ(q\circ r)$, where $\circ$ stands for $*$ or $;$
3. $\le$ is a partial order
4. $*$ and $;$ are monotonic: if $p\le p'$ and $q\le q'$, then $p\circ q\le p'\circ q'$
5. the exchange law: $(p*q);(r*s) \le (p;r)*(q;s)$
6. 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.