Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.radix-sort

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/radix_sort.clj1 definitions, 3 theorems

AHoF Radix Sort (LSD): sort fixed-width integer keys in O(n * d) without comparing whole keys -- process the digits from LEAST to most significant, and on each pass STABLY sort by that digit only. Stability is what makes it correct: a later pass on a higher digit preserves the order established by earlier passes on lower digits WITHIN each group of keys sharing that higher digit (not globally: units sorting gives [21,12], and the tens pass reorders it to [12,21]). The per-digit ordering decision is: digit-precedes? digit-a digit-b = decide (digit-a <= digit-b) over exact-rational (integer) digit values. Proved native and axiom-free: the digit-order test and worked instances on concrete digits -- digit 2 precedes digit 7; the worked certificate 2 <= 7 as a native nnrat/at-most; and digit 7 does not precede digit 2. The digit extraction and the stable per-digit sort (e.g. counting sort) are executable; what is proved is the per-digit ordering decision at these instances. That each stable pass sorts by its digit, and the correctness of LSD radix sort, are classical and not proved here. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.radix-sort` prints this classification.

radix-sort/digit-precedes? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

radix-sort/smaller-digit-precedes :
  → lis/extends? 2 7 = data/true

radix-sort/preceding-digit-at-most :
  → 2 ≤ 7

radix-sort/larger-digit-follows :
  → lis/extends? 7 2 = data/false