Proofs: Polyphase merge sort
These are the human proofs of Polyphase merge sort, at full length.
Polyphase merge sort sorts in l phases full
This proof shows: correctness.
We use the line numbers of the pseudocode. Let . A distribution is a vector of run counts for the input tapes. Define the perfect distributions by and
Write for the sum of the entries of .
Lemma 1 (shape). For each , is non-increasing, and for all its entries are at least 1. The totals grow strictly: .
Proof. is non-increasing. If , then , so is non-increasing, and each entry is at least . Also , because and .
So line L2 finds a level , and . Line L4 gives each tape at most real runs, because it picks the tape with the largest deficit, and the total deficit before the last real run is at least 1. Line L5 fills each tape to exactly runs. A dummy run is an empty run.
Lemma 2 (one phase). Suppose that before line L8 the output tape is empty and the input tapes hold the counts of , , in some order. Then after line L11 the new output tape is empty and the input tapes hold the counts of , in some order.
Proof. Let , so the input tapes hold . The smallest of these is , by Lemma 1. Lines L9 and L10 take runs from each input tape and write runs to the output tape. The input tapes now hold , and the old output tape holds . The tape that held runs is empty. If , all , so it is the only empty tape, and line L11 picks it. If , then , all input tapes are empty, line L11 picks one of them, and the counts are on the old output tape and 0 elsewhere. In both cases the counts are those of .
Lemma 3 (contents). At each test of line L7, each run on a tape is sorted, and the multiset union of all runs on the tapes is the multiset of the items of .
Proof. Line L1 makes sorted runs whose union is , and dummy runs are empty. Line L10 removes one run from each input tape and appends their merge. The merge of sorted runs is sorted, and it holds exactly the items of the runs it merged.
Theorem. If , the loop of line L7 runs exactly times, and line L12 returns the items of in non-decreasing order.
Proof. Before the first phase, the input tapes hold and the output tape is empty. By Lemma 2 and induction, after phases the tapes hold the counts of , with total . By Lemma 1, for , and . So the test of line L7 fails for the first time after phases, when exactly one run is left. By Lemma 3, this run is sorted and holds all items of .
The sort is not stable. Take , three equal keys, with and . The distribution is : tape 1 holds and tape 2 holds . Phase 1 merges and onto tape 3. Phase 2 merges from tape 1 with from tape 3, and the merge takes tape 1 first on equal keys, so the output is .