Stable binary radix sorting: mathematical specification

The order is the unsigned order on encoded words. In particular this does not claim that sign-and-magnitude integer encodings are ordered as integers. The construction and proofs here are original; the executable native program is supplied separately.

Main definitions

• digit: one binary digit, represented as zero or one.
• select: the stable subsequence with a specified digit.
• partition: zeros followed by ones, preserving the order within each part.
• passes: least-significant-digit radix passes.

Main results

• partition_perm: a pass preserves the multiset.
• passes_correct: sufficiently many passes give a sorted permutation.

def Cslib.Algorithms.WordRAM.RadixSort.digit (b v : ℕ) : ℕ

Binary digit b of unsigned word v.

def Cslib.Algorithms.WordRAM.RadixSort.select (b t : ℕ) (xs : List ℕ) : List ℕ

The stable subsequence of words whose digit b equals t.

def Cslib.Algorithms.WordRAM.RadixSort.partition (b : ℕ) (xs : List ℕ) : List ℕ

Stable zero/one partition at digit b.

def Cslib.Algorithms.WordRAM.RadixSort.passes : ℕ → List ℕ → List ℕ

Apply the first bits binary radix passes, starting with the least significant bit.

theorem Cslib.Algorithms.WordRAM.RadixSort.digit_lt_two (b v : ℕ) : digit b v < 2

Every binary digit is below two.

theorem Cslib.Algorithms.WordRAM.RadixSort.digit_eq_shift (b v : ℕ) : digit b v = v >>> b % 2

The native shift/remainder implementation reads precisely digit.

theorem Cslib.Algorithms.WordRAM.RadixSort.length_select_le (b t : ℕ) (xs : List ℕ) : (select b t xs).length ≤ xs.length

A selection never increases the length.

theorem Cslib.Algorithms.WordRAM.RadixSort.mem_select {b t v : ℕ} {xs : List ℕ} : v ∈ select b t xs ↔ v ∈ xs ∧ digit b v = t

A selected word occurred in the original list and has the requested digit.

theorem Cslib.Algorithms.WordRAM.RadixSort.select_append (b t : ℕ) (xs ys : List ℕ) : select b t (xs ++ ys) = select b t xs ++ select b t ys

Appending an input word appends it to precisely its selected subsequence.

theorem Cslib.Algorithms.WordRAM.RadixSort.partition_perm (b : ℕ) (xs : List ℕ) : (partition b xs).Perm xs

A stable bit partition is a permutation of the input, including repeated words.

theorem Cslib.Algorithms.WordRAM.RadixSort.length_partition (b : ℕ) (xs : List ℕ) : (partition b xs).length = xs.length

Each pass keeps exactly the same number of words.

theorem Cslib.Algorithms.WordRAM.RadixSort.passes_perm (bits : ℕ) (xs : List ℕ) : (passes bits xs).Perm xs

All radix passes preserve the input multiset.

theorem Cslib.Algorithms.WordRAM.RadixSort.partition_pairwise {b : ℕ} {xs : List ℕ} (hs : List.Pairwise (fun (u v : ℕ) => u % 2 ^ b ≤ v % 2 ^ b) xs) : List.Pairwise (fun (u v : ℕ) => u % 2 ^ (b + 1) ≤ v % 2 ^ (b + 1)) (partition b xs)

A pass extends sortedness modulo 2^b to sortedness modulo 2^(b+1).

theorem Cslib.Algorithms.WordRAM.RadixSort.passes_pairwise (bits : ℕ) (xs : List ℕ) : List.Pairwise (fun (u v : ℕ) => u % 2 ^ bits ≤ v % 2 ^ bits) (passes bits xs)

The output is sorted on the low bits bits.

theorem Cslib.Algorithms.WordRAM.RadixSort.passes_correct (bits : ℕ) (xs : List ℕ) (hbound : ∀ (v : ℕ), v ∈ xs → v < 2 ^ bits) : (passes bits xs).Perm xs ∧ List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) (passes bits xs)

Keys strictly below 2^bits are sorted in unsigned order after bits passes.