Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.hierarchical-clustering

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

AHoF Agglomerative Hierarchical Clustering: build a hierarchy of clusters (a dendrogram) bottom-up -- start with each point in its own cluster and repeatedly MERGE THE TWO CLOSEST clusters, under a linkage that defines inter-cluster distance (single / complete / average). Unlike k-means it needs no preset k and yields a full tree that can be cut at any level. At each step it selects the closest of two candidate cluster pairs by linkage distance: closest-pair dab pab dcd pcd = if dab <= dcd then pab else pcd (return the id of the smaller-distance pair), over exact-rational distances. Proved native and axiom-free: the closest-pair selection; a worked choice of the nearer pair; and the certificate that the merged pair's distance is at most the alternative's (native nnrat/at-most) -- the greedy merge that shapes the dendrogram. The linkage distances and the merge bookkeeping are executable; what is proved is the closest-pair merge decision. 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.hierarchical-clustering` prints this classification.

hierarchical/closest-pair :
  (x₁ : ℚ≥0) (x₂ : ℕ) (x₃ : ℚ≥0) (x₄ : ℕ)
  → ℕ

hierarchical/merges-closest-pair :
  → dijkstra/closer-vertex 2 0 6 1 = 0

hierarchical/merges-second-when-closer :
  → dijkstra/closer-vertex 9 0 4 1 = 1

hierarchical/merged-is-closest :
  → 2 ≤ 6