Reference · Algorithm guarantees

rainbow.algorithms.proofs.nearest-neighbor

Algorithm guaranteessrc/rainbow/algorithms/proofs/nearest_neighbor.clj1 definitions, 1 theorems

Nearest-neighbor value function approximation over exact rationals. Given two stored data points with their distances to a query and their stored values, the approximator returns the value of the nearer point (the one with the smaller distance), decided by exact rational comparison. This is the nonparametric value lookup of a nearest-neighbor approximator (AHoF D25): the approximated value at a query is the value carried by the closest data point, selected by a decidable distance comparison. Scope (measured by the kernel): this module has 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.nearest-neighbor` prints this classification.

decision/nearest-value :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

decision/nearest-value-unfold :
  (distance-a value-a distance-b value-b : ℚ≥0)
  → decision/nearest-value distance-a value-a distance-b value-b = logic/if-data ℚ≥0 (most = most) (most) value-a value-b
  where most := audit/decide-nnrat-at-most distance-a distance-b