Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.knn

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

AHoF K-Nearest Neighbors (instance-based classification): classify a query point by a majority vote among its K nearest training examples -- a non-parametric method with no training phase (lazy learning). Given the per-class vote counts among the K neighbors, the predicted label is the class with the most votes: knn-predict votes = argmax_c votes(c) over exact-rational (integer) vote counts (returning the predicted class index), defined as the argmax-index fold over the class vote counts. Proved native and axiom-free, as worked instances: votes [2, 4, 1] predict class 1; and the worked certificates 2 <= 4 and 1 <= 4 (native nnrat/at-most). That the prediction is a plurality class for all vote vectors is not proved here; the distance computation and the K-nearest selection are executable. 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.knn` prints this classification.

Depends onalgorithms.proofs.argmax-index

knn/predict :
  (x₁ : List ℚ≥0)
  → ℕ

knn/predicts-plurality-class :
  → knn/predict [2, 4, 1] = 1

knn/plurality-dominates-zero :
  → 2 ≤ 4

knn/plurality-dominates-two :
  → 1 ≤ 4