Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.kmeans

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

AHoF K-Means Clustering (Lloyd's algorithm): partition points into k clusters by alternating an ASSIGNMENT step (assign each point to the nearest cluster centroid) and an UPDATE step (move each centroid to the mean of its assigned points), until assignments stop changing. Classically, the within-cluster variance decreases monotonically, which guarantees convergence (not proved here). The assignment step selects, for a point, the closer of two candidate centroids by (squared) distance: assign da ca db cb = if da <= db then ca else cb (return the id of the nearer centroid), over exact-rational distances. Proved native and axiom-free: the nearest-centroid assignment; a worked assignment; and the certificate, for the worked point, that the chosen centroid's distance is at most the alternative's (2 <= 7, native nnrat/at-most). The centroid update (a mean) and the distance computation are executable; what is proved is the nearest-centroid assignment. 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.kmeans` prints this classification.

kmeans/assign :
  (x₁ : ℚ≥0) (x₂ : ℕ) (x₃ : ℚ≥0) (x₄ : ℕ)
  → ℕ

kmeans/assigns-to-nearest :
  → kmeans/assign 2 0 7 1 = 0

kmeans/assigns-to-second-when-nearer :
  → kmeans/assign 9 0 3 1 = 1

kmeans/assigned-is-nearest :
  → 2 ≤ 7