Notational considerations and the relational calculus

Notational considerations and the relational calculus

W.H.J. Feijen and A.J.M. van Gasteren -and others- wrote the exchange rules of the relational calculus

(0a) the left-exchange

$$ [ x; y \Rightarrow z ] \equiv [ 7 2; \sim y \Rightarrow \sim x ] $$

( ${ob}$ ) the "right-exchange"

$$ [ x; y \Rightarrow z ] \equiv [ \sim x; \neg z \Rightarrow \neg y ] $$

The appeal to an exchange rule of the above form is often followed or preceded by shunting or taking the contrapositive. Rutger M. Dgkstra realized that these manipulations are caused by the fact that the implication is an asym- metric way of writing the disjunction, but instead of writing $[i(x;y)\lor z]$ , which would have introduced a negation in front of the composition, he pushed that negation as far to the outside as he could. After the introduction of the "somewhere operator" () , which is the conjugate of the "everywhere operator" $\langle x\rangle \equiv \neg [1x]$

he formulated the exchange rules

[\left\langle {x,y \land z}\right\rangle \equiv \left\langle {z,y \land x}\right\rangle ] [\left\langle {x,y \land z}\right\rangle \equiv \left\langle {\sim x;\sim y \land y}\right\rangle ]

For a number of calculations this was a con-

siderable improvement.

Formulae (0) tell us that equations

$$ x: [ x; y \Rightarrow z ] \quad a n d \quad y: [ x; y \Rightarrow z ] $$

For the weakest solution of the former, C.A.R. Hoare and He Jifeng introduced y\z and for the weakest solution of the latter $z/x$ . R.C. Backhouse interchanged the role of \ and /, and everybody -Hoare and He Jifeng included-agreed that this was an improvement. The / (read: "over") and \ (read: "under") are now introduced by the"Factorization rules"

$$ \begin{array}{l} (2 a) \quad [ x; y \Rightarrow z ] \equiv [ x \Rightarrow 2 / y ] \ (2 b) \quad [ x; y \Rightarrow z ] \equiv [ y \Rightarrow x \backslash z ] \ \end{array} $$

Instantiating these definitions with

$x = {2/9}$ and $y = x \cdot z$ respectively,we get the "cancellation rules"

$$ \begin{array}{l} (3 a) \quad [ (z / y); y \Rightarrow z ] \ (3 b) \quad [ x; (x \backslash z) \Rightarrow z ] \ \end{array} $$

In the above form, the cancellation rules have an undeniable appeal, but so far, I and I are only part of nomenclature -viz. a way of writing the weakest solutions of special types of equations. The / and \ can only contribute really, provide we know their properties, but which? To quote R.M.Dykstra "The number of

lemmas that can be formulated about factors is vast. I will refrain from listing them because the properties of "under" and "over" are much less nice than those of composition and -given the latter- factors are in fact redundant."

The above-mentioned redundancy can be made more explicit by applying to (a) the contra-positive:

$$ \begin{array}{l} [ x; y \Rightarrow z ] = [ x \Rightarrow \neg (\neg z; \sim y) ] \ [ x; y \Rightarrow z ] \equiv [ y \Rightarrow \neg (\sim x; \neg z) ] \ \end{array} $$

Comparing these formulae with (2), we conclude

(4a) $\left\lbrack {z/y \equiv \neg \left( {{72} + {7y}}\right) }\right\rbrack$ [\left\lbrack {x \backslash z \equiv \eta \left( {{\nu x};{\eta z}}\right) }\right\rbrack ]

Observing all the above, we see that R.M. Dgkstra introduced the somewhere operator and that Hoare, He Jifeng introduced, and Backhouse maintained "over" and "under", all because no one knew how to negate a composition.

Before pursuing the above line of thought, we turn for a moment to our unary operators and their notation. Tarski denotes negation

by an "over bar", so that , for instance, de Morgan's law can be rendered by

