Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.cosine-similarity

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

AHoF Cosine Similarity: measure the similarity of two vectors by the cosine of the angle between them -- the dot product normalized by the product of their magnitudes, cosine dot-product magnitude-product = (a . b) / (|a| |b|). It is 1 for parallel vectors, 0 for orthogonal ones, and ignores magnitude, which is why it is the standard similarity for document term-vectors (TF-IDF), word and sentence embeddings, and recommendation. Proved native and axiom-free: the cosine as exact rational division of the dot product by the magnitude product; a worked similarity; and that identical unit-aligned vectors (dot product equal to the magnitude product) have cosine 1. The dot product and the magnitudes (a square root) are executable; what is proved is the normalized similarity. Requires nnrat/divide (division is the rational-division capability, composed here), nnrat/equivalent, 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.cosine-similarity` prints this classification.

Depends onmath.rational.division

cosine/similarity :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

cosine/cosine-example :
  → accuracy/accuracy 3 4 = 3/4

cosine/aligned-vectors-cosine-one :
  → accuracy/accuracy 5 5 = 1