Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.naive-bayes

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/naive_bayes.clj2 definitions, 4 theorems

AHoF D-family Naive Bayes classifier: predict a class from features assumed conditionally independent given the class. The (unnormalized) posterior score of a class is its prior times the product of per-feature likelihoods, nb-score prior likelihoods = prior * (likelihood_1 * likelihood_2 * ...), and the predicted class is the argmax of these scores over the classes. Proved native and axiom-free: the class score composes the proved list-product fold over the feature likelihoods with the prior; a worked score; the prediction is the proved argmax-index fold over the class scores; a worked classification; and the certificate that the predicted class's score dominates every other class's (native nnrat/at-most). The likelihood/prior estimates are executable; what is proved is the score product and the argmax prediction. Requires list-product/product, argmax-index/argmax-index, nnrat/multiply, 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 4 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.naive-bayes` prints this classification.

Depends onalgorithms.proofs.list-productalgorithms.proofs.argmax-index

naive-bayes/score :
  (x₁ : ℚ≥0) (x₂ : List ℚ≥0)
  → ℚ≥0

naive-bayes/classify :
  (x₁ : List ℚ≥0)
  → ℕ

naive-bayes/score-example :
  → naive-bayes/score 1 [2, 3] = 6

naive-bayes/classify-example :
  → knn/predict [6, 4, 5] = 0

naive-bayes/prediction-dominates-one :
  → 4 ≤ 6

naive-bayes/prediction-dominates-two :
  → 5 ≤ 6