Heapsort (with A.J.M. van Gasteren and W.H.J.Feijen)

A v G 8 / E W D 7 9 4 / W F 3 9 - 0

Heapsort.

Heapsort is an efficient algorithm for sorting in situ. For brevity's sake we shall sort integers. We take for Heapsort the following functional specification:

11 N: int {N≥1} m(i:0≤i<N): array of int {BM: bag of int such that PO: BM= (B i:0≤i<N: m(i))} Heapsorf {m such that R: PO ∧ (A i, j: 0≤i<j ∧ 1≤j<N: m(i) ≤m(j))}

The above states no more than that Heapsort is a

We shall approach Heapsort by numbered versions, starting with Heapsort0.

Heapsort $\mathcal{O}$ : II q: int $j = N$ $\left{ {\text{invariant }{\mathcal{P}}{1}}\right.$ $1 ≤ q ≤ N ∧ {P}{0} ∧ \left( {\underline{A}i,j;0 ≤ i < j A}\right) ≤ j < N : m\left( i\right) ≤ m\left( j\right) )}$ $; * \left\lbrack {q ≠ 1}\right.$ $\rightarrow \operatorname{So}{ m,q$ such that ${\mathcal{P}}{1};\frac{\operatorname{dec}}{2}q}$ $] * \left{ {{P}{1} ∧ q = 1,\text{ hence }}\right}$

A v G 8 / E W D 7 g 4 / W F 3 g - 1

The above states that the sorted sequence is built up "from right to left", i.e. in the order of decreasing subscript.

Our first version of So is

So:

11p:int

; 51

\begin{array}{l} {m (i: 0 ≤ i < q), p \mathrm {s u c h t h a t} \ R _ {1}: 0 ≤ p < q ^ {\prime} ∧ P _ {1} ∧ (\underline {{A}} i: 0 ≤ i < q: m (p) ≥ m (i)) } \ ; q := q - 1; m: s w a p (p, q) \ \end{array}

1

An unsophisticated S1 would leave m unchanged and would only locate a maximum value $m(p)$ among the leftmost q elements of m; the N2-algorithm that would result is known as Bubble Sort. In view of our later transition to Heapsort1 we allow S1 to rear-range m(i:osicg) as well in order to establish a relation H about m(i:psicg), to be used as follows in our final version of So.

So:

[p:int]

; S _ {1} {m (i: 0 ≤ i < q), p \mathrm {s u c h t h a t} H \cap R _ {1} }

; q := q - 1; m: s w a p (p, q) {H (p := p + 1) }

i p := p + 1 {H }

1

A v G 8 / E W D 7 g 4 / W F 3 g - 2

In order to justify the last two assertions in the above we require $H$ ,besides being an assertion about $m\left( {i : p ≤ i < q}\right)$ ,to satisfy

H ⇒ H (p, q := p + 1, q - 1) (0)

In order that $H$ -which is about $m\left( {i : p ≤ i < q}\right)$ - assist in establishing the last factor of ${R}_{1}$ -which is about $m\left( {i : 0 ≤ i < q}\right)$ - we require $H$ to satisfy

(H ∧ p = 0) ⇒ (\underline {{H}}: p ≤ i < q: m (p) ≥ m (i)) (1)

and ${S}_{1}$ to terminate with $p = 0$ . Hence we suggest

