Incremental sorting once more

Incremental sorting once more

This is a summary of the findings of the ATAC session of 24 September 1985, at which we tackled the completeness question raised at the end of EWD937. Eventually we found a completeness result of the type we had been looking for, thanks to a simplification introduced by Ted Herman.

As before we consider a directed graph, whose nodes are vertices and whose arrows are solid or dotted, such that no two dotted arrows are incident.

With precondition $P\left( {0,given by}\right)$

${P}_{0} : \;\left( {\underline{\mathrm{A}}\xi ,n : \xi \rightarrow n\text{ occurs in the graph: }5 \leq n}\right)$

we consider the statement $S$ given by

S: (1) $\xi ,n : \xi \rightarrow n$ occurs in the graph: ord. $\xi ,n$ )

where I I stands for potenitally concurrent execution and ord is for the purpose of this discussion most conveniently defined by

$$ \operatorname {o r d}. x. y = x, y := (x \min y), (x \max y) $$

In the following we shall develop the complete rules for the determination which of the inequalities of $P_0$ are maintained by $S$ , a question we rephrase as "which solid arrows are maintained."

A solid arrow is said to have an "incidence" for every dotted arrow with which it has an endpoint in common. The "dual" of a graph is formed by inverting the direction of every arrow in the graph.

Incidences are of two kinds, "harmless" ones and

"dangerous" ones.

Theharmlessonesare and its dual

Lemma 0 Solid arrows without dangerous incidences are maintained.

Proof In the following case analysis we represent the solid arrow $x \rightarrow y$ with all its incidences and form - with the axiom of assignment the weakest precondition of $x \leq y$ under the ord operations indicated, and show that it is implied by $x \leq y$

(i) $x \rightarrow y\;\left( {x \leq y \Leftrightarrow x \leq y}\right)$ (ii) $x \rightarrow y \Leftrightarrow z\;x \leq \left( {y\max z}\right) \Leftrightarrow x \leq y$ (iii) $u \in - x \rightarrow y$ dual of (ii) (iv) $u \Leftarrow x \rightarrow y \leftarrow z \quad \left( {u\min x}\right) \leq \left( {y\max z}\right) \Leftarrow x \leq y$

(End of Proof)

On account of Lemma 0 we only need to check solid arrows with dangerous incidences. We have three cases to distinguish (A) the dangerous incidence is the solid arrow's only one: $x \rightarrow y \rightarrow z$ (and its dual ← ← - )

$$ x \leq (y \min z) $$

$$ = {\mathrm {a r i t h m e t i c} } $$

$$ x \leq y, \land x \leq z $$

$$ = {\mathrm {t r a n s i t i v i l y} o f \leq 3 $$

$x \leq y \land$ (the graph contains a solid path from $x$ to 2).

(B) the solid arrow has one dangerous incidence and one harmless one: $u \leftarrow x \rightarrow y \rightarrow z$ (and its dual

there is a solid path from u to z or from

$$ \begin{array}{l} (u \min x) \leq (y \min z) \ = {\mathrm {a r i t h m e t i c} } \ (u \leq y \vee x \leq y) \land (u \leq z \vee x \leq z) \ = {\mathrm {s i n c e} x \leq y } \ (u \leq z \vee x \leq z) \ = {\mathrm {t r a n s i t i v i t y} f \leqslant 3 \ \end{array} $$

Combining (A) and (B) - dealing exhaustively

Lemma 1 Let solid arrow $x \rightarrow y$ have its only

(solid arrow $x \rightarrow y$ is maintained under $S$ ) $\equiv$

$\left( {x \rightarrow y \rightarrow z\text{ occurs in a subgraph of the form }\right. }$

or of the form

where $a \rightarrow b$ denotes a solid path from $a$ to $b$ ) (And its dual.)

We are left with

(C) the solid arrow has two dangerous incidenoes: $u \rightarrow x \rightarrow y \rightarrow z$ (which is its own dual)

$$ \begin{array}{l} (u \max x) _ {2} \leq (y \min z) \ = {\mathrm {a r i t h m e t i c} } \ \end{array} $$

$u \leq y \land u \leq z \land {xyz} \land x \leq 2$ $= {$ transfivity of $p \leq }$ $x \leq y \land$ (there are solid paths from $u$ to $y$ ,

Lemma 2 Let $x \rightarrow y$ have two dangerous

solid arrow $x \rightarrow y$ is maintained under $S \equiv$ $u\cdots \rightarrow x \rightarrow y\cdots \rightarrow z$ occurs in a subgraph of

My earlier mistake, which Ted Herman has undone, was that, seduced by my interest in graphs of which each solid arrow was maintained, I looked for subgraphs with the same property. Furthermore I failed to see that I only needed to embed each solid arrow with its dangerous incidences. (That I did not hit the distinction harmless/dangerous was stupid: it is invariant under arrow inversion, and the duality of theorems was something I was aware of).

The requirement that all solid arrows be maintained does not allow us to eliminate the notion of the solid path that could consist of more than 1 arrow, as there are solid paths $\left( {x \rightarrow z}\right.$ in the first,and $u \rightarrow z$ in the last diagram) that are without dangerous incidence.

This observation greatly reduces my interest in the conjecture that under the requirement of universal maintenance of all solid arrows the middle diagram may be strengthened to

This conjecture might lead to the further assumption that under maintenance of all solid arrows the diagonals in the last diagram, having dangerous incidences, should be single arrows, but that conjecture is wrong as is shown by the following theorem

Austin, 26 September 1985

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