A comparison of relational proofs

A comparison of relational proofs

The purpose of this note is to compare different proofs for the same theorem of the relational calculus, so that we may get some feeling for the sources of manipulative advantages and disadvantages. The theorem chosen is simple enough that it can be proved from first principles; yet I hope it is "deep" enough to make the experiment interesting.

Theorem Let $t$ be the strongest solution of

[{x}_{1} = \left\lbrack {j \vee a;x \Rightarrow x}\right\rbrack ]

i.e. -in view of Knaster-Tarski-

(0) $[J \vee a; t \equiv t]$ (1) $\left\lbrack {j \Rightarrow x}\right\rbrack \land \left\lbrack {a;j \Rightarrow x}\right\rbrack \Rightarrow \left\lbrack {t \Rightarrow x}\right\rbrack$ for all $x$ ;

let $s$ be the strongest solution of

$(x + x)$ $x:[b \vee a; x \Rightarrow x]$ 1.a.

(2) $\left\lbrack {b \vee a;s \equiv s}\right\rbrack$

$\left\lbrack {b \Rightarrow x}\right\rbrack \land \left\lbrack {a;x \Rightarrow x}\right\rbrack \Rightarrow \left\lbrack {s \Rightarrow x}\right\rbrack ;\;$ then

$\left\lbrack {s \equiv t;b}\right\rbrack$

Proof In this proof we try to find closed ex- pressions for t and s ,whereafter we es- tablish (4) by manipulating these expressions. Comparing $(\ast)$ with $(\ast \ast)$ ,we see that $(\ast)$ is obtained from $(\ast \ast)$ with for b the special choice

J; so we focus on $(xx)$ and try to find an expression for s in terms of (a,b). We observe

5

$$ \begin{array}{l} = {(2) } \ b \vee a; s \ = {(2) } \ b \vee a; (b \vee a; s) \ = {\quad ; \mathrm {o v e r} v } \ b \vee a; b \vee a; a; s \ = {(2) a n d ; o v e r v } \ b \vee a; b \vee a; a; b \vee a; a; a; s \qquad \mathrm {e t c .} \ \end{array} $$

which suggests for s the closed form, viz.

(5) $\left\lbrack {s \equiv \left\langle {\exists n : n \geq 0 : q.n;b}\right\rangle }\right\rbrack ,$ where (6) $\left\lbrack {q.0 \equiv j}\right\rbrack$ and $\left\lbrack {q.\left( {n + 1}\right) \equiv c;q.n}\right\rbrack$ for all $n$ .

To check that conjecture (5) verifies (2) we observe

$$ \begin{array}{l} b \vee a; \langle \exists n: n \ge 0: q. n; b \rangle \ = {}; o v e r \exists } \ b \vee \langle \exists n: n > 0: a; q. n; b \rangle \ = {6 } \ q. 0; b \vee \langle \exists n: n \geqslant 0: q. (n + 1); b \rangle \ = {p. c., t r a n s f o r m i n g t h e d u m m y } \ q. 0; b \vee \langle \exists n: n \geqslant 1: q. n; b \rangle \ = {p, c. } \ \langle \exists n: n \geq 0: q. n; b \rangle \ \end{array} $$

To check that conjecture (5) verifies (3) for

$$ \begin{array}{l} a n y x, w e o b s e r v e \ [ \langle \exists n: n \ge 0: q. n; b \rangle \Rightarrow x ] \ = {\mathrm {p r e d . c a l c .} } \ \langle \forall n: n \geqslant 0: [ q. n; b \Rightarrow x ] \rangle \ \Leftrightarrow {\mathrm {b y m a t h e m a t h a l i n d u c t i o n , s e e b e l o w} } \ \end{array} $$

$$ - - [ b \Rightarrow x ] \wedge [ a; x \Rightarrow x ] $$

For the mathematical induction we observe for

the base:

$$ \begin{array}{l} [ q, 0; b \Rightarrow x ] \ = {() } \ [ j; b \Rightarrow x ] \ = {\mathrm {r e l . c a l c .} } \ [ b \Rightarrow x ] \ \end{array} $$

for the step:

$$ \begin{array}{l} [ q. (n + 1); b \Rightarrow x ] \ = {6 } \ [ a; q, n; b \Rightarrow x ] \ \Leftrightarrow {[ a; x \Rightarrow x ] } \ [ a; q, n; b \Rightarrow a; x ] \ \Leftrightarrow {\mathrm {m o n o t h e n i c i l y} _ {j} } \ [ q, n; b \Rightarrow x ] \ \end{array} $$

By substituting $b \mathrel{\text{:=}} J$ we derive for $t$

(7) $\left\lbrack {t \equiv \left\langle {\exists n : n \geq 0 : q.n}\right\rangle }\right\rbrack$ ,

and now we are ready to establish (4)

$$ \begin{array}{l} s \ = {(5) } \ \langle \exists n: n \geq 0: q. n; b \rangle \ = {\quad ; \text {o v e r} \exists } \ \langle \exists n: n \ge 0: q. n \rangle ; b \ = {() \ t; b \ \end{array} $$

(End of Proof $0$

Proof 0 uses that relational composition is associative, sufficiently disjunctive and has J as its neutral element. It is the type of proof that I may have preferred 15 years ago, but now it annoys me a little, as its mathematical induction over the naturals strikes me as a foreign element.

Proof1 Here (4) is established by means of a ping-pong argument; ping is easy.

$$ [ s \Rightarrow t; b ] $$

$$ \begin{array}{l} \Leftrightarrow {3) w i t h x := +; b } \ [ b \Rightarrow t; b ] \land [ a; t; b \Rightarrow t; b ] \ \Lleftarrow {m o n o t o n i c i t y o f ; } \ [ j \Rightarrow t ] \land [ a; t \Rightarrow t ] \ = {0 } \ t r u e \ \end{array} $$

Pong uses the exchange rules, primarily to get $t$ all by itself in the antecedent position:

$$ \begin{array}{l} [ t; b \Rightarrow s ] \ = {l e f t e x c h a n g e } [ 7 s; \sim b \Rightarrow \neg t ] \ = {c o n t r a p o s i t i v e } [ t \Rightarrow \neg (\neg s; \sim b) ] \ \begin{array}{r l} {\Leftarrow} & {{(1) \mathrm {w i t h} x := \neg (\neg s; \sim b) }} \ & {[ j \Rightarrow \neg (\neg s; \sim b) ] \land [ a; \neg (\neg s; \sim b) \Rightarrow \neg (\neg s; \sim b) ]} \end{array} \ = {c o n t r a p o s i h v e; r i g h t e x c h a n g e } [ 7 s; \sim b \Rightarrow 7 J ] \wedge [ \sim a; 7 s; \sim b \Rightarrow 7 s; \sim b ] \ \end{array} $$

[\left. \left. \left. \Leftrightarrow \right} \left{ {\text{ left exchange and monotonicties }}\right} \right. ]

$= { J$ and right exchange

$$ \begin{array}{l} [ j; b \Rightarrow s ] \land [ n a; 7 s \Rightarrow 7 s ] \ [ b \Rightarrow s ] \land [ a; s \Rightarrow s ] \ = {(\mathbf {2}) } \ t r u e \ \end{array} $$

(End oPruoP1)

In a global sense, Proof 1 isn't too bad: the way in which ping uses (0) & (3) and pong uses (1) & (2) is absolutely standard, and since, say, 1985, I can write that down without thinking. There is, however, a dual problem with pong: firstly, all those negations giving rise to contrapositives that don't really contribute to the argument - Rulger M. Dijkstra's objection - and the $\sim$ , which now can be regarded as a foreign element.

Proof 2 Ping as above. For pong, we first observe that on account of monotonicities

$$ [ t \Rightarrow u ] \land [ u; b \Rightarrow s ] ^ {\prime} \Rightarrow [ t; b \Rightarrow s ] $$

In order to ease the demonstration of $[t \Rightarrow u]$ , we want to choose a weak $u$ . Fortunately, $x: [x; b \Rightarrow s]$ has a weakest solution (because ; is universally disjunctive); calling it $u$ we have

$\left\lbrack {u;b \Rightarrow s}\right\rbrack$ (9) $\left\lbrack {x;b \Rightarrow s}\right\rbrack \Rightarrow \left\lbrack {x \Rightarrow u}\right\rbrack$ for all $x$ .

And now we observe

$$ [ t; b \Rightarrow s ] $$

$$ \begin{array}{l} \Leftrightarrow {m o n o t o n i c i l i e s } \ [ t \Rightarrow u ] \land [ u; b \Rightarrow s ] \ = {(\mathbf {8}) } \ [ t \Rightarrow u ] \ \end{array} $$

$$ \begin{array}{l} \Leftrightarrow \quad {(1) \mathrm {w i t h} x := a } \ [ ] \Rightarrow u ] \land [ a; u \Rightarrow u ] \ \Leftrightarrow {(\mathrm {9}) \mathrm {w i t h} x := j, \mathrm {w i t h} x := a; u } \ [ ]; b \Rightarrow s ] \land [ a; u; b \Rightarrow s ] \ \Leftrightarrow {j a n d (8) } \ [ b \Rightarrow s ] \land [ a; s \Rightarrow s ] \ = {2 } \ \end{array} $$

true

(End of Proof 2)

formulae (8) and (9) capture in the traditional manner that $u$ is the weakest solution of $x: \left\lbrack {x;b \Rightarrow s}\right\rbrack$ . They do not capture the consequence of the fact that $\left\lbrack {x;b \Rightarrow s}\right\rbrack$ is an antimonotonic function of $x$ ,i.e. that any predicate stronger than the weakest solution solves the equation as well. We take that in account by replacing (9) by

$$ (1 0) \quad [ x; b \Rightarrow s ] \equiv [ x \Rightarrow u ] \quad f o r a l l x $$

which reduces (8) to a consequence (instan.

hate (10) with $x = u$ ).

The tradition is emerging to eliminate the identifier u and to write s/b instead - read: "s over b"- . The infix operator / is now defined by

(1) $\left\lbrack {x,y \Rightarrow z}\right\rbrack \equiv \left\lbrack {x \Rightarrow z/y}\right\rbrack \;f\left( x\right)$

(Notice the difference between (10) and (11): (10) was used to define u in terms of b and s , (11) defines the operator / .) The analogue of (8), [\left\lbrack {\left( {z/y}\right) ;y \Rightarrow z}\right\rbrack \text{for all}y,z]

becomes a consequence, known as the law of "cancelation". We can now rewrite our last calculation as follows

$$ \begin{array}{l} [ t; b \Rightarrow s ] \ = {\mathrm {d e f . o f} / } \ [ t \Rightarrow s / b ] \ \Leftrightarrow {(\mathbf {i}) w i t h x := s / b } \ [ j \Rightarrow s / b ] \land [ a; (s / b) \Rightarrow s / b ] \ = {\mathrm {d e f . o f} /, \mathrm {t w i c e} } \ [ j; b \Rightarrow s ] \land [ a; (s / b); b \Rightarrow s ] \ \Leftrightarrow {J a n d c a n c e l a t i o n + m o n o t o n i c i t i e s } \ [ b \Rightarrow s ] \land [ a; s \Rightarrow s ] \ = {2 } \ t r u e \ \end{array} $$

We could do without the step that introduced u, as the monotonicities exploited have now been captured by the introduction of

Similarly, we can define $\left{ \begin{array}{ll} \text{ } \ \end{array}\right.$ -read "under" - by

(13) $\left\lbrack {x;y \Rightarrow z}\right\rbrack \equiv \left\lbrack {y \Rightarrow x \backslash z}\right\rbrack$ with its own law of cancelation (14) $\left\lbrack {x;\left( {x/2}\right) \Rightarrow 2}\right\rbrack$

The fact that using formulae like (8) and (9) or (10) is a general technique raises the question: are the equations $x: [x; y \Rightarrow z]$ and $y: [x; y \Rightarrow z]$ so special that their solutions deserve special operators (or functions) to denote them?

(11) is of the form $[f.x\Rightarrow z]\equiv [x\Rightarrow g.z]$ i.e. the form of a Galois connection, and so is (13). Given an $p$ , the introduction of its Galois partner $g$ may be a simple way of capturing that it exists (and that $f$ is universally disjunctive), but it is most rewarding if $g$ has much nicer manipulative properties than $p$ . It looks as if the answer to the question raised can only be given by the out-. come of a systematic study of how we can manipulate with / and

Austin, 16 October 1992

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