Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.counting-sort

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

AHoF Counting Sort: a stable, NON-comparison, O(n + k) sort for integer keys in a small range [0, k). Count how many items have each key, then take the CUMULATIVE counts (a prefix sum) to get each key's ending offset in the output, and place items from the end for stability. The cumulative counts are exactly the proved prefix-sum scan applied to the count histogram: cumulative-counts = cumulative-sum counts. Proved native and axiom-free: the cumulative counts reuse the proved prefix-sum/cumulative-sum fold (a worked histogram [2,1,3] -> offsets [2,3,6]), and its length-preservation and prefix-sum correctness are already proved in general (scan-length, scan-correctness). The histogram build and the stable placement are executable; what is proved is that the placement offsets are the prefix sum of the counts. Requires prefix-sum/cumulative-sum, algebra/nat-add, data/cons/nil (the prefix-sum module composed here plus the D63 checkpoint). Scope (measured by the kernel): this module has 1 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.counting-sort` prints this classification.

Depends onalgorithms.proofs.prefix-sum

counting-sort/cumulative-counts :
  (x₁ : List ℕ)
  → List ℕ

counting-sort/offsets-example :
  → counting-sort/cumulative-counts [2, 1, 3] = [2, 3, 6]

counting-sort/offsets-are-prefix-sum :
  (counts : List ℕ)
  → counting-sort/cumulative-counts counts = prefix-sum/cumulative-sum counts