Some simple lemmata on incremental sorting

Some simple lemmata on incremental sorting

A standard component of many in situ sorting al- gorithms is the operation ord, given by ord.x.y = if $x > y\rightarrow x,y\equiv y,x$ [] xsy→ skip fi ; it satisfies {true} ord.x.y{xsy} . (0)

For a bunch of ord operations that have no argua- ments in common, their potentially concurrent execu-tion will be indicated by a command of the form

(∥ \xi , \eta : C, (\xi , \eta): o r d, \xi , \eta)

where $C(\xi ,\eta)$ describes which pairs of variables are involved.

We shall formulate a number of lemmata by directed graphs. The variables the lemma is about are in one-to-one correspondence to the nodes of the graph that formulates the lemma. In the graph some arrows are drawn, some are dotted; no two dotted arrows have an endpoint in common. Such a graph should be read as the following sentence:

${ \left( {\underline{A},\xi ,\eta : \xi \rightarrow \eta }\right)$ occurs in the graph: $\xi ≤ \eta }$

(II $\xi ,\eta : \xi \rightarrow \eta$ occurs in the graph: ord. $\xi ,\eta$ )

$\left{ {\left( {25},n : 5 \rightarrow nor5 \rightarrow n\text{ occurs in the graph: }5 ≤ n}\right) }\right}$

Though the formulation of the lemmata does not require the nodes/variables to be named, we shall usually name them so as to be able to refer to them in the proof. In view of (0), it suffices in each proof to demonstrate that the precondi

tion is maintained.

Lemma 0

u \rightarrow v x \rightarrow y

Proof 0 As the ord operation involves x and y only, u and v are not involved, their values remain unchanged and their order is maintained. (End of Proof 0.)

Lemma 1a

u \rightarrow y \leftarrow - x

Lemma 1b

y \leftarrow - x \rightarrow v

Lemma 1c

u \rightarrow y \leftarrow - x \rightarrow v

Proof1 Operation ord.x.y neither increases x nor decreases y ; from the constancy of u and v the conclusions now follow. (End of Proof1.)

Lemma 2

\begin{array}{l} a \longrightarrow A \ \uparrow \ b \longrightarrow B \end{array}

Proof 2 Initially, the maximum of the four values is an element of ${a,A}$ ; hence $A$ finally equals that maximum and hence $B ≤ A$ is maintained; similarly, the minimum of the four values is initially an element of ${b,B}$ , is hence finally equal to $b$ and therefore $bsa$ is maintained. (End of Proof 2.)

Note that it is essential that both ord.a.A and ord.b.B are executed. Lemma 2 is the most interesting of all. The two subgraphs $a \leftarrow b$ and $A \leftarrow B$ can be generalized to two arbitrary congruent directed graphs with drawn arrows -a

EWD932 b-2

"lower-case graph" and an "upper-case graph" -, pro- vided ord. x. X is executed for each pair (x, X) of corresponding variables

Lemma 3a

Lemma 3b

Proof3 The value of $a$ is the maximum of the triple; the value of $b$ is the minimum of the triple. The conclusions follow. (End of Proof 3.)

As special consequences we mention:

Lemma 4

See EWD937 for correction.

Lemma 5

From Lemmata 2 and 5 it follows that 4 elements can be sorted by 5 ord's, partially ordered in time:

ord.0.2 11 ord.1.3

; ord. 0.1 || ord. 2.3

; ord. 1.2

As $2^4 < 4! ≤ 2^5$ , 5 ord operations is indeed the minimum.

So much for my simple lemmata. Needless to say, my feelings about their pictorial representation are very mixed.

I am indebted to the Austin Tuesday Afternoon Club for its constructive rejection of an earlier version.

Austin, 10 September 1985

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