Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.quicksort

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

AHoF Quicksort: an in-place, average-case O(n log n) comparison sort by divide-and-conquer -- pick a pivot, PARTITION the remaining elements into those at most the pivot and those greater, then recursively sort each side. The partition decision that routes each element is: goes-left? element pivot = decide (element <= pivot) (elements at most the pivot go to the left partition), over exact-rational keys. Proved native and axiom-free: the partition decision; that an element at most the pivot goes left; the certificate that a left-partition element really is at most the pivot (native nnrat/at-most) -- so after recursion the whole array is sorted; and that an element greater than the pivot goes right. The pivot choice, the in-place swaps, and the recursion are executable; what is proved is the partition comparison decision. 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.quicksort` prints this classification.

quicksort/goes-left? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

quicksort/small-goes-left :
  → lis/extends? 3 5 = data/true

quicksort/left-partition-below-pivot :
  → 3 ≤ 5

quicksort/large-goes-right :
  → lis/extends? 8 5 = data/false