Reference · Algorithm guarantees

rainbow.algorithms.proofs.powell

Algorithm guaranteessrc/rainbow/algorithms/proofs/powell.clj1 definitions, 3 theorems

AHoF O33 Powell's Method: the conjugate search-direction generated from a cycle of coordinate line minimizations. Where cyclic coordinate search (O32) descends along fixed axes, Powell adds a new direction equal to the net displacement of a whole cycle and rotates it into the direction set: net-direction = cycle-end - cycle-start This is the finite-vector difference of the cycle endpoints -- the distinctive Powell step (the direction-set update). The line minimizations themselves and the direction-set bookkeeping stay in the executable reference; what is proved here is the net-direction recurrence and worked instances. 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.powell` prints this classification.

Depends onmath.finite.vector

powell/net-direction :
  (x₁ x₂ : List ℚ)
  → List ℚ

powell/net-direction-unfold :
  (start end : List ℚ)
  → powell/net-direction start end = vector/subtract end start

powell/net-direction-example :
  → powell/net-direction [signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 2, signed/from-nnrat 3] = [signed/from-nnrat 2, signed/from-nnrat 3]

powell/net-direction-3d-example :
  → powell/net-direction [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 1, signed/from-nnrat 2, signed/from-nnrat 3]