Reference · Algorithm guarantees

rainbow.algorithms.proofs.pattern-search

Algorithm guaranteessrc/rainbow/algorithms/proofs/pattern_search.clj3 definitions, 3 theorems

Generalized pattern search over exact rationals: a derivative-free poll that moves to the best of a set of candidate points. Each candidate carries an objective value; the poll picks the candidate with the smaller value (an argmin by decided comparison), and the move is accepted only when the polled best improves on the current objective. This is the poll-and-accept structure of pattern search (AHoF O35); no gradient is used, only objective comparisons. Scope (measured by the kernel): this module has 3 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.pattern-search` prints this classification.

search/poll-better :
  (x₁ x₂ : ℚ≥0) (x₃ x₄ : ℚ)
  → ℚ

search/poll-improves :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

search/pattern-move :
  (x₁ x₂ : ℚ≥0) (x₃ x₄ : ℚ)
  → ℚ

search/poll-better-unfold :
  (value-a value-b : ℚ≥0) (point-a point-b : ℚ)
  → search/poll-better value-a value-b point-a point-b = logic/if-data ℚ (most = most) (most) point-a point-b
  where most := audit/decide-nnrat-at-most value-a value-b

search/poll-improves-unfold :
  (best-value current-value : ℚ≥0)
  → failmon/safe? best-value current-value = audit/decide-nnrat-at-most best-value current-value

search/pattern-move-unfold :
  (best-value current-value : ℚ≥0) (best-point current-point : ℚ)
  → search/pattern-move best-value current-value best-point current-point = logic/if-data ℚ (failmon/safe? best-value current-value = failmon/safe? best-value current-value) (failmon/safe? best-value current-value) best-point current-point