Reference · Algorithm guarantees

rainbow.algorithms.proofs.coordinate-search

Algorithm guaranteessrc/rainbow/algorithms/proofs/coordinate_search.clj4 definitions, 4 theorems

Cyclic coordinate search over signed-rational pair state. A cycle optimizes along each coordinate in turn: it descends the first coordinate, then descends the second coordinate of the *already-updated* state, so the coordinate updates compose sequentially (the MAP-OVER / reduce-over-dimensions pattern, AHoF O32). Each coordinate update is a one-dimensional gradient step; the two partial gradients are parameters. Scope (measured by the kernel): this module has 4 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.coordinate-search` prints this classification.

search/coordinate-update-first :
  (rate : ℚ≥0) (gradient : data/Product ℚ ℚ → ℚ≥0) (s : data/Product ℚ ℚ)
  → data/Product ℚ ℚ

search/coordinate-update-second :
  (rate : ℚ≥0) (gradient : data/Product ℚ ℚ → ℚ≥0) (s : data/Product ℚ ℚ)
  → data/Product ℚ ℚ

search/coordinate-cycle :
  (rate : ℚ≥0) (gradient-first gradient-second : data/Product ℚ ℚ → ℚ≥0)
  (s : data/Product ℚ ℚ)
  → data/Product ℚ ℚ

search/coordinate-iterate :
  (rate : ℚ≥0) (gradient-first gradient-second : data/Product ℚ ℚ → ℚ≥0) (x₁ : ℕ)
  (x₂ : data/Product ℚ ℚ)
  → data/Product ℚ ℚ

search/coordinate-update-first-unfold :
  (rate : ℚ≥0) (gradient : data/Product ℚ ℚ → ℚ≥0) (s : data/Product ℚ ℚ)
  → search/coordinate-update-first rate gradient s = data/pair ℚ ℚ (product/first ℚ ℚ s - signed/from-nnrat (rate · gradient s)) (product/second ℚ ℚ s)

search/coordinate-update-second-unfold :
  (rate : ℚ≥0) (gradient : data/Product ℚ ℚ → ℚ≥0) (s : data/Product ℚ ℚ)
  → search/coordinate-update-second rate gradient s = data/pair ℚ ℚ (product/first ℚ ℚ s) (product/second ℚ ℚ s - signed/from-nnrat (rate · gradient s))

search/coordinate-cycle-unfold :
  (rate : ℚ≥0) (gradient-first gradient-second : data/Product ℚ ℚ → ℚ≥0)
  (s : data/Product ℚ ℚ)
  → search/coordinate-cycle rate gradient-first gradient-second s = search/coordinate-update-second rate gradient-second (first)
  where first := search/coordinate-update-first rate gradient-first s

search/coordinate-iterate-zero :
  (rate : ℚ≥0) (gradient-first gradient-second : data/Product ℚ ℚ → ℚ≥0)
  (initial : data/Product ℚ ℚ)
  → search/coordinate-iterate rate gradient-first gradient-second 0 initial = initial