Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.kruskal

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

AHoF Kruskal's Minimum Spanning Tree: build an MST by scanning edges in increasing weight order and adding each edge unless it would form a cycle -- i.e. unless its endpoints are already in the same connected component. Cycle detection uses the proved union-find connectivity: an edge is accepted exactly when its endpoints are NOT yet connected, accepts-edge? ra rb = NOT (connected? ra rb) over the exact-rational component representatives. Proved native and axiom-free: the acceptance rule as the negation of union-find connectivity; that an edge between different components is added (it grows the forest); that an edge within one component is rejected (it would close a cycle); and (via the imported union-find theorems) the underlying connectivity certificates. The edge sort and the union updates are executable; what is proved is the cycle-free acceptance decision. Requires union-find/connected?, logic/if-data (union-find composed here) and the D63 checkpoint. Scope (measured by the kernel): this module has 2 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.kruskal` prints this classification.

Depends onalgorithms.proofs.ahof.union-find

kruskal/accepts-edge? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

kruskal/adds-cross-component-edge :
  → kruskal/accepts-edge? 3 5 = data/true

kruskal/rejects-cycle-edge :
  → kruskal/accepts-edge? 3 3 = data/false