A sequel to EWD1241 and WF 233/AvG 141

A sequel to EWD1241 and WF233/Avg/41

In WF233/Avg141 "More about unique solutions and well-foundedness", Wim Feigen and Nelly van Gasteren have recorded a theorem and its proof which Rutger M. Dijkstra had shown them at the ETAC session of 10 December 1996. Rutger's theorem (which generalizes the results of EWD 1241) states that for left-founded relation $r$ , arbitrary relation $y$ and right-founded relation $s$ , $r; y; s$ is the unique solution of

(0) $x : \left\lbrack {x \equiv r;x \vee y \vee x;s}\right\rbrack$

(where $^ \text{本}$ denotes the reflexive transitive closure). In this note I record how in the ETAC session of 17 December 1996, the uniqueness was proved from first principles.

A formal statement of the uniqueness is as follows. Let

(1) $\left\lbrack {p \equiv r;p \vee y \vee p;s}\right\rbrack$ . (2) $\left\lbrack {q \equiv r;q \vee y \vee q;j\rbrack ,}\right.$ $\left\lbrack {h \Rightarrow k}\right\rbrack \Leftarrow \left\lbrack {h \Rightarrow k \vee {r}{i}\left( {h \land {r}{k}}\right) }\right\rbrack \left( {\forall h,k}\right) .$ $\left\lbrack {h \Rightarrow k}\right\rbrack \Leftarrow \left\lbrack {h \Rightarrow k \vee \left( {h \land {\neg k}}\right) ;s}\right\rbrack \;\left( {\forall h,k}\right) ;$

then $\left\lbrack {p \equiv q}\right\rbrack$

Remark. (3) expresses that $r$ is left-founded.

This is usually expressed by

$$ [ h \Rightarrow f a l s e ] \Leftarrow [ h \Rightarrow r; h ] (\forall h) $$

which (i) follows from (3) by instantiating

$k \mathrel{\text{:=}}$ false, and implies(3)by instantiating

$h \mathrel{\text{:=}} h \land {rk}$ . This is a general transformation.

(End of Remark.)

Before proving the above theorem, we prove - because we can use it a number of times- The following

Lemma For all $a,b,c,d$

(i) $\left\lbrack {a \Leftarrow b;d}\right\rbrack \Rightarrow \left\lbrack {a \vee b;\left( {c \land d}\right) \equiv a \vee b;c}\right\rbrack$ (ii) $\left\lbrack {a \Leftarrow b;d}\right\rbrack \Rightarrow \left\lbrack {a \vee \left( {c \land \neg b}\right) ;d}\right. \equiv a \vee c;d\rbrack$

Proof of (i) We observe

$a \vee {b}_{j}\left( {c \land \neg d}\right)$

$\left{ {\left\lbrack {a \Leftarrow b;d}\right\rbrack ,i.e.\left\lbrack {a \equiv a \vee b;d}\right\rbrack }\right.$

$a \vee {b}{i}d\;v\;{b}{j}\left( {c \land {7d}}\right)$

$= \;\left{ {\mathrm{v}\text{over};}}\right}$

$a \vee b;\left( {d\vee \left( {c \land \neg d}\right) }\right)$

$= \;\left{ {\text{pred.}\operatorname{calc}.}\right}$

$a \vee {}^{\prime }b;\left( {d \vee c}\right)$

$= \;\left{ {v\text{ over }j}\right}$

$a \vee b;d \vee b;c$

$\left{ {\left\lbrack {a \Leftarrow b;d}\right\rbrack }\right}$

$a \vee b;c$

(End of Proof of (i).)

In order to prove that $[p \equiv q]$ follows from (1) through (4), it suffices to show that the latter imply $[p \Rightarrow q]$ , as symmetry provides the other half of the proof. We observe

$$ [ p \Rightarrow q ] $$

$\Leftrightarrow \;{ \left( 3\right) \text{ with }h,k \mathrel{\text{:=}} p,q}$

$$ [ p \Rightarrow q \lor r; (p \land \neg q) ] $$

[\left{ {\left\lbrack q \Leftrightarrow r;q\right\rbrack f}\right. \text{from}\left( 2\right) ;\text{Lemma }\left( i\right) \text{with}]

$$ a, b, c, d := q, r, p, q } $$

$$ [ p \Rightarrow q \lor r; p ] $$

$\Leftrightarrow \;\left{ \begin{array}{l} \text{ (4 ) with } h,k \end{array}\right. = p,q \vee r;p$

$$ [ p \Rightarrow q \lor r; p \lor (p \land \neg q \land \neg (r; p)); s ] $$

$\equiv \;\left{ {\left\lbrack {p \Leftarrow p;s}\right\rbrack f{o}^{\prime }m}\right. \left( 1\right) ,hence\left\lbrack {r;p \Leftarrow r;p;s}\right\rbrack ;$ Lemma (ii) with $a,b,c,d = r;p,r;p,p \land {7q},s}$

$$ [ p \Rightarrow q \lor r; p \lor (p \land \neg q); s ] $$

[\left{ {\left\lbrack {q \Leftrightarrow q;s}\right\rbrack f{o}^{\prime }m\left( 2\right) ;{l}{e}{l}{m}\left( l\right) }\right. ]

$$ a, b, c, d := q, q, p, s } $$

$$ [ p \Rightarrow q \lor r; p \lor p; s ] $$

[\left( 1\right) } ]

$$ \begin{array}{l} [ y \Rightarrow q ] \ \equiv \quad {(2) } \ t r u e \ \end{array} $$

The contributions of Putger M. Dijkstra and of the ETAC are acknowledged.

Nuenen, 21 December 1996

prof. dr. Edsger W. Dgksha

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712 - 1188, USA