$$ [ \overline {{x \wedge y}} = \overline {{x}} \vee \overline {{y}} ] $$

The attraction of this notation is that it in- introduces neither the need for parentheses nor priority rules. There is the typographical disad-. vantage that the bars can get long and the formulae high - I quote from a report I recently received the following formula

$$ \overline {{x + x + \bar {x} + x + \bar {x} + \bar {x}}} + \overline {{\bar {x} + \bar {x}}} $$

there is the methodological disadvantage that it does not really generalize - it is only the line segment that tends itself nicely to ex- tension - , and finally the fundamental dis- advantage that there is -at least to the best of my knowledge - no manageable formalism (like BNF) for the definition of such multi-dimensional syntaxes. Hoare and He Jifeng stick to Tarski's over bar, R.C. Backhouse adopts the convention of the prefix "7" with a binding power higher than "j".

Then there is the transposition. Tarski uses the "over cup", so that its being an involution can be rendered by

$$ [ \stackrel {y} {x} = x ] \quad , $$

but the rendering of $\left\lbrack {\sim \left( {x,y}\right) \equiv {\sim y};{\sim x}}\right\rbrack$

requires the stretched cup:

$$ [ \overline {{x ; y}} \equiv \overline {{y ; x}} ]. $$

Hoardie and He Jifeng define $\overline{\mathbf{R}} = \overline{\mathbf{R}} \backslash \overline{\mathbf{I}}$

and then use the right-hand side in their calculations - I quote , for instance,

$$ (\overline {{Q}} \backslash \overline {{I}}) \subseteq \overline {{((\overline {{R}} \backslash \overline {{I}}) \backslash (\overline {{P}} \backslash \overline {{I}})) \backslash \overline {{I}}}}; $$

I think that we can agree that here something went wrong. Commutation with negation can

be rendered by

$$ [ \stackrel {\sim} {x} = \stackrel {\sim} {x} ] $$

Because transposition commutes with negation, Backhouse opts for a postfix cup.

Commutatior can now be rendered by

$$ [ (7 x) u \equiv 7 (x u) ] \quad , $$

i.e. for the combination of the two we get

by mere omission of the parentheses the unique form 7x, whereas , so far, have to choose between ~1x and 7~x

An alternative way of avoiding this choice is the introduction of a third operator.

Denoting it by " / " and calling it " mirror ", we can define it by

$$ [ / / x \equiv \sim 7 x ] \tag {5} $$

We give it the same high binding power as $\sim$ and 7 .

In EWD982 "Relational Calculus according to ATAC", the remark was already made that when you have 2 commuting involutions, you have a 3rd, in particular, with the triple $(\alpha ,\beta ,\gamma)$ any permutation of the triple $(7,\sim ,\parallel)$ , we have

$$ [ \alpha \alpha x \equiv x ] a n d [ \alpha \beta x = \gamma x ] f o r a l l x, $$

From which it follows that we never need to apply more than one of them. The introduction of can be defended on the grounds that it does justice to the underlying symmetry between the three operators.

After this interlude on the operator " , we continue our considerations triggered by "some- where ", "over", and "under". It is quite possible to negate a composition! As a matter of fact, Tarski has shown us how to do it: introduce a new operator for the conjugate of the composition. We call it the "confrontation" and denote it by an infix "1" that we give the same binding power as the ";". As conjugate of composition, confrontation, defined by

$$ (6) \qquad [ x! y \equiv \neg (\neg x; \neg y) ] \qquad , $$

is associative - is universally conjunctive in both arguments

• has $\neg J$ as its neutral element.

Moreover, we have now the "vocabulary" to describe how our three unary operators interact with composition and with con- frontation:

(7) $\left\lbrack {7\left( {x,y}\right) \equiv 7 \times 1,{7y}}\right\rbrack$

