A heuristic explanation of Batcher’s Baffler

A heuristic explanation of Batchers Baffler

[This is intended to be my final synthesis of EWD's 932b, 935a, 937, 939, and 940.]

Abstract Butcher's Baffler -so named by David Gries - is a sorting algorithm that is of interest because many of its "comparison-swaps" can be executed concurrently. It is also of interest because it used to be hard to explain.

This note explains Batcher's Baffler by designing it. Besides including all heuristics, it has two distinguishing features, both contributing to its clarity and brevity:

(0) the little) theory the algorithm relies upon is dealt with in isolation; (1) by suitable abstractions, all case analyses have been removed from the argument. (End of Abstract.)

Batcher's Baffler - so named by David Gries after K.E.Batcher, who designed it in 1968- is a sorting algorithm. Its building block considers a set of disjoint pairs of elements, swapping each pair of values that is out of order; the pairs of the set being disjoint, they will be treated as if dealt with concurrently. Since eventually all pairs have to be in order, we are interested in theorems about sets of "comparison swaps" that maintain for some other pairs the fact that they are

already in order.

We shall present the relevant lemmata graphically, in the form of directed graphs with dotted arrows and solid arrows. A dotted arrow $x \rightarrow y$ stands for the "comparison swap"

{true} x, y := x min y, x max y {x ≤ y}. A solid arrow x→y stands for the invariant relation x≤y; more precisely, the graphs representing our lemmata should be read as follows: if initially the inequalities corresponding to the solid arrows hold, they are maintained by the execution of the operations corresponding to the dotted arrows (whose inequalities eventually hold as well).

Lemma 0

Proof The maximum of the four values is initially an element of the set ${b,B}$ ,hence finally equal to $B$ ; the inequality $A \leq B$ is therefore maintained. Similarly,the minimum of the four values is initially an element of the set ${a,A}$ ,hence finally equal to a ;the inequality $a \leq b$ is therefore maintained. (End of Proof.)

Lemma 1

Proof The four solid arrows are together equivalent to a max $A \leq b \min B$ ; this relation is maintained by each of the operations corresponding to the dotted arrows. (End of Proof.)

So much for the little theory we need.

Our purpose is to sort array $\rho \left( {i : 0 \leq i < N}\right)$ . For simplicity's sake, this finite array is mentally extended in both directions to infinity,i.e. with values " -∞ " to its left and values " +∞ " to its right (the direction from left to right being the order of increasing subscript value).

with the predicate ${OK}$ being given by

$$ o k. i. j \equiv f _ {i} \leq f _ {j} $$

our purpose is to establish relation $R$ given by

$R \equiv \left( {A{a}_{i} : {Ok}.i\left( {i + 1}\right) }\right)$

by rearranging the values of $P\left( {i : 0 \leq i < N}\right)$ . Note that,thanks to our extension,Ok. i. j trivially holds for $i < 0 \vee j \geq N$ .

The algorithm manipulates array f only by means of the operation Ord. i. j with $i < j$ and given by

Ord. i. j = if ${OK}$ . i. $j \rightarrow$ skip [] $\rightarrow {OK}$ . i. $j \rightarrow$ swap. ${F}{i} \cdot j\;{F}{i}$ - the swap interchanges the values of ${f}{i}$ and ${f}{j} -$ The operation Ord. i. j establishes O.K. i. j. Note that,thanks to our extension,

$$ i < 0 \vee j \geqslant N \Rightarrow \mathrm {O r d .} i. j = s k i p $$

independently of the value of $f\left( {i : 0 \leq i < N}\right)$ .

In view of $R$ we choose as invariant $P_0$ given by $P_0 = \begin{array}{l} (\underline{\mathsf{A}}_i:: \mathsf{OK}.i.(i + t)) \ \end{array}$ , which is easily established since $t \geq N \Rightarrow P_0$ . This choice suggests for Batcher's Baffler the form

"establish $t\geq N$ ${P_0}$ 1 do t+1 → "decrease t under invariance of P

od R3

The guiding principle of our development is that, once an OK relation has been established, it will be maintained, i.e. if "decrease t under invariance of Po" involves the transition from $t = t^{\prime}$ to $t = t^{\prime \prime}$ , we require

$$ (\underline {{A}} i: O K. i. (i + t ^ {\prime \prime})) \Rightarrow (\underline {{A}} i: O K. i. (i + t ^ {\prime})) $$

an implication whose validity requires (in view of Ok's transitivity) to be a multiple of t". Under that constraint, the most modest decrease of t - i.e. the one that strengthens Po as little as possible- is halving it , and we therefore pro-. pose to restrict t to powers of 2 . (At this stage this proposal is tentative; its wisdom will

transpire shortly.)

