Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.boyer-moore

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

AHoF Boyer-Moore Majority Vote: find the element that appears MORE than n/2 times (if one exists) in O(n) time and O(1) space -- a single streaming pass that keeps just a candidate and a counter, incrementing on a match and decrementing otherwise (replacing the candidate when the counter hits zero). A verification pass then confirms the survivor is a true majority exactly when its final count strictly exceeds half the length: is-majority? count threshold = decide (threshold <= count) where threshold = ceil((n+1)/2) (a strict majority), over exact-rational counts. Proved native and axiom-free: the majority test; that a count reaching the majority threshold confirms the majority; the certificate that a confirmed majority's count meets the threshold (native nnrat/at-most); and that a count below the threshold means no majority exists. The single-pass candidate/counter scan is executable; what is proved is the majority-confirmation 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.boyer-moore` prints this classification.

boyer-moore/is-majority? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

boyer-moore/confirmed-majority :
  → bo/is-safe 4 4 = data/true

boyer-moore/majority-meets-threshold :
  → 4 ≤ 4

boyer-moore/no-majority :
  → bo/is-safe 3 4 = data/false