Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.quickselect

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

AHoF Quickselect (Hoare's selection): find the k-th smallest element of an unsorted array in expected O(n) -- faster than sorting -- by partitioning around a pivot (as in quicksort) but recursing into ONLY the side that contains the target rank. After partitioning, the target lies in the left partition exactly when its rank is at most the pivot's final rank: recurse-left? target-rank pivot-rank = decide (target-rank <= pivot-rank) over exact-rational (integer) ranks. Proved native and axiom-free: the recursion-side decision and worked instances on concrete ranks -- target rank 2 against pivot rank 4 recurses left; the worked certificate 2 <= 4 as a native nnrat/at-most; and target rank 7 against pivot rank 4 recurses right. The partitioning and pivot selection are executable; what is proved is the recurse-which-side decision at these instances. Correctness of the selection and its linear expected time 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.quickselect` prints this classification.

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

quickselect/target-in-left :
  → lis/extends? 2 4 = data/true

quickselect/left-target-below-pivot :
  → 2 ≤ 4

quickselect/target-in-right :
  → lis/extends? 7 4 = data/false