Proofs: Block sort

Block sort returns the stable sorted order full

This proof shows: correctness, termination.

Tag each item with its input position. A sequence is stably sorted if its keys do not decrease and items with equal keys are in increasing order of their tags. For items $u, v$ write $u \sqsubset v$ when $u$ belongs before $v$ in the stable order: the key of $u$ is less than that of $v$, or the keys are equal and the tag of $u$ is smaller. This is a strict total order on the items, and "stably sorted" means increasing in $\sqsubset$.

We use these facts from other pages: the rotation by three reversals, and the rotation merge with its stability, from in-place merge sort; insertion sort is correct; LOWER-BOUND on a sorted range returns the first place whose item is not less than the key.

Termination. Every loop runs over a finite range with an index that moves one way, and the only recursion is the rotation merge, which ends. So BLOCK-SORT ends.

The outer sort. By induction on the levels, at the start of the level with width $w$ each run $A[jw \ldots (j+1)w - 1]$ is stably sorted, and the tags in one run are smaller than those in the next. For $w = 16$ this is line L1. A pair of runs that line L4 skips has its last left item not greater than its first right item, so its concatenation is already stably sorted. Any other pair is merged by BLOCK-MERGE, which by the theorem below makes it stably sorted. When $w \ge n$ there is one run. It remains to prove the theorem.

Theorem. Let $P = A[lo \ldots mid-1]$ and $Q = A[mid \ldots hi-1]$ be stably sorted, with all tags of $P$ smaller than all tags of $Q$, and $m = |P| \ge |Q| \ge 1$. Then BLOCK-MERGE leaves $A[lo \ldots hi-1]$ stably sorted and changes nothing outside it.

If $m < 64$, line L5 is the rotation merge, which is stable. Otherwise we follow the lines.

Line L7. The scan keeps the invariant: the found items form one block, in increasing order, each the first item of $P$ with its key, and the other items of $P$ seen so far keep their relative order, before the block. An item is added when its key is greater than the last found key; since $P$ is sorted, it is then the first copy of a new key. A rotation of the block forward past the gap keeps the order of the gap items. At the end, a rotation puts the block at the front. So $A[lo \ldots lo+f-1]$ holds the first copies $c_1 \sqsubset \cdots \sqsubset c_f$ of the $f$ smallest keys of $P$, and $P' = A[lo+f \ldots mid-1]$ is $P$ without them, still stably sorted.

Lemma 1 (putting the buffer back). Let $A[b \ldots b+f-1]$ hold distinct keys $c_1 < \cdots < c_f$, each the first copy of its key in $P$, and let $A[b+f \ldots hi-1]$ hold the stably sorted order $U$ of the other items of $P \cup Q$. Then the rolling loop of redistribute in line L17 leaves the stably sorted order of all of them.

Proof. For each $c_i$, the items of $P \cup Q$ with the same key all have larger tags than $c_i$: those in $P$ because $c_i$ is the first copy in $P$, and those in $Q$ because all tags of $Q$ are larger. So in the stable order $c_i$ goes right before the first item of $U$ that is not less than it, which is what LOWER-BOUND finds. The loop handles $c_1$ first. It rotates the block past the items of $U$ that are less than $c_1$, which keeps their order, and leaves $c_1$ right before the first item that is not less than it. Then $c_1$ is fixed, and the remaining block $c_2, \ldots$ continues from there; the items it passes are greater than $c_1$ and are still in stable order. The keys $c_i$ increase, so each $c_i$ lands after $c_{i-1}$, and by induction the result is the stable order. $\square$

Line L8. If $f < k$, the rotation merge stably merges $P'$ and $Q$ into $U$, and Lemma 1 finishes. From now on $f = k = 3s$ with $s = \lceil \sqrt{m} \rceil$.

Line L10. $P'$ has $m - 3s$ items. It is cut into $R$ with $r < s$ items followed by $p$ A-blocks of $s$ items, and $Q$ into $q$ B-blocks of $s$ items followed by the tail $W$ with fewer than $s$ items. There are $t = p + q \le (m + |Q|)/s \le 2m/s \le 2s$ blocks, so there are enough tags. Tag $j$ is the $j$-th smallest buffer key, and it is set beside block $j$, in the order A-blocks, then B-blocks. When $q > 0$, let $\tau$ be the tag of the first B-block; a block is an A-block if and only if its tag is less than $\tau$, and this stays true as tags move with blocks.

Lemma 2 (the block order). After line L12, list the blocks, with $W$ among them, as $Z_1, \ldots, Z_u$ from left to right, and let $h(Z)$ be the first item of $Z$. Then (a) the blocks from one run are in their original order, and (b) if $i < j$, then $h(Z_j) \not\sqsubset h(Z_i)$ when $Z_i$ and $Z_j$ come from different runs.

