More pointless relational calculus: the transitive closure

Introductory Remark In this note we shall use that equation $Y: [P, Y \Rightarrow Y]$ has a unique strongest solution for monotonic $f$ . The theorem of Knaster-Tarski, viz. that this strongest solution is also $f$ 's strongest fixpoint, will not be used.

Instead of $\left\lbrack {A \vee B} \Rightarrow C\right\rbrack$ we shall mostly write the equivalent $\left\lbrack {A \Rightarrow C}\right\rbrack \land \left\lbrack {B \Rightarrow C}\right\rbrack$ . (End of Introductory Remark.)

The transitive closure of $R$ can be defined as the strongest solution of

or of $\begin{array}{l} Y \colon \left\lbrack {\mathcal{R} \vee {\mathcal{R}}{;}\mathcal{Y} \Rightarrow \mathcal{Y}}\right\rbrack \ Y \colon \left\lbrack {\mathcal{R} \vee {\mathcal{Y}}{;}\mathcal{Y} \Rightarrow \mathcal{Y}}\right\rbrack \end{array}$

Legend a The semicolon ", " is given a binding power between dis/conjuncti on and the unary $n$ ?/""(End of Legend a.)

One of the purposes of this note is to demonstrate the equivalence of these two definitions, i.e. to prove $[Q \equiv S]$ , where $Q$ and $S$ are given by

$(0a)$ $R \Rightarrow Q]$ $(ob)$ $R;Q\Rightarrow Q]$

(1) $\left\lbrack {R \Rightarrow Y}\right\rbrack \land \left\lbrack {R;Y \Rightarrow Y}\right\rbrack \Rightarrow \left\lbrack {Q \Rightarrow Y}\right\rbrack \;\left( {a \Vdash Y}\right)$ (2a) $\left\lbrack {R \Rightarrow S}\right\rbrack$ (2b) $\left\lbrack {S;S \Rightarrow S}\right\rbrack$ (3) $\left\lbrack {R \Rightarrow Y}\right\rbrack \land \left\lbrack {Y;Y \Rightarrow Y}\right\rbrack \Rightarrow \left\lbrack {S \Rightarrow Y}\right\rbrack \;\left( {allY}\right) .$

Proof The proof of. $[Q\equiv S]$ is -not sur- prisingly-by mutual implication.We observe

$$ [ Q \Rightarrow S ] $$

$\Leftrightarrow { \left( 1\right)$ with ${Y}_{i} = S}$

$$ [ R \Rightarrow S ] \land [ R; S \Rightarrow S ] $$

[\left( {{ \text{monotonicity of }} ;3}\right) ]

$$ [ R \Rightarrow S ] \land [ S; S \Rightarrow S ] $$

$= \left{ {\left( {2a}\right) \text{ and }\left( {2b}\right) }\right}$

$$ [ S \Rightarrow Q ] $$

[\left( 3\right) \text{with}{Y}_{i} = Q} ]

$$ [ R \Rightarrow Q ] \land [ Q; Q \Rightarrow Q ] $$

$$ = {(\mathbf {0 a}) } $$

$$ [ Q; Q \Rightarrow Q ] $$

$= \left{ \left( {ob}\right) \text{ and }\left( 1\right) ,\text{ see Lemma below }\right}$ true

(End of Proof.)

In the pointless relational calculus, transitivity is expressed by

$$ (X \mathrm {i s t r a n s i t i v i t y}) \equiv [ X; X \Rightarrow X ] $$

From the definition of $S$ - see (2b). It follows immediately that $S$ is transitive. Our remaining obligation is to show that $Q$ is transi-

Lemma Relation Q, given by (0) and (1), satisfies $\left\lbrack {Q;Q \Rightarrow Q}\right\rbrack$ .

Proof We observe for any $z$

$$ [ Q; Q \Rightarrow Q ] $$

$\Leftrightarrow {$ monotonically ${of}}$

$$ [ Z; Q \Rightarrow Q ] ^ {\wedge} [ Q \Rightarrow Z ] $$

In order to facilitate the establishment of

the second conjunct we choose the weakest $z$ satisfying the first conjunct. We observe

$$ \begin{array}{l} [ Z; Q \Rightarrow Q ] \ = {\mathrm {l e f t - e x c h a n g e} } \ [ \neg Q; \sim Q \Rightarrow \neg Z ] \quad , \ \end{array} $$

from which we conclude that the weakest Z - i.e. the strongest 72- satisfies

(4) $\left\lbrack {\neg Z \equiv \neg Q; \sim Q}\right\rbrack$

In order to demonstrate $\left\lbrack {Q \Rightarrow 2}\right\rbrack$ for $Z$ given by (4) we observe

$$ [ Q \Rightarrow Z ] $$

$\Leftrightarrow \;{ \left( i\right)$ with $Y \mathrel{\text{:=}} Z}$

$$ [ R \Rightarrow Z ] \land [ R; Z \Rightarrow Z ] $$

$= {$ contrapositive; right-exchange $}$

$$ \begin{array}{l} [ \neg Z \Rightarrow \neg R ] \land [ \sim R; \neg Z \Rightarrow \neg Z ] \ = {(4), 3 \mathrm {t i m e s} } \ [ \neg Q; \sim Q \Rightarrow \neg R ] \land [ \sim R; \neg Q; \sim Q \Rightarrow \neg Q; \sim Q ] \ \Leftrightarrow {\mathrm {m o n o t o n i c i t y} o f; } \ [ \sim Q; \sim Q \Rightarrow \neg R ] \land [ \sim R; \neg Q \Rightarrow \neg Q ] \ = {\mathrm {l e f t - e x c h a n g e}; \mathrm {r i g h t - e x c h a n g e} } \ [ R; Q \Rightarrow Q ] \wedge [ R; Q \Rightarrow Q ] \ = {(\mathrm {o b}) } \ t r u e. \ \end{array} $$

(End of Proof.)

The above proof contains a 1-bit rabbit: instead of defining Z as we have done, we could have tried the weakest Z satisfying $[Q;Z\Rightarrow Q]$ . Such was indeed my first effort; it would have been the correct choice, had (ob) been replaced by. $[\mathbb{Q};\mathbb{R}\Rightarrow \mathbb{Q}]$ . The introduction of Z may have come as a surprise, but I think that, upon closer scrutiny, it does not qualify as a rabbit: we have to show that Q;Q implies something, and, composition being monotonic, we have to use (i), i.e. we have to exploit the circumstance under which we can conclude that Q implies something; that latter something we called Z.

The definition of the transitive closure of $R$ as the strongest S satisfying (2) can be read as "the strongest transitive relation implied by $R^*$ . It is better disentangled than the

definition of $Q$ ,since in (0) both conjuncts refer to $R$ . Moreover,(2) does not confront us with the dilemma how to compose with $R$ .

Compare the situation with the syntactic definition of <word> ; here we have the analogous three options

$$ < w o r d > := < l e t t e r > | < l e t t e r > < w o r d > $$

$$ \langle w o r d \rangle : := < l e t t e r > | < w o r d > < w o r d > $$

$$ \langle w o r d \rangle : := < l e t t e r > | < w o r d > < l e t t e r > $$

The middle one, though leading to an ambiguous grammar, may have advantages. Stronger, its ambiguity could be its virtue: we can blame a grammar for its ambiguity or praise it for not being overspecific.

Inks Lake State Park

28 November 1991

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

PS. See also EWD945.