Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.pattern-search

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

AHoF O35 worked generalized pattern search over exact rationals, minimizing f(x) = x^2 from x = 2 with step 1. The poll evaluates the two candidates x + 1 = 3 (objective 9) and x - 1 = 1 (objective 1); the smaller objective is 1, so the poll picks the point 1. Since the polled objective 1 improves on the current objective f(2) = 4, the move is accepted to 1 -- a derivative-free step using only objective comparisons. The selections are proved by reflexivity of the decided comparisons. 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.pattern-search` prints this classification.

ahof-o35/forward-point :
  → ℚ

ahof-o35/backward-point :
  → ℚ

ahof-o35/current-point :
  → ℚ

ahof-o35/polled-best :
  → ℚ

ahof-o35/poll-picks-backward :
  → ahof-o35/polled-best = ahof-o35/backward-point

ahof-o35/move-accepts-best :
  → search/pattern-move 1 4 ahof-o35/polled-best ahof-o31/initial = ahof-o35/backward-point

ahof-o35/pattern-search :
  → proposition/conjunction (ahof-o35/polled-best = ahof-o35/backward-point) (move = ahof-o35/backward-point)
  where move := search/pattern-move 1 4 ahof-o35/polled-best ahof-o31/initial