\begin{array}{l} S _ {1}: \ \begin{array}{r l}&{p := h (q)}\&{{\mathrm {i n v a r i a n t} P _ {2}: 0 \le p ∧ P _ {1} ∧ H }}\&{; * [ p \ne 0 \rightarrow p := p - 1}\&{{H (p := p + 1) }}\&{; S _ {2}}\&{{m (i: p \le i < q) \mathrm {s u c h t h a t} H }}\&{\vdots}\end{array} \ \end{array}

where $h$ is such that

(p = h (q)) ⇒ (H ∧ 0 \le p) . \tag {2}

A v G 8 / E W D 7 9 4 / W F 3 9 - 3

Substituting S1 in our final version of So and substituting the result in Heapsorto, we get a program in which relation H - together with p - can be taken outside the repetition of Heapsorto . The transformation is very likely to improve the efficiency since we can conclude from S1 that So restores H with $p = 1$ ,a value very likely to be much smaller than h(q) . The result of the transformation is Heapsort1 .

Heapsort1: $\begin{array}{l}\left[p,q:\mathrm{int}\right.\ \vdots q:= N\left{\mathsf{P}_1\right} \ \vdots p:= h(q)\left{\mathrm{invariant}\mathsf{P}_2\right} \ \vdots \left[q≠ 1\right.\ \rightarrow \left{\mathrm{invariant}\mathsf{P}_2\right} \ \left[p≠ 0\right.\ \rightarrow p:= p - 1\ \left{\mathsf{H}(p:= p + 1)\right} \ ;S_2\ \left{m(i:p < i < q)\mathrm{~such~that~}H\right} \ \rbrack \ ;q:= q - 1;m:\operatorname {swap}(p,q);p:= p + 1\ ]\end{array}$

Our remaining task is the choice of an appropriate $H$ and the design of the corresponding $S_{2}$ and $h$ .

A v G 8 / E W D 7 g 4 / W F 3 g - 4

A possibility for $H$ would be

(\underline {{A}} i, j: p ≤ i < j < q: m (i) ≥ m (j))

but - besides begging the question - it is stronger than necessary since the right-hand side of (1) would be implied by $H$ all by itself. Hence the above suggestion is weakened by requiring $m\left( i\right) ≥ m\left( j\right)$ for a subset of(i,j)-pairs with isj :

H. $\left( {\underline{A}{\mathrm{i}}{j} : p ≤ i < j < q ∧ c\left( {i}{j}\right) : m\left( i\right) ≥ m\left( j\right) }\right)$

Requirement (0) is satisfied; (2) is satisfied by $h(q) = q$ . Viewing the natural numbers $(<q)$ as the vertices of a directed graph and the truth of $c(i,j)$ as the presence of a directed edge from vertex $i$ to vertex $j$ , (1) is equivalent to the requirement that all vertices are reachable from vertex 0, in formula

(\underline {{A}} j: j > 0: (\underline {{E}} i: 0 ≤ i < j: c (i, j))) . \tag {3}

For the purpose of describing $S_{2}$ , we reformulate

c c (i, j) = c (i, j) \vee (\underline {{E}} k: i < k < j: c (i, k) \wedge c c (k, j))

as

H: $\left( {\underline{A}{i}_{,j} : p ≤ i < j < q∧ c\in \left( {i,j}\right) : m\left( i\right) ≥ m\left( j\right) }\right)$

A v G 8 / E w D 7 g 4 / W F 3 g - 5

${S}_{2}$ can then establish $H$ using ${SH},$ given by

SH: $\underset{\sim }{A}{i,j} : p ≤ i < j < q∧ c \subset \left( {i,j}\right) : m\left( i\right) ≥ m\left( j\right) \vee i = w} ,$

which has the useful property

$\left( {S - H}\right) = \left( {\underline{A}j : w < j < q∧ c\left( {w,j}\right) : m\left( w\right) ≥ m\left( j\right) }\right) ⇒ H.$

A still somewhat abstract form of $S_{2}$ is

S2:

111 w : int

\begin{array}{l} {H (p := p + 1) } \ ; w := p {i n v a r i a n t S H } \ ; * [ (\underline {{E}} _ {j}: w < j < q ∧ c (w, j)) \ \rightarrow | [ v: i n t ] \ ; S 3 {v s u c h t h a t: \ w < v < q ∧ c (w, v) a n d m (v) m a x i m a l \ j - [ m (w) ≥ m (v) ] \rightarrow {H } w := q {S H } \ [ m (w) < m (v) \rightarrow m: s w a p (v, w); w := v {S H, s e e N o t e } \ ] ] \ ] * \ j i \ \end{array}

Note. See page 7.

Our next task is to propose a suitable c. Require- ment (3) states that for $j > 0$ the equation in $i$

A v g 8 / E w D 7 g 4 / W F 3 g - 6

o s i < j ∧ c (i, j)

has at least 1 solution; since nothing is gained by giving it more solutions C will be chosen such that it has exactly 1 solution. In other words, the directed graph we referred to takes the form of a rooted tree. The structure of S2 shows that for given w the solutions j ofo $c(w,j)$ have to be generated; for reasons of convenience these solutions will be consecutive integers. We propose for some integer d

c (i, j) = (i = (j - 1) \underline {{d i v}} d)

Remark. With $d = 2$ we obtain the traditional Heapsort. Since $d = 3$ gives a better worst-case behaviour, we present the code for general $d$ . (End of Remark.)

In our following version of $S_{2}$ , $h$ and $k$ are used to delimit the solutions $j$ of $w < j < q ∧ c(w, j)$ ; they are those of $h ≤ j < k$ . In the code replacing $S_{3}$ , $h$ is used for scanning. Further optimizations - e.g. reducing the number of subscriptions - are left to the reader.

A v g 8 / E W D 7 g 4 / W F 3 g - 7

S2:

\begin{array}{l} 1 [ w, h, k: i n t \ ; w := p; h := d \cdot w + 1; k := \min (h + d, q) \ ; * [ h < k \ \rightarrow | [ v: i n t ] \ ; v, h := h, h + 1 \ i * [ h < k \ \rightarrow - [ m (v) ≥ m (h) \rightarrow h := h + 1 \ [ ] m (v) ≤ m (h) \rightarrow v, h := h, h + 1 \ ] - \ \end{array}

\begin{array}{l} ] * \ ; - [ m (w) ≥ m (v) \rightarrow s k i p {h = k } \ [ [ m (w) < m (v) \rightarrow m: s w a p (v, w); w := v \ ; h := d \cdot w + 1; k := m i n (h + d, q) \ ] - \ \rbrack \rbrack \ \begin{array}{c} \text {]} * \ \text {]} \end{array} \ \end{array}

Note (To be inserted on page 5.) Relation SH states that $m\left( w\right)$ is the only element that may have descen-dants exceeding itself. If so, being the only one, $m\left( w\right)$ has a son exceeding itself. Because $m\left( v\right)$ is a maxi- mum son of $m\left( w\right)$ ,after the swap $m\left( v\right)$ is the only element that may have descendants exceeding itself. Note that for this conclusion it was not essential that sons have a unique father. (End of Note.)

References

Williams, J.W.J., Algorithm 232 HEAPSORT,

C.A.C.M. 7,6 (Jun 1964) 347-348

Floyd, Robert W., Algorithm 242 TReESORT 3.

C.A.C.H 7,12 (Dec 1964) 701

drs. A.J.M.van Gasteren

BP Venture Research Fellow

W.H.J.FeJen

Department of Mathematics

and Computing Science

University of Technology

5600 MB EINDHOVEN

The Netherlands

22 June 1981

pror. dr. Edsger W. Dgiksha

Burroughs Research Fellow

Plataanstraat 5

5671 AL NUENEN

The Netherlands