A symmetry in the sorting task

A symmetry in the sorting task

That an integer sequence $f_{i}$ (osi) is ascending is usually stated as

$$ (\exists i, j: i < j: f _ {i} \leq f _ {j}) $$

We can reformulate this in terms of $<$ only as

$$ (\exists i, j: i < j: \neg (f _ {j} < f _ {i})) $$

or -trading and the Morgan- more symmetrically

$$ (\underline {{A}} i, j: \rightarrow (i < j \land f _ {j} < f _ {i})) $$

Calling the inner conjunction the characterization of a "conflict", we see that "being sorted" can be described as "having no conflicts".

Some remarks are in order.

The ordering between i, j could differ from the ordering between the f-values, which could be reals, words. fIgures or what have you. Well, we knew this. We went for an ascending sequence rather than an increasing one because we wished to allow $f_{i} = f_{j}$ for $i \neq j$ . But equality is a very strong notion, closely associated with the rule of Leibniz, and we can get the same freedom by introducing among the $f$ -values a partial order:

what used to be equality can then be weakened to "ordered in neither direction": for two values a and b, $\eta (a < b \lor b < a)$ then expresses that we don't care about their relative order in which they occur in a sorted sequence.

We shall use -as we just did- $<$ to denote a nonreflexive partial order, i.e. we have the reflexivity

(0)

and the transitivity

$x < y \land y < z \Rightarrow x < z$

Because it is always a good idea to draw trivial conclusions immediately, we deduce

$\Rightarrow x < y \land y < x)$

• The last remark is that the $i, j$ need not be taken from the integers but may be taken from some partially ordered set. A sequence being sorted can then be generalized to a one-to-one correspondence being free of conflicts. For the definition of a conflict:

let $i,j$ belong to the one set, and

let $a, b$ belong to the other set, and

let (i,a) and (j,b) be a pair of elements

of a one-to-one correspondence; then, this

pair presenting a conflict means

$$ (i < j \land b < a) \lor (j < i \land a < b) $$

We may expect that it is possible to remove a conflict by "twisting", i.e. by replacing a conflicting pair $(i,a)$ and $(j,b)$ by the pair $(i,b)$ and $(j,a)$ . Furthermore - thanks to the transitivity of $<$ we may expect that a local removal of a conflict by a twist reduces the total number of conflicts. The big question is: how do we prove all this without destroying the symmetry between the two sets, without case analyses, and without all sorts of duplication in the argument?

For the sake of brevity

we denote sequences of elements from the original sets by juxtaposition • < between two sequences of equal length denotes the sequence of truth values obtained by element-wise application of < the conjunction of a sequence of truthvalues is denoted by surrounding the sequence by a pair of square brackets.

e.g. $\left\lbrack {{ib} < {ja}}\right\rbrack \equiv i < j \land b < a$

The important properties are illustrated by

$$ [ i b < j a ] \equiv [ b i < a j ] $$

$$ [ x < y ] \equiv x < y $$

$$ [ x x < y y ] \equiv [ x < y ] $$

$$ [ i b < j a ] \wedge [ k < c ] \equiv [ i b k < j a c ]. $$

As a consequence of (0) we mention

$\neg \left\lbrack {{xy} < x + 2}\right\rbrack \; \land \;7\left\lbrack {y \times 2 \times 2}\right\rbrack .$ and as a consequence of (0) and (1) (5) $\neg \left\lbrack {{abc} < {bca}}\right\rbrack \land \neg \left\lbrack {{abc} < {cab}}\right\rbrack$

Denoting the presence of a conflict between the elements $\left( {i,a}\right)$ and(j,b)of a one-to-one correspondence by $\left( {i,a}\right) \operatorname{con}\left( {j,b}\right)$ ,we can now define in our new notation con by

(i,a) $\operatorname{con}\left( {j,b}\right) \equiv \left\lbrack {{ib} < {ja}}\right\rbrack \vee \left\lbrack {{ja} < {ib}}\right\rbrack$

Its evident properties are

$$ \begin{array}{l} (i, a) \underline {{\underline {{\operatorname {c o n}}}}} (j, b) \equiv (j, b) \underline {{\underline {{\operatorname {c o n}}}}} (i, a) \ (i, a) \underline {{\underline {{\operatorname {c o n}}}}} (j, b) \equiv (a, i) \underline {{\underline {{\operatorname {c o n}}}}} (b, j) \ \lnot (j, a) \underline {{c o n}} (i, a) \land \lnot (j, a) \underline {{c o n}} (j, b) \ \end{array} $$

In order to show that removal of a conflict by "twisting" works and reduces the total number of conflicts, we prove two theorems.

Theorem 0

$$ \begin{array}{l} (i, a) \underline {{\operatorname {c o n}}} (j, b) \wedge (k, c) \underline {{\operatorname {c o n}}} (i, b) \wedge (k c) \underline {{\operatorname {c o n}}} (j, a) \ \Rightarrow (k, c) \underline {{c o n}} (i, a) \wedge (k, c) \underline {{c o n}} (j, b) \ \end{array} $$

Proof We first establish (i)

$$ (k, c) \underline {{\mathrm {c o n}}} (i, a) \wedge (k, c) \underline {{\mathrm {c o n}}} (j, b) $$

$$ = {(6), d e f. o f c o n } $$

$$ ([ k a < i c ] \vee [ i c < k a ]) \wedge ([ k b < j c ] \vee [ j c < k b ]) $$

$$ = {\wedge d i s t r i b u t e s o v e r v } $$

$$ [ k a k b < i c j c ] \vee [ k a j c < i c k b ] \vee $$

$$ [ i c k b < k a j c ] \vee [ i c j c < k a k b ] $$

Next we establish (ii)

$$ \begin{array}{l} [ i b < j a ] \land (k, c) \underline {{c o n}} (i, b) \land (k, c) \underline {{c o n}} (j, a) \ = {(1) \quad \mathrm {w i t h} a, b := b, a } \ [ i b < j a ] \land \ ([ k b k a < i c j c ] \vee [ k b j c < i c k a ] \vee \ [ i c k a < k b j c ] \vee [ i c j c < k b k a ]) \ \Rightarrow {\wedge d i s t r i b u t e s o v e r v ; a b s o r p t i o n } \ [ k b k a < i c j c ] \vee [ i c j c < k b k a ] \vee \ [ i b k b j c < j a i c k a ] \vee [ i b i c k a < j a k b j c ] \ = {(5) } \ [ k b k a < i c j c ] \vee [ i c j c < k b k a ] \ = {\mathrm {s y m m e t r y} o f \wedge } \ [ k a k b < i c j c ] \vee [ i c j c < k a k b ] \ \Rightarrow \quad {(i) } \ (k, c) \underline {{c o n}} (i, a) \wedge (k, c) \underline {{c o n}} (j, b) \ \end{array} $$

From (ii) with $i, b, j, a := j, a, i, b$ and the symmetry of $\wedge$ we derive the same implication, except that the first conjunct of the antecedent is replaced by $[ja < ib]$ . Disjunctive combination of (ii) and the latter implication yields Theorem (0).

(End of Proof.)

Theorem 1

(i,a)con(j,b)A (k,c)con(i,b)

$\left( {k,c}\right) \underline{\operatorname{con}}\left( {i,a}\right) \vee \left( {k,c}\right) \underline{\operatorname{con}}\left( {j,b}\right)$

Proof

(i,a)con(j,b)A (k,c)con(i,b) $= { {def. of}\;{con}.i.e.\left( 6\right) }$ $\left( {\left\lbrack {ib < {ja}}\right\rbrack \vee \left\lbrack {{ja} < {ib}}\right\rbrack }\right) \land \left( {\left\lbrack {kb < {ic}}\right\rbrack \vee \left\lbrack {{ic} < {kb}}\right\rbrack }\right)$ $= {$ distribution of $\Lambda$ over $v}$

$\left\lbrack {{ibkb} < {jaic}}\right\rbrack \vee \left\lbrack {{ibic} < {jakb}}\right\rbrack v$

$\left\lbrack {{jakb} < {ibic}}\right\rbrack \vee \left\lbrack {{jaic} < {ibkb}}\right\rbrack$

$\Rightarrow$ {transitivity and ahsorption}

$\left\lbrack {{kb} < {jc}}\right\rbrack v\left\lbrack {{ic} < {ka}}\right\rbrack v$

[\left\lbrack {ka < {ic}}\right\rbrack \;v\;\left\lbrack {{jc} < {kb}}\right\rbrack ]

${ 6} ,i.e.\;{def}.\;{op}\;{con} =$

$(k,c)$ con(i,a) V (k,c)con(i,b)

(End of Proof.)

Corollary

$$ (i, a) \underline {{\underline {{\operatorname {c o n}}}}} (j, b) \Rightarrow \neg (j, a) \underline {{\underline {{\operatorname {c o n}}}}} (i, b) $$

Proof Theorem 1 with $k,c \mathrel{\text{:=}} j,a\;\left( {\text{End of Proof.}}\right)$

Consider now a one-to-one correspondence containing the pair $X$ given by $X = {(i, a), (j, b)}$ and let $X$ contain a conflict, i.e. let $(i, a) \cong (j, b)$ . Let us derive a new one-to-one correspondence by twisting the elements of $X$ , i.e. by replacing $X$ by $Y$ , given by $Y = {(i, b), (j, a)}$ .

From the Corollary we conclude that $Y$ contains no conflict, i.e. that the twist successfully removed the conflict in $X$ .

The other elements, which occur in both one- to-one correspondences, have at most two conflicts with $X$ and at most two with $Y$ . According to Theorem 0, an element having both conflicts with $Y$ has both conflicts with $X$ . According to Theorem 1, an element having a conflict with $Y$ has a conflict with $X$ .

We conclude that replacing $X$ by $Y$ has reduced the total number by at least one.

To claim that I have been successful at removing all duplication, would be an exaggeration. In retrospect I could have tried the introduction of a symmetric operator, § say, between sequences of equal length. Giving § a higher binding power than the logical operators we could have written

(7) $\left( {i,a}\right) \underline{\operatorname{con}}\left( {j,b}\right) \equiv {ib}\xi {ja}$

We would then have developed a $\xi$ -calculus. The symmetry and associativity of $\wedge$ would be expressed by

(8) $X\left\lbrack Y\right\rbrack \equiv p \cdot X\left\lbrack {p \cdot Y}\right\rbrack$ for any permutation $p$ .

The most complicated rule would be

(g) $X \in Y \land R \subseteq S \equiv {XR} \subseteq Y\sum \vee {XS} \subseteq Y\overline{R}$

The analogue of (5) would have been - with lower case letters for single elements -

(10) $\tau \left( {{xYZ}\;8{Y}_{X}Z}\right)$

I might have saved a factor of 2 , and I think it would have been an improvement. Let us investigate how we would then have proved Theorem 0 at a single go.

antecedent of Theorem 0

$$ = {(-) } $$

${ib}\xi {ja} \land {kb}\xi {ic} \land {ka}\xi {jc}$

$$ \begin{array}{l} = {(9) } \ i b \xi j a \wedge (k b k a \xi i c j c \vee k b j c \xi i c k a) \ \Rightarrow {\wedge d i s t r i b u t e s o v e r v; a b s o r p t i o n } \ k b k a \S i c j c v (i b \S j a \wedge k b j c \S i c k a) \ = {(a) } \ k b k a \S i c j c v (i b k b j c \S j a i c k a v i b i c k a \S j a k b j c) \ = {(1 0) } \ k b k a \S 1 c j c \ = {(8) } \ k a k b \xi i c j c \ \Rightarrow {\mathrm {a b s o r p t i o n} } \ k a k b \xi i c j c v k a j c \xi i c k b \ = {(a) } \ k a \xi i c \wedge k b \xi j c \ = {(7) } \ \mathrm {c o n s e q u e n t o f T h e o r e m O} \ \end{array} $$

The experiment shows a considerable improvement; I still hesitate about its moral. Note that the first two "evident properties" of con are shared by $\S !$ In view of the above proof, the obvious advantage of $\S$ is that it can be applied to sequences of any length.

Austin, 12 Feb. 1988

prof. dr. Edsger W. Dgkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712- 1188, USA