Reference · Algorithm guarantees

rainbow.algorithms.proofs.hooke-jeeves

Algorithm guaranteessrc/rainbow/algorithms/proofs/hooke_jeeves.clj2 definitions, 5 theorems

AHoF O34 Hooke-Jeeves pattern search: the exploratory probe and the pattern (acceleration) move over vector-valued state. An exploratory move adds a step vector to the base; when it improves, the pattern move accelerates in the same direction by extrapolating past the improved point: probe = base + step pattern-move = improved + (improved - base) Both are finite-vector operations (add, subtract), reusing the n-dimensional vector state. This is a direct-search method: no gradient, just structured moves. The acceptance test that chooses whether to keep a probe stays an executable concern; what is proved here is the two move recurrences and worked two- and three-dimensional instances. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values) and 2 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.hooke-jeeves` prints this classification.

Depends onmath.finite.vector

hooke/probe :
  (x₁ x₂ : List ℚ)
  → List ℚ

hooke/pattern-move :
  (x₁ x₂ : List ℚ)
  → List ℚ

hooke/probe-unfold :
  (base step : List ℚ)
  → hooke/probe base step = vector/add base step

hooke/pattern-move-unfold :
  (base improved : List ℚ)
  → hooke/pattern-move base improved = vector/add improved (vector/subtract improved base)

hooke/probe-example :
  → hooke/probe [signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 1, signed/from-nnrat 2] = [signed/from-nnrat 1, signed/from-nnrat 2]

hooke/pattern-move-example :
  → hooke/pattern-move [signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 1, signed/from-nnrat 2] = [signed/from-nnrat 2, signed/from-nnrat 4]

hooke/pattern-move-3d-example :
  → hooke/pattern-move [signed/from-nnrat 0, signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 1, signed/from-nnrat 2, signed/from-nnrat 3] = [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6]