Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bucket-sort

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

AHoF Bucket Sort: sort values drawn from a uniform range in EXPECTED linear time by distributing them into ordered buckets by value, sorting each bucket (with any comparison sort), and CONCATENATING the buckets in order. It beats comparison sorts' n log n bound in expectation when the input is uniform (few items per bucket). Correctness rests on emitting buckets in increasing index so every value of a lower bucket precedes every value of a higher one: bucket-precedes? bucket-a bucket-b = decide (bucket-a <= bucket-b) over exact-rational (integer) bucket indices. Defined: the bucket-order test. Proved native and axiom-free, as worked instances: bucket 1 precedes bucket 4, bucket 4 does not precede bucket 1, and the worked certificate 1 <= 4 (native nnrat/at-most). That the concatenation is globally sorted, and the expected linear running time, are classical and not proved here. The value-to-bucket distribution and per-bucket sort are executable. 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.bucket-sort` prints this classification.

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

bucket-sort/lower-bucket-first :
  → bin-packing/fits? 1 4 = data/true

bucket-sort/preceding-bucket-index-at-most :
  → 1 ≤ 4

bucket-sort/higher-bucket-later :
  → bin-packing/fits? 4 1 = data/false