Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.quadratic-fit

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

AHoF O10 Quadratic Fit Search: fit a parabola through three sampled points and step toward its vertex, keeping the three lowest-valued points as the bracket shrinks. The bracket-tracking core is the minimum of the three sampled values: best-of-two a b = if (a <= b) then a else b best-of-three a b c = best-of-two (best-of-two a b) c over exact rationals (min via the nnrat eliminator). Proved native and axiom-free: the pairwise min, the three-way min, and worked instances retaining the smallest sampled value. Requires audit/decide-nnrat-at-most, logic/if-data (both in the D63 checkpoint). 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.quadratic-fit` prints this classification.

quadfit/best-of-two :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

quadfit/best-of-three :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

quadfit/keeps-smallest :
  → quadfit/best-of-three 3/4 1/2 1 = 1/2

quadfit/keeps-smallest-first :
  → quadfit/best-of-three 1/2 3/4 1 = 1/2

quadfit/pairwise-min :
  → ppo/nnrat-min 3/4 1/2 = 1/2