Relational Calculus according to ATAC

Relational Calculus according to ATAC

This is my personal summary of the relational calculus as it emerged at the ATAC session of 23.9.1986. Major credit is due to He Jifeng (in absentia), Tony Hoare and Wim H. Hesselink; no one but me is to be blamed for shortcomings in this text.

To begin with we introduce a prefix operator $\infty$ - read "tilde"-. It has the same -i.e. maximum-binding power as 7 ; unary prefix operators are right associative (as usual).

$$ \operatorname {A x i o m} 0 \quad [ X \Rightarrow \infty Y ] \equiv [ Y \Rightarrow \infty X ] $$

$$ \mathrm {T h e o r e m 0} \quad [ \infty f a l s e = t r u e ] $$

$$ \begin{array}{l} \mathrm {P r o o f} 0 \quad \mathrm {t r u e} \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ f a l s e \Rightarrow c o t r u e ] \ = {A x m. 0 w i t h X, Y := p o s e, t r u e } \ [ t r u e \Rightarrow \infty f a l s e ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ \infty , \mathrm {f a l s e} = \mathrm {t r u e} ] \ \end{array} $$

(End of Proof ${0}^{.})$

$$ \begin{array}{l} \mathrm {A x i o m} 1 \qquad [ X \Leftarrow \infty Y ] \equiv [ Y \Leftarrow \infty X ] \ \mathrm {T h e o r e m 1} \qquad [ \infty \mathrm {t r u e} \equiv \mathrm {f a l s e} ] \ \end{array} $$

Proof1 Similar to Proof0. (End of Proof1.)

Remark Replacing $\infty$ by 7 in the above axioms yields theorems from the predicate calculus, but please note that the negation satisfies the stronger

$$ [ X \Rightarrow \neg Y \equiv Y \Rightarrow \neg X ] \qquad a n d $$

$$ [ X \Leftarrow \neg Y \equiv Y \Leftarrow \neg X ] $$

(End of Remark)

Theorem 2 $\left\lbrack {X \equiv \sim Y}\right\rbrack \equiv \left\lbrack {Y \equiv \sim X}\right\rbrack$

$$ \begin{array}{l} \mathrm {P r o o f} 2 [ X \equiv \sim Y ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ X \Rightarrow \infty Y ] \land [ X \Leftarrow \infty Y ] \ = {A x m s, 0 a n d 1 } \ [ Y \Rightarrow \infty X ] \land [ Y \Leftarrow \infty X ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ Y \equiv \circ X ] \ \end{array} $$

(End of Proof 2.)

Theorem 3 $\left\lbrack {X \equiv \odot \odot X}\right\rbrack$

true

