Reference · Algorithm guarantees

rainbow.algorithms.proofs.general-descent

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

The general descent skeleton over signed rationals: the parent of the whole descent family. A step delegates to three pluggable functions -- a direction `direction(point)`, a step length `step-size(point)`, and an update rule `update(point, step, direction)` -- and composes them into the next point. Every concrete descent method (gradient descent, momentum, Newton, ...) is this skeleton with particular plug-ins (AHoF O13). The skeleton is proved once; instances reuse its unfold and iterate recurrence.

optimization/general-descent-step :
  (direction : ℚ → ℚ) (step-size : ℚ → ℚ≥0) (update : ℚ → ℚ≥0 → ℚ → ℚ) (point : ℚ)
  → ℚ

optimization/general-descent-iterate :
  (direction : ℚ → ℚ) (step-size : ℚ → ℚ≥0) (update : ℚ → ℚ≥0 → ℚ → ℚ) (x₁ : ℕ) (x₂ : ℚ)
  → ℚ

optimization/general-descent-step-unfold :
  (direction : ℚ → ℚ) (step-size : ℚ → ℚ≥0) (update : ℚ → ℚ≥0 → ℚ → ℚ) (point : ℚ)
  → optimization/general-descent-step direction step-size update point = update point (step-size point) (direction point)

optimization/general-descent-iterate-zero :
  (direction : ℚ → ℚ) (step-size : ℚ → ℚ≥0) (update : ℚ → ℚ≥0 → ℚ → ℚ) (initial : ℚ)
  → optimization/general-descent-iterate direction step-size update 0 initial = initial

optimization/general-descent-iterate-successor :
  (direction : ℚ → ℚ) (step-size : ℚ → ℚ≥0) (update : ℚ → ℚ≥0 → ℚ → ℚ) (steps : ℕ)
  (initial : ℚ)
  → iterate (data/succ steps) initial = (fun x₁ => fun previous => optimization/general-descent-step direction step-size update previous) steps (iterate steps initial)
  where iterate := optimization/general-descent-iterate direction step-size update