Reference · Algorithm guarantees

rainbow.algorithms.proofs.gradient-ascent

Algorithm guaranteessrc/rainbow/algorithms/proofs/gradient_ascent.clj2 definitions, 4 theorems

Bounded fixed-rate gradient ascent over exact nonnegative rationals. The update `point + rate * (gradient point)` is the shared ITERATE skeleton of AHoF D49 and the many policy/parameter ascent methods that plug a different gradient estimator into the same loop. The gradient is a first-class function argument, so this engine is reused by specialization rather than re-derived.

optimization/nnrat-ascent-step :
  (gradient : ℚ≥0 → ℚ≥0) (rate point : ℚ≥0)
  → ℚ≥0

optimization/nnrat-ascent-iterate :
  (gradient : ℚ≥0 → ℚ≥0) (rate : ℚ≥0) (x₁ : ℕ) (x₂ : ℚ≥0)
  → ℚ≥0

optimization/nnrat-ascent-step-unfold :
  (gradient : ℚ≥0 → ℚ≥0) (rate point : ℚ≥0)
  → optimization/nnrat-ascent-step gradient rate point = point + rate · gradient point

optimization/nnrat-ascent-iterate-zero :
  (gradient : ℚ≥0 → ℚ≥0) (rate initial : ℚ≥0)
  → optimization/nnrat-ascent-iterate gradient rate 0 initial = initial

optimization/nnrat-ascent-iterate-successor :
  (gradient : ℚ≥0 → ℚ≥0) (rate : ℚ≥0) (steps : ℕ) (initial : ℚ≥0)
  → iterate (data/succ steps) initial = (fun x₁ => fun previous => optimization/nnrat-ascent-step gradient rate previous) steps (iterate steps initial)
  where iterate := optimization/nnrat-ascent-iterate gradient rate

optimization/nnrat-ascent-step-transfer :
  (gradient : ℚ≥0 → ℚ≥0) (rate left-point right-point : ℚ≥0)
  → proposition/conjunction (step₁ = left-point + rate · gradient left-point) (step = right-point + rate · gradient right-point)
  where step := optimization/nnrat-ascent-step gradient rate right-point
  where step₁ := optimization/nnrat-ascent-step gradient rate left-point