$$ \begin{array}{l} \mathrm {P r o o f} 3 [ X = \infty \in X ] \ = {\mathrm {T h m . 2 w i t h} Y := \infty X } \ [ \infty X \equiv \infty X ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ \end{array} $$

(End of Proof 3 .)

Next we introduce a binary infix operator, called "composition" and denoted by $\vdots$ . Its binding power is less than that of the unary operators and higher than the binary logical operators.

$$ \mathrm {A x i o m} 2 \quad [ X; (Y; Z) \equiv (X; Y); Z ] $$

In view of the associativity of composition we feel from now on free (but not obliged) to omit parenthesis pairs from continued compositions.

The next axiom introduces a constant, denoted

$$ \mathrm {A x i o m} 3 \quad [ X; Y \Rightarrow D ] \equiv [ X \Rightarrow \infty Y ] $$

$$ \begin{array}{r l} {\mathrm {T h e o r e m 4}} & {[ X _ {0}; \ldots ; X _ {1}; Y _ {0}; \ldots ; Y _ {1} \Rightarrow D ]} \ & {[ Y _ {0}; \ldots ; Y _ {1}; X _ {0}; \ldots ; X _ {1} \Rightarrow D ]} \end{array} $$

i.e. with a continued composition everywhere implying D, we are free to rotate the arguments of the continued composition: only their cyclic order matters.

$$ \begin{array}{l} \mathrm {P r o o f} 4 \quad [ X _ {0}; \dots ; X _ {1}; Y _ {0}; \dots ; Y _ {1} \Rightarrow D ] \ = {\mathrm {A x i a m 2 : w e a r e p r e e t o p l a c e p a r e n t h e s e s} } \ [ (X _ {0}; \dots ; X _ {1}); (Y _ {0}; \dots ; Y _ {1}) \Rightarrow D ] \ = {\mathrm {A x i a m} 3 } \ [ (X _ {0}; \dots ; X _ {1}) \Rightarrow \infty (Y _ {0}; \dots ; Y _ {1}) ] \ = {\text {A x i a m} 0 } \ [ (Y _ {0}; \dots ; Y _ {1}) \Rightarrow \infty (X _ {0}; \dots ; X _ {1}) ] \ = {\mathrm {A x i o m s} 3 \mathrm {a n d} 2 } \ [ Y _ {0}; \dots ; Y _ {1}; X _ {0}; \dots ; X _ {1} \Rightarrow D ] \ \end{array} $$

(End of Proof $\lambda = 1$ )

$$ \mathrm {T h e o r e m 5 a} \quad [ X \equiv X; \infty D ] $$

[\text{Proof.}{5a}\;\left\lbrack {Z \Rightarrow uX}\right\rbrack ]

$$ \begin{array}{l} = {A x i o m 3 w i t h X, Y := Z, X } \ [ Z; X \Rightarrow D ] \ = {\mathrm {T h m} 3 \mathrm {w i t h} X := D } \ [ Z; X \Rightarrow \infty D ] \ = {A x i o m 3 w i t h X, Y := (Z; X), \in D } \ [ (Z; X); \circ D \Rightarrow D ] \ = {A x i o m 2 } \ [ 2; (X; \omega D) \Rightarrow D ] \ = {A x i o m 3 w i t h X, Y := Z, (X; c o D) } \ [ 2 \Rightarrow \sim (X; \sim D) ] \ \end{array} $$

Since the equivalence between the extreme lines of the above holds for any $Z$ and $X$ , we conclude for any $X$

true

$$ \begin{array}{l} = {\mathrm {a b o v e} a b s e r v a t i o n } \ [ \sim X \equiv \sim (X; \sim D) ] \ \Rightarrow {\text {L e i b n i 2} } \ [ \infty , X \equiv \infty (X; \cap D) ] \ = {\mathrm {T h e o r e m} 3 \mathrm {t w i c e} } \ [ X \equiv (X, \circ D) ] \ \end{array} $$

(End of Proof 5a)

Remark We could similarly show that $c\mathbf{D}$ is also the left-identity element of composition, but this conclusion is postponed. (End of Remark.)

The next (and final?) axiom connects $\mathbf\eta$ and

$$ \operatorname {A x i o m} 4 \quad [ \infty (\infty X; \infty Y) \equiv \neg (\neg Y; \neg X) ] $$

$$ \mathrm {T h e o r e m 6 a} [ X \equiv \neg D; X ] $$

$$ \begin{array}{l} \mathrm {P r o o f 6 a t r u e} \ = {A x i o m 4 w i t h X, Y := \neg X, D } \ [ \infty (\infty X; \infty D) \equiv \neg (\neg D; \neg \neg X) ] \ = {\mathrm {T h m} 5 a: \mathrm {p r e d i c a t e c a l c u l u s} } \ [ \infty , X \equiv \neg (\neg D; X) ] \ = {\mathrm {T h m} 3 } \ [ \neg X \equiv \neg (\neg D; X) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ X \equiv \neg D; X ] \ \end{array} $$

(End of Proof 6a)

Remark We could similarly have shown that $\mathcal{D}$ is a right identity element of composition, but this conclusion now follows in a moment. (End of Remark)

$$ \mathrm {T h e o r e m 7} \quad [ \in D \equiv \neg D ] $$

$$ \begin{array}{l} \mathrm {P r o o f} _ {7} \quad \infty D \ = {\mathrm {T h m} G a \mathrm {w i t h} X := \in D \ \therefore D; \infty D \ = {\mathrm {T h m} 5 a \mathrm {w i t h} X := \neg D } \ \urcorner D \ \end{array} $$

(End of Proof 7)

Combining Theorems 5a, 6a and 7 , we conclude

$$ \mathrm {T h e o r e m 5} [ X \equiv X; \infty D ] \mathrm {a n d} [ X \equiv \infty D; X ] $$

Theorem 6 [X ≡ ?D; X] and [X ≡ X; ?D]

And now we are ready to show that our two unary operators commute:

Theorem 7 $\left\lbrack {{100} \times \equiv {0.17} \times }\right\rbrack$

Proof7 [1a $X \Rightarrow H$ ]

$$ \begin{array}{l} = {\text {p r e d i c a t e c a l c u l u s} } \ [ \neg H \Rightarrow \infty X ] \ = {\mathrm {A x i o m} 3 \mathrm {w i t h} X, Y := i H, X } \ [ \neg H; X \Rightarrow D ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ 1 H, 1 7 X \Rightarrow D ] \ = {p r e d i c a t e c a l c u l u s } \ [ \neg D \Rightarrow \neg (\neg H; \neg X) ] \ = {A x i o m 4 w i t h X, Y := 7 X, H } \ [ \neg D \Rightarrow \infty (\infty \neg X; \infty H) ] \ = {A x i o m 3 w i t h X, Y := \neg D, (a x _ {i} a H) } \ [ \neg D; \infty , X; \infty H \Rightarrow D ] \ = {\mathrm {T h e o r e m} 6 } \ [ \infty X; \infty H \Rightarrow D ] \ = {A x i o m 3 w i t h X, Y := c o n X, c o n H } \ [ \cos X \Rightarrow \cos H ] \ = {\mathrm {T h e o r e m} 3 } \ [ \infty X \Rightarrow H ] \ \end{array} $$

From first and last line we conclude Theorem 7, as $H$ was arbitrary. (End $P{P}{2}P{P}{3}$ )

(End of $P{r}{00}{P}{7}$ )

Theorem 8 Composition is universally disjunctive in each of its arguments, i.e.

(i) $[(E_{i:}X_{j});Y\equiv (E_{i:}X_{j};Y)]$

and

(ii) $[X;(\underline{E} i:Y_i)\equiv (\underline{E} i:X_iY_i)]$

To prove (i) we observe for any $H$

$$ [ (E _ {i}: X _ {i}); Y \Rightarrow \infty H ] $$

$$ = {A x i o m 3 } $$

$$ [ (\underline {{E}} i: X. i); Y; H \Rightarrow D ] $$

$$ = {A x i a m 3 } $$

$$ [ (\underline {{E}} i: X. i) \Rightarrow \infty (Y; H) ] $$

$$ = {\mathrm {q u a s i - d i s t r i b u t i o n c o n s e q u e n t} } $$

$$ [ (\underline {{A}} i: X. i \Rightarrow \infty (Y; H)) ] $$

$$ = {\mathrm {A x i c m} 3 } $$

$$ [ (A _ {i}: X, i; Y; H \Rightarrow D) ] $$

$$ = {A x i o m 3 } $$

$$ [ (A i: X. i; Y \Rightarrow o H) ] $$

$$ = {\mathrm {q u a s i d i s t r i b u t i o n c o n s e q u e n t} } $$

$$ [ (\underline {{E}} i: X. i; Y) \Rightarrow \infty H ] $$

and since $\sin H$ is arbitrary, (i) has been proved.

To prove (ii) we observe

$$ \begin{array}{l} [ X; (\underline {{E}} i: Y, i) \Rightarrow \in H ] \ = {A x i o m 3 } \ [ X; (E _ {i}: Y _ {i}); H \Rightarrow D ] \ = {\mathrm {T h e o r e m} 4 } \ [ (\underline {{E}} _ {i}: Y _ {i}); H; X \Rightarrow D ] \ = {\mathrm {a s a b o v e} x \mathrm {t o} x \mathrm {w i t h} X, Y, H := Y, H, X } \ \end{array} $$

$$ \begin{array}{l} [ (\bar {A} i: Y _ {i}; H; X \Rightarrow D) ] \ = {\mathrm {T h e o r e m} 4 } \ [ (A _ {i}: X; Y, i; H \Rightarrow D) ] \ = {\mathrm {A} x _ {\mathrm {i c m}} 3 } \ [ (A i: X; Y, i \Rightarrow o H) ] \ = {\mathrm {q u a s i d i s t r i b u t i o n} } \ [ (E i: X; Y, i) \Rightarrow o H ] \ \end{array} $$

and since $\omega \in H$ is arbitrary,(ii) has been proved.

(End of Proof 8)

Inspired by Theorem 7 we introduce a last unary operator, called "the converse"; we shall tentatively denote it by $\phi$ .

$$ A x i o m 5 [ \phi X \equiv - \infty X ] $$

In view of Theorem 3 - $\left\lbrack {X \equiv \propto \propto X}\right\rbrack$ ,of Theorem 7 - $\left\lbrack {\neg \infty X \equiv \neg \neg X}\right\rbrack$ - and of $\left\lbrack {X \equiv {\neg \neg }X}\right\rbrack$ we have

Theorem 9 Of the three operators $\lnot ,\infty$ ,and $\phi$

(i) each is the functional composition of the other two (ii) any pair commutes (iii) each is its own inverse

Proof is left to the reader.

Theorem 10 [Phi $X \Rightarrow Y$ ] $\equiv \left\lbrack {X \Rightarrow \phi Y}\right\rbrack$

$$ \begin{array}{l} \mathrm {P r o o f} 1 0 [ \Phi X \Rightarrow Y ] \ = {\mathrm {T h e o r e m} 9 } \ [ \sim \neg X \Rightarrow Y ] \ = {\mathrm {A x i o m} 1 } \ [ \sim Y \Rightarrow \neg X ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ X \Rightarrow 1 0 Y ] \ = {\mathrm {T h e o r e m} 9 } \ [ X \Rightarrow \phi Y ] \ \end{array} $$

(End of Proof)

Theorem 11 Operator $\phi$ is universally junctive.

Proof 11 We shall first prove that $\phi$ is universally conjunctive by observing

$$ \begin{array}{l} [ H \Rightarrow \phi (\underline {{A}} i: X, i) ] \ = {\mathrm {T h e o r e m} 1 0 } \ [ \Phi H \Rightarrow (A i: X, i) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ (\neg i: \neg H \Rightarrow X. i) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ (A i: [ \phi H \Rightarrow X. i ]) \ = {\mathrm {T h e o r e m} 1 0 } \ (\underline {{A}} i: [ H \Rightarrow 4 X. i ]) \ = {\text {p r e d i c a t e c a l u l u s} } \ [ (A i: H \Rightarrow \phi X. i) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ H \Rightarrow (\underline {{A}} i: \Phi X. i) ] \ \end{array} $$

and hence $\left\lbrack {\phi \left( {{A}{i} : X,i}\right) \equiv \left( {{A}{i} : X,i}\right) }\right\rbrack$ has been established.

Universal disjunctivity is now proved by observing

$$ \begin{array}{l} \Phi (\underline {{E}} _ {i}: X _ {i}) \ = {\mathrm {T h e o r e m} 9, \mathrm {p r e d i c a t e c a l c u l u s} } \ \lnot \mathrm {中} (\overline {{A}} _ {i}: \neg X. i) \ = {\mathrm {中 u n i v e r s a l l y c o n j u n c h i v e} } \ \lnot (\underline {{A}} i::: \Phi \lnot X _ {i}) \ = {\mathrm {p r e d i c a t e c o l u l u s}, \mathrm {T h e o r e m} 9 } \ (E i: 4 X _ {i}) \ \end{array} $$

(End of Proof 10)

Because Theorem 9- $\Phi$ commutes with $7$ , and equivalence and implication can be expressed in $\land , \lor$ and $7$ , can we take the converse of arbitrary boolean expressions by replacing all atoms by their converses.

So much for my summary of yesterday afternoon.

Austin, 24 September 1986

prof. dr. Edsger W. Dgkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712- 1188

United States of America