Reference · Algorithm guarantees

rainbow.algorithms.proofs.conjugate-gradient

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

Conjugate gradient descent over signed rationals with pair-valued state. The state carries a position and a search direction. Each step forms a new direction from the current negative gradient plus beta times the remembered previous direction, `d' = -gradient(x) + beta * d`, then moves the position `x' = x + alpha * d'`. The remembered direction is the closure-with-memory that distinguishes conjugate gradient from plain steepest descent (AHoF O18); the separate step size alpha distinguishes it from momentum. 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.conjugate-gradient` prints this classification.

optimization/conjugate-direction :
  (beta : ℚ≥0) (gradient : ℚ → ℚ) (x d : ℚ)
  → ℚ

optimization/conjugate-step :
  (alpha beta : ℚ≥0) (gradient : ℚ → ℚ) (s : data/Product ℚ ℚ)
  → data/Product ℚ ℚ

optimization/conjugate-iterate :
  (alpha beta : ℚ≥0) (gradient : ℚ → ℚ) (x₁ : ℕ) (x₂ : data/Product ℚ ℚ)
  → data/Product ℚ ℚ

optimization/conjugate-direction-unfold :
  (beta : ℚ≥0) (gradient : ℚ → ℚ) (x d : ℚ)
  → optimization/conjugate-direction beta gradient x d = signed/negate (gradient x) + signed/scale beta d

optimization/conjugate-step-unfold :
  (alpha beta : ℚ≥0) (gradient : ℚ → ℚ) (s : data/Product ℚ ℚ)
  → optimization/conjugate-step alpha beta gradient s = data/pair ℚ ℚ (product/first ℚ ℚ s + scale) (optimization/conjugate-direction beta gradient (product/first ℚ ℚ s) (product/second ℚ ℚ s))
  where scale := signed/scale alpha (optimization/conjugate-direction beta gradient (product/first ℚ ℚ s) (product/second ℚ ℚ s))

optimization/conjugate-iterate-zero :
  (alpha beta : ℚ≥0) (gradient : ℚ → ℚ) (initial : data/Product ℚ ℚ)
  → optimization/conjugate-iterate alpha beta gradient 0 initial = initial