Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.mesh-adaptive

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

AHoF O39 Mesh Adaptive Direct Search (MADS): a derivative-free direct-search method that probes the objective at mesh points around the incumbent. Each poll step steps from the current point along a poll direction by the current mesh size: poll x delta direction = x + delta * direction over the finite-vector state. When a poll point improves the objective the mesh is coarsened; otherwise it is refined -- an executable control concern. The poll directions are drawn to grow dense on the unit sphere (the property that makes MADS convergent), also executable. What is proved here is the deterministic poll-step recurrence and worked instances from a zero incumbent, where a unit mesh step lands exactly on the poll direction. Requires the shared finite-vector operations (vector/add, vector/scale) over signed rationals -- carried by the D63 checkpoint via the vector layer. 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.mesh-adaptive` prints this classification.

Depends onmath.finite.vector

mads/poll :
  (x₁ : List ℚ) (x₂ : ℚ≥0) (x₃ : List ℚ)
  → List ℚ

mads/poll-unfold :
  (x : List ℚ) (delta : ℚ≥0) (direction : List ℚ)
  → mads/poll x delta direction = vector/add x (vector/scale delta direction)

mads/poll-unit-2d-example :
  → mads/poll [signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 3, signed/from-nnrat 2] = [signed/from-nnrat 3, signed/from-nnrat 2]

mads/poll-unit-3d-example :
  → mads/poll [signed/from-nnrat 0, signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6] = [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6]