$$ \begin{array}{l} [ \sim (x; y) \equiv \sim y; \sim x ] \ [ \parallel (x; y) \equiv \parallel y! / / x ] \ [ \neg (x; y) \equiv \neg x; \neg y ] \ [ \sim (x!, y) \equiv \sim y!, \sim x ] \ [ / / (x!, y) \equiv / / y; / / x ] \ \end{array} $$

Instead of R.M. Dykgstra's exchange rules (1) with the "somewhere operator", we can now write

[\left\lbrack {x,y \sim z}\right\rbrack \equiv \left\lbrack {z,{ny} \sim x}\right\rbrack ] (8b) $\left\lbrack {x!{y}^{v}z}\right\rbrack \equiv \left\lbrack {{\sim x}!{z}^{v}{y}^{r}}\right\rbrack$

Moreover, we have now a shorter definition of "over" and "under": instead of (4) we could now write

(9a) $\left\lbrack {2/y \equiv z,\therefore y}\right\rbrack$ [\left\lbrack {x \backslash z \equiv /x!,z}\right\rbrack ]

and the factorization and cancellation rules (2)

and (3) can be rewritten accordingly, e.g.

$$ (1 0 a) \qquad [ x; y \Rightarrow z ] \equiv [ x \Rightarrow z! / / y ] $$

$$ (1 0 b) \quad [ x; y \Rightarrow z ] \equiv [ z \Rightarrow 1 1 x! y ]. $$

and instantiations like

$$ [ (z!, \prime \prime y); y \Rightarrow z ] $$

$$ [ x \Rightarrow (x; y)!, / / y ] $$

Formulae (9) suggest to me to forget about "over" and "under" and to trade them for "mirror" and "confrontation." I ended EWD 1136 with the suggestion of "a systematic study of how we can manipulate with / and \". Some results already emerge. For instance, when we ask ourselves how associative / is -it isn't - we find

$$ [ (x / y) / z \equiv x / (z; y) ] $$

which is nothing but the associativity of ! in disguise. This obfuscation is very similar to the complications of the contrapositive and shunting, where the implication sign has disguised the associativity of the disjunction.

*

When I introduced the conjugate of the compo-sition into my calculations, I was temporarily unaware that Tarski had already introduced the operator. David A. Naumann reminded me of it.

Tarski called the composition "relative multiplication" and the confrontation "relative addition". He denoted the former, like us, by " $\vdots$ " and, in a graphical pun, the latter by " $\frac{1}{3}$ ". It is surprising to see that Tarski's "relative addition" was ignored and "over" and "under" were introduced, as all the people involved knew Tarski's article. Under the assumption that trading / and \ For and , is a manipulative simplification -and, to say the truth, I am almost certain it is-, I can only think of the following explanations.

(i) People don't really manipulate with / and \, i.e. $2 / y$ and $x\backslash z$ are more notahons for the weakest solutions of two special equations -as exemplified by factorization and cancellation rules- than that / and $\backslash$ are viewed as operators with pleasant properties. (ii) The lack of $\parallel$ for $\sim$ made $\mu$ and more effective abbreviations. (iii) People were put off -and rightly so- by Tarski's misleading terminology: the analogy with arithmetic is too shallow. (Of course, / and \ are also inspired by arithmetic analogy; the analogy makes me suspicious, but I have seen others attracted by it.)

(iv) With $\frac{3}{2}$ , Tarski chose the wrong symbol. I first used $\phi$ , and that worked, but then I realized that I did not have a role for its obvious partner $d$ , so I switched to $\phi$ , and that worked too. After D.A. Naumann had reminded me that my invention had been anticipated by Tarski, I felt that the least I could do was to use Tarski's symbol, but, no matter how hard I tried, it did not work. (I tried a smaller $t$ , e.g. $\frac{3}{2}$ , but still the symbol was too big for its high binding power. For formulae with Tarski's symbol, I found no way of spacing that my hand-eye coordination could adopt, I gave up and, upon analysis of my difficulties, decided to try!.) About the shape of the character // for "mirror" I still have doubts.

Austin, 5 November 1992

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 USA