Proof. Line L11 is a selection sort on the key (first item, tag) compared as in the code: $Z$ before $Z'$ if $h(Z) < h(Z')$, or the keys are equal and the tag of $Z$ is smaller. The tags are distinct, so this is a strict total order, and selection sort produces it; exchanging blocks of equal length with their tags keeps each block intact. For blocks of one run, the first items increase in $\sqsubset$ with the original order, and on equal keys the tag order is the original order, so (a) holds. For blocks from different runs with equal first keys, the A-block has the smaller tag and comes first, and its first item also has the smaller input position; so the order of line L11 agrees with $\sqsubset$ on first items, which gives (b).

For $W$: every B-block comes before $W$ in $Q$, so $h(B) \sqsubset h(W)$ for each B-block $B$. Line L12 puts $W$ just before the longest suffix of blocks that are all A-blocks whose first key is greater than the key of $h(W)$. So each block $Z$ after $W$ is an A-block with $h(W) \sqsubset h(Z)$. Now let $Z$ be an A-block before $W$, and let $Y$ be the block just before $W$. If $Y$ is an A-block, its key is at most that of $h(W)$, and by (a) so is the key of $h(Z)$; since $h(Z)$ is in $P$ and $h(W)$ in $Q$, $h(Z) \sqsubset h(W)$. If $Y$ is a B-block, then $Z$ is before $Y$, and by (b) $h(Z) \sqsubset h(Y) \sqsubset h(W)$. So (b) holds with $W$ placed, and (a) holds because $W$ is after every B-block. $\square$

Lemma 3 (the local merges). Before each step of lines L14 and L15, the array range of the blocks reads: the items made final so far, in stable order; then the swap space $S$; then $F$, a stably sorted suffix of the items of one run seen so far; then $Z, Z_{\text{next}}, \ldots$ in place. Every final item is $\sqsubset$ every item of $F$ and of the blocks not yet handled.

Proof. At the start nothing is final and $F = R$. $R$ is the beginning of $P'$, so its items are $\sqsubset$ every other item of $P'$, but not necessarily of $Q$; this is all the invariant needs, since nothing is final yet.

Same run (line L14). $Z$ is the next block of $F$'s run, by Lemma 2(a), so every item $x$ of $F$ has $x \sqsubset h(Z)$ and is $\sqsubset$ every later item of its own run. A later item $y$ of the other run lies in a block $Z'$ after $Z$, and by Lemma 2(b), $h(Z') \not\sqsubset h(Z)$; the two are distinct items, so $h(Z) \sqsubset h(Z')$, and $x \sqsubset h(Z) \sqsubset h(Z') \sqsubseteq y$. So all of $F$ may become final. Moving $F$ before $S$ by exchanges keeps its order, and the new $F = Z$ is a suffix of its run seen so far.

Different runs (line L15). The loop writes, at each step, the $\sqsubset$-smaller of the heads of $F$ and $Z$; the test in the code is exactly this, as ties of keys go to the item from $P$, which has the smaller tag. Each write exchanges an item of $S$ with the chosen item. Let $g = |Z| \le s$. The writing place starts $s$ places before the head of $F$ and gains one place on it for each item taken from $Z$, so it reaches the unread items only after all of $Z$ is read. So no unread item is overwritten, and the items of $S$ are only moved. The loop stops when one side is used up; two sides cannot run out at the same step, as each step takes one item. If $F$ was empty, nothing is written. Otherwise let $e$ be the head of the rest of the other side, and $u$ the last item of the used-up side, which was the last item written. Every written item is $\sqsubset e$, and $e$ is $\sqsubset$ every later item of its run. Every written item is $\sqsubseteq u$, and $u$ is $\sqsubset$ every later item of its own run, because the blocks of a run come in order. So the written items are $\sqsubset$ everything not yet handled, and they may become final. If $F$ was used up, the code leaves $S$ as one block followed by the rest of $Z$. If $Z$ was used up, the code moves the rest of $F$ to the right end with exchanges in decreasing order of position, which keeps its order and leaves $S$ as one block before it. In both cases the new $F$ is a suffix of one run seen so far. $\square$

Lines L16 and L17. After the last block, line L16 makes $F$ final by Lemma 3 with no blocks left, so the range of the blocks is the stable order of $P' \cup Q$ followed by $S$. The rotation puts $S$ next to $T$, so the buffer of $k$ distinct items is at the front, in some order, followed by the stable order of the other items. Insertion sort puts the buffer in increasing order, which is its stable order because the keys are distinct. Lemma 1 then gives the stable order of all of $P \cup Q$. Only $A[lo \ldots hi-1]$ was touched. This proves the theorem, and with the outer induction, BLOCK-SORT leaves $A$ stably sorted. $\blacksquare$