Another forced ping-pong argument?

Another forced ping-pong argument?

I owe the following theorem to Rutger (see [0]): for any relation $f$ (0) $\left\lbrack {f;\neg J \equiv \neg f}\right\rbrack \equiv \left\langle {\forall y : \left\lbrack {f;\neg y \equiv \neg \left( {f;y}\right) }\right\rbrack }\right\rangle$

I think this quite a remarkable theorem. The right-hand side expresses that the preFix operators " $f_{j}$ " and " $j$ " commute, i.e. that the functions $(f_j)_0$ (7) and (7) $0$ (f); are the same; the left-hand side only expresses that these two functions yield the same value when applied to $J$ .

Now the crucial observation is that at both sides an expression monotonic in $f$ equivales an expression antimonotonic in $f$ . Mutual implication turns such equivalences into monotonic and anti-monotonic conjuncts; (0) can be rewritten as

(1) $\left\lbrack {\neg f \Rightarrow f;\neg J}\right\rbrack \land \left\lbrack {f;\neg J \Rightarrow \neg f}\right\rbrack$

$$ \langle \forall y: [ \neg (f; y) \Rightarrow f; \neg y ] \rangle \land \langle \forall y: [ f; \neg y \Rightarrow \neg (f; y) ] \rangle $$

and now it stands to reason to try to equate the two monotonic conjuncts and to equate the two antimonotonic conjuncts, i.e. to prove separately

(2) $\left\lbrack {\neg f \Rightarrow f;\neg J}\right\rbrack \equiv \left\langle {\forall y : \lbrack \neg \left( {{f}{;}y}\right) \Rightarrow {f}{;}y}\right\rbrack$ $\left\lbrack {f;{7}^{3} \Rightarrow f}\right\rbrack = \left\langle {\forall y : \left\lbrack {f;{7}^{3} \Rightarrow f}\right\rbrack \Rightarrow \left( {f;y}\right) }\right\rangle$

This, indeed, can be done and for the sake of completeness we include the two proofs

Proofs We observe for any $f$

$$ \begin{array}{l} \langle \forall y: [ \neg (f; y) \Rightarrow f; \neg y ] \rangle \ = {\mathrm {p r e d . c a l c .} } \ \langle \forall y: [ f; y, v f; v y ] \rangle \ = {\mathrm {r e l . c a l c .} } \ \langle \forall y: [ p; (y, v, v y) ] \rangle \ = {\text {p r e d . c a l c .} } \ \langle \forall y: [ p; (j \vee \neg j) ] \rangle \ = {p r e d. c a l c., r a n g e o f y n o n - e m p h y } \ [ f; (Y \vee \neg J) ] \ = {\mathrm {r e l . c a l c .} } \ [ f \vee f; i ] \ = {\mathrm {p r e d . c a l c .} } \ [ \neg f \Rightarrow f; \neg J ] \ \end{array} $$

$$ \begin{array}{l} a n d \ \langle \forall y: [ f; \neg y, \Rightarrow \neg (f; y) ] \rangle \ = {\mathrm {r e l . c a l c .} }. \ \langle \forall y: [ \sim f; f; y \Rightarrow , y ] \rangle \ = {f \Rightarrow \mathrm {i n s t .} y := J } \left{\Leftarrow \mathrm {m o n o t o n i c i l y o f}; \right} \ [ \sim f; f \Rightarrow J ] \ = {\text {r e l . c a l c .} } \ [ f; \neg J \Rightarrow \neg f. ] \quad (E n d o p P r o o f s.) \ \end{array} $$

The reason for writing this note is to point out that the transition from (1) to (2) $\land$ (3), though "it stands to reason" and usually seems sound heuristics, is less forced than I had expected (and hoped) to be. Look at the following examples.

Suppose that for some $p$ and $q$ ,we have to prove for any real $x$

$\left( 4\right) \;3 \leq x \land x \leq {10} \equiv p \leq x \land x \leq q\;\left( {{mod}\;p - q = 1}\right)$

Viewing $\left\langle {\forall x : \left( 4\right) }\right\rangle$ as an equation in $p,q,\;\left( {p,q}\right) = \left( {3,{10}}\right)$ is its only solution, and , hence,we can replace the proof obligation (4) by the obligation to show that for any $x$

$\Rightarrow p \leq x$ (6) $x \leqslant 10 \equiv x \leqslant 10$

i.e. we equate the monotonic conjuncts and, separately, the antimonotonic ones.

But suppose now that, instead of $\left( 7\right) \;x \leq 3\; \land {10} \leq x \equiv x \leq p\; \land q \leq x$

Replacing this analogyously by the

[\left( \delta \right) \times {53} \equiv \times 5p] (9) ${105} \times \equiv q \leq x$

gives a much stronger obligation

$$ \begin{array}{l} s i n c e \ \langle \forall x: (7) \rangle \equiv p < q \ \end{array} $$

Currently I don't see how to express that (1) is more like (4) than like (7).

[0] Rutger M. Dgkstra, Relational Calculus and Relational Program Semantics, CS-R9408, Department of Mathematics and Computing Science of the University of Groningen.

Austin, 3 January 1995

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