Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.rbf-surrogate

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

AHoF O61 Radial Basis Function surrogate: an interpolating surrogate model that predicts by a weighted sum of radial basis functions centered at the sampled points. With basis-function evaluations phi_i at the query and fitted weights w_i, the prediction is the weighted sum (shown for two centers; the general case folds this over all centers): predict w1 phi1 w2 phi2 = w1 * phi1 + w2 * phi2 over exact nonnegative rationals. The radial kernel phi(r) = exp(-(r/l)^2) (or a multiquadric with a square root) is transcendental and stays an executable concern -- its VALUES are supplied as rationals; the fitted weights come from solving the interpolation system, also executable. What is proved here is the deterministic prediction combination and worked instances that reduce by reflexivity on the exact rational arithmetic. Requires nnrat/add and nnrat/multiply (in the D63 checkpoint). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 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.ahof.rbf-surrogate` prints this classification.

rbf/predict :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

rbf/predict-unfold :
  (w1 phi1 w2 phi2 : ℚ≥0)
  → qmdp/value w1 phi1 w2 phi2 = w1 · phi1 + w2 · phi2

rbf/predict-example :
  → qmdp/value 2 3 1 4 = 10

rbf/predict-single-basis :
  → qmdp/value 2 3 0 4 = 6