Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.prim

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

AHoF Prim's Minimum Spanning Tree: grow an MST from a start vertex by repeatedly adding the minimum-weight edge that CROSSES THE CUT between the in-tree vertices and the rest. Unlike Kruskal (which sorts all edges globally and uses union-find), Prim maintains a frontier of candidate crossing edges and greedily takes the lightest. Choosing between two crossing edges by weight is: lighter-edge wa ea wb eb = if wa <= wb then ea else eb (return the endpoint/id of the lighter crossing edge), over exact-rational edge weights. Defined: the two-edge selection. Proved native and axiom-free, as worked instances: between weights 1 and 4 the first edge (to vertex 2) is chosen, between weights 6 and 3 the second (to vertex 5) is chosen, and the worked certificate 1 <= 4 (native nnrat/at-most). The cut property (a lightest crossing edge belongs to some MST) and the minimality of the tree Prim grows are classical and not proved here. The frontier priority queue and cut maintenance are executable. Requires nat, audit/decide-nnrat-at-most, logic/if-data, 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.prim` prints this classification.

prim/lighter-edge :
  (x₁ : ℚ≥0) (x₂ : ℕ) (x₃ : ℚ≥0) (x₄ : ℕ)
  → ℕ

prim/picks-lighter-crossing :
  → kmeans/assign 1 2 4 5 = 2

prim/picks-second-when-lighter :
  → kmeans/assign 6 2 3 5 = 5

prim/chosen-edge-is-minimum :
  → 1 ≤ 4