Explicit incorporation of the manipulations on t yields for Butcher's Baffler

$$ \begin{array}{l} t := 1; \underline {{\operatorname {d o}}} t < N \rightarrow t := 2. + \underline {{\operatorname {o d}}} {P _ {0} \wedge t \mathrm {i s a p o w e r o f} 2 } \ ; d o + \neq 1 \rightarrow t := + / 2 \ ; {\mathcal {P}: (\underline {{A}} i: = O K. i. (i + 2 +)) } \ " r e s t o r e P o " \ {P _ {0}: (\underline {{A}} i: O K, i. (i + t)) } \ \end{array} $$

[\text{odd}\left{ {R\rbrack : A : E}\right} ]

The rest of this note is concerned with the development of the subalgorithm for "restore Po" as specified above by its pre- and postconditions. (For this subalgorithm it is no longer relevant that $t$ is a power of 2.)

The design of Batcher's Baffler is driven by the desire to find groups of Ord operations with disjoint argument pairs, because such Ord operations could be executed concurrently. As each Ord operation establishes the corresponding OK relation, we are invited to select from the postcondition Po a group of OK relations with disjoint argument pairs. Such a group occurs in

$$ P _ {2} \equiv (\mathrm {A i}: e. i: O K. i. (i + t)) $$

if we can find a predicate $e$ such that

(0) $e.i \equiv \neg e.\left( {i + t}\right)$

There are many such predicates, all variations on the same theme; the simplest one is

$$ (1) \quad e. i \equiv (i \mod 2 \cdot t) < t $$

Remark It is the factor of 2 in the above for- mula that will justify our earlier choice to re- strict t to powers of 2 . (End of Remark.)

In order to capture the remaining OK relations of ${P}{0}$ we write ${P}{0}$ as ${P}{2} \land {P}{3}$ ,thus finding

Note that (0) is maintained when e is replaced by 7e ; in other words: also the OK relations occurring in ${P}_{3}$ have disjoint argument pairs.

Using II to denote the potentially concurrent com- bination of statements, we have indeed

${S}{2} : \;\left{ {\text{true}} \left( {\parallel i : e.i : {\operatorname{Ord}}{i}\left( {i + t}\right) }\right) \left{ {P}_{2}\right} }\right.$ and

[\left{ {\text{true}}\right} \left( {\begin{Vmatrix}i : {ze}.i : {\operatorname{Ord}}{i}\left( {i + t}\right) }\right) \left{ {P}{3}\right} ]

But we cannot achieve P2 P3 -i.e. Po- by performing S2 and S3 consecutively (in some order), for in general the second one will destroy what the first one has accomplished. So we have to proceed more carefully, e.g. First establishing $\mathbb{P}_2$ -the choice is irrelevant, as we were free to call either polarity of the partitioning predicate e - and then establishing $\mathbb{P}_3$ with a repetition for which $\mathbb{P}_2$ is an invariant, i.e. we may expect that repetition to establish $\mathbb{P}_2 \wedge \mathbb{P}_3$ under invariance of $\mathbb{P}_2 \wedge \mathbb{P}_4$ , where $\mathbb{P}_4$

is a suitable generalization of $P_{3}$ .

In order to be a suitable generalization of $P_3$ , $P_4$ too should be composed of OK-relations with disjoint argument pairs. In view of (o) this can be achieved by replacing $t$ in OK.i.(i + t) by an odd multiple of $f$ . Since the general even value has a slightly simpler form than the general odd value, we propose to rewrite $P_3$ -see(o)- as

${P}_{3} \equiv \;\left( {\underline{A}i : e.i : {OK}.}\right) .\left( {i + 2,t}\right) )$

and propose for $P$

${P}_{4} = \;\left( {\underline{A}i : e.i : {OK}.}\right) .\left( {i + v \cdot t}\right) )$

the latter to ensure that all argument pairs in $\mathcal{P}4$ are disjoint. It now stands to reason to consider

[\left{ {\text{true}}\right} \left( {\parallel i : e.i : {Ord}.}\right) .\left( {i + v \cdot t}\right) )\left{ {P}_{4}\right} ]

and to investigate under which conditions 54 maintains $P_{2}$ . Because v is even, it suffices to investigate the fate of OK. (i.v.t). (i.v.t + t) with i satisfying e.i. With its incident ord operations it yields the picture

which is certainly not a lemma, but we can recognize the sequence $\longrightarrow$ in Lemma1, redrawn for the purpose:

of the three solid arrows added, the two horizontal ones -v being even! - are implied by $P_{1}$ . The third one is implied by $P_{42v}$ . In other words, for statement S4 we have established the theorem

$$ {P _ {1} \wedge P _ {2} \wedge P _ {2, v} ^ {v} } S 4 {P _ {2} \wedge P _ {4} } $$

Taking the invariance of $P_{1}$ for the time being for granted, this theorem tells us, as

$$ P _ {4} \land v = 2 \Rightarrow P _ {3} $$

that we can establish P3 under invariance of $P_{2}$ by first establishing $\mathsf{P4}$ with v equal to a sufficiently high power of 2 , and then repeatedly halving v while maintaining $\mathsf{P2}\wedge \mathsf{P4}$ by executing $54$

Independently of $e$ , ${P}{4}$ holds if(v-1). $t \geq N$ ; with $e$ as given in (1),however,the weaker $v + 2\mathrm{\;N}$ suffices. With that choice for $e$ (and still under the assumption of the invariance of ${P}{1}$ ) we get the following program for Balther's Baffler.

$$ \begin{array}{l} 1 [ t, v 0: i n t; t, v 0 := 1, 1 \ ; \underline {{d o}} + < N \rightarrow + := 2 + \underline {{o d}} {P _ {0} \wedge v _ {0} + > N } \ ; \underline {{d o}} + \neq 1 \rightarrow t, v 0 := t / 2, 2 \cdot v 0 {P _ {1} \wedge v 0. + \geq N } \ ; (1 1 i: e. i: O r d. i. (i + t)) {P _ {1} \wedge P _ {2} \wedge v o. t \geq N } \ ; \llbracket v: i n t; v := v 0 {P _ {1} \wedge P _ {2} \wedge P _ {4} } \ ; \underline {{d o}} v \neq 2 \rightarrow v := v / 2 {P _ {1} \wedge P _ {2} \wedge P _ {4} ^ {v} _ {2, v} } \ j (| i: e. i: O r d. (i + t). (i + v \cdot t)) \ {P _ {1} \wedge P _ {2} \wedge P _ {4} } \ \operatorname {o d} \left{P _ {2} \wedge P _ {3} \right} \ ] \left{\left. P O \wedge v O + \geq N \right} \right. \ \operatorname {o d} {P _ {0} \wedge t = 1 } \ \mathbb {1} {R } \ \end{array} $$

We are left with the obligation to verify that ${P}_{1}$ , i.e.

$$ (\mathrm {A i}: O K. i. (i + 2 +)) $$

is maintained by S2 and S4 . The latter two are both of the form

$$ (1 1 i: p. i: O r d. i. (i + m. t)) $$

with $p.i \equiv e.i\;$ or $p.i \equiv 7$ e.i and with odd $m$ . In

$$ \begin{array}{l} {i \longrightarrow i + 2 \cdot t,} \ {\quad i + m \cdot t \longrightarrow i + (m + 2) \cdot t} \end{array} $$

however, we recognize Lemma 0 . With either choice

for $p$ ,each OK relation of ${P}_{1}$ occurs,because

And this completes our derivation of Batcher's

History and acknowledgements

We are first and foremost indebted to K.E. Balcher, who invented this algorithm in 1968. I saw it for the first time explained and proved to be correct in a manuscript by David Gries. His explanation is in two steps, dealing with "sort two-ordered" first, and then reducing the complete sorting task to repeated applications of the former; in the above I have followed his way of breaking down the invariant.

In the fall semester of 1985, my target was the derivation of programs rather than just their explanation. The leitmotiv of that course was that, in the design of a program, it often pays to develop the underlying theory first. It had been chosen because of my experience that such a theory could provide a strong heuristic guidance. Because I did not know it too well and it looked sufficiently ambitious, Batcher's Baffler was one of the examples selected as proving ground for this approach. As we did not know what would be needed, our initial theory encompassed more than the two lemmata given here.

The ATAC (= Austin Tuesday Afternoon Club) Focussed its attention on the theory and the graphical notation of its lemmata; this led to a com- plection of the theory and an improvement of its presentation.

The EtAC (= Eindhoven Tuesday Afternoon Club) focussed its attention on the argument that led to my design and suggested several improvements. There, C.S. Scholten suggested the extension of the finite array to an infinite one; this suggestion deserves to be mentioned explicitly since it did away with the last case analyses in the argument.

Finally, an oversight - in the initialization of $P_4$ was pointed out to me in late December '85, when I had the privilege of presenting Bacher's Baffler to the Eindhoven Informatics Colloquium.

All these contributions are gratefully acknowledged.

Austin, 19 February 1986

prop. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 United States of America.