Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.nearest-neighbor

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

AHoF D25 worked nearest-neighbor value function approximation over exact rationals. Two stored data points carry values 3/4 and 1/4. When the query is nearer the first point (distance 1/4 versus 1/2) the approximated value is 3/4; when a second query is nearer the second point (distance 1/2 versus 1/4) the approximated value is 1/4. The approximation follows the nearest point, decided by exact rational distance comparison, proved by reflexivity of the decided comparison. 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.nearest-neighbor` prints this classification.

ahof-d25/value-a :
  → ℚ≥0

ahof-d25/value-b :
  → ℚ≥0

ahof-d25/query-near-a :
  → ℚ≥0

ahof-d25/query-near-b :
  → ℚ≥0

ahof-d25/query-near-a-is-value-a :
  → ahof-d25/query-near-a = ahof-d25/value-a

ahof-d25/query-near-b-is-value-b :
  → ahof-d25/query-near-b = ahof-d25/value-b

ahof-d25/nearest-neighbor :
  → proposition/conjunction (ahof-d25/query-near-a = ahof-d25/value-a) (ahof-d25/query-near-b = ahof-d25/value-b)