Reference · Algorithm guarantees

rainbow.algorithms.proofs.gradient-descent

Algorithm guaranteessrc/rainbow/algorithms/proofs/gradient_descent.clj2 definitions, 3 theorems

Bounded fixed-rate gradient descent over signed rationals. Descent subtracts the rate-scaled gradient from the current signed point: `point - from-nnrat(rate * gradient point)`. Subtraction is the signed-rational (addition-only) construction, so descent trajectories can pass through zero and become negative without the kernel needing primitive subtraction. This is the descent counterpart of the gradient-ascent engine and the simplest instance of the operations-research descent pattern (AHoF O17).

optimization/signed-descent-step :
  (rate : ℚ≥0) (gradient : ℚ → ℚ≥0) (point : ℚ)
  → ℚ

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

optimization/signed-descent-step-unfold :
  (rate : ℚ≥0) (gradient : ℚ → ℚ≥0) (point : ℚ)
  → optimization/signed-descent-step rate gradient point = point - signed/from-nnrat (rate · gradient point)

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

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