Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.jaccard-similarity

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

AHoF Jaccard Similarity: measure how alike two SETS are by the size of their intersection over the size of their union, jaccard intersection-size union-size = |A intersect B| / |A union B|, a value in [0, 1] that is 1 for identical sets and 0 for disjoint ones. It underlies near-duplicate detection, document/shingle similarity (with MinHash), recommendation overlap, and clustering-quality indices. Proved native and axiom-free: the similarity as exact rational division of the intersection size by the union size; a worked similarity; and that identical sets (intersection = union) have similarity 1. The set intersection/union computations are executable; what is proved is the Jaccard ratio. 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.jaccard-similarity` prints this classification.

Depends onmath.rational.division

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

jaccard/jaccard-example :
  → accuracy/accuracy 2 5 = 2/5

jaccard/identical-sets-similarity-one :
  → accuracy/accuracy 4 4 = 1