Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.set-cover

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

AHoF Set Cover (greedy approximation): given a universe of elements and a collection of subsets, choose the fewest subsets whose union is the whole universe. The greedy algorithm -- whose approximation ratio is the harmonic number H_n = 1 + 1/2 + ... + 1/n <= 1 + ln(n) for n elements (Chvatal 1979), logarithmic and asymptotically best possible for this NP-hard problem -- repeatedly picks the subset that covers the most still-UNCOVERED elements. Given each candidate subset's count of newly-covered elements, the pick is the argmax: greedy-pick coverage = argmax_s coverage(s) over exact-rational (integer) coverage counts (returning the chosen subset index). Proved native and axiom-free: the greedy pick is defined as the argmax-index fold over coverage counts; a worked pick on counts [2,5,3] selects subset 1; and the worked certificates 2 <= 5 and 3 <= 5 as native nnrat/at-most. The set/element bookkeeping and coverage recomputation are executable; what is proved is the maximum-coverage pick at this instance. The H_n <= 1 + ln(n) approximation bound of greedy set cover is classical and not proved here. Requires argmax-index/argmax-index, nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and 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.set-cover` prints this classification.

Depends onalgorithms.proofs.argmax-index

set-cover/greedy-pick :
  (x₁ : List ℚ≥0)
  → ℕ

set-cover/picks-max-coverage :
  → knn/predict [2, 5, 3] = 1

set-cover/chosen-covers-most-vs-zero :
  → 2 ≤ 5

set-cover/chosen-covers-most-vs-two :
  → 3 ≤ 5