Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.general-descent

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/general_descent.clj5 definitions, 3 theorems

AHoF O13 worked general descent, instantiated to gradient descent. The pluggable skeleton is fed a constant unit gradient as the direction, a constant rate 1/2 as the step size, and `update(point, rate, direction) = point - rate * direction`. From the signed point 1 this reproduces the gradient descent trajectory 1, 1/2, 0, -1/2 -- the same descent as O17, but assembled through the general three-plug-in skeleton rather than a bespoke step. The trajectory values are proved by signed cross-product equivalence. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.general-descent` prints this classification.

ahof-o13/direction :
  (x₁ : ℚ)
  → ℚ

ahof-o13/step-size :
  (x₁ : ℚ)
  → ℚ≥0

ahof-o13/update :
  (x₁ : ℚ) (x₂ : ℚ≥0) (x₃ : ℚ)
  → ℚ

ahof-o13/initial :
  → ℚ

ahof-o13/trajectory :
  (x₁ : ℕ)
  → ℚ

ahof-o13/trajectory-values :
  → proposition/conjunction (iterate = signed/from-nnrat 1/2) (conjunction)
  where conjunction := proposition/conjunction (optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update 2 ahof-d62/reward = signed/from-nnrat 0) (optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update 3 ahof-d62/reward = signed/make 0 1/2)
  where iterate := optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update 1 ahof-d62/reward

ahof-o13/descent-recurrence :
  → proposition/conjunction (iterate = ahof-d62/reward) (∀ (steps : ℕ), optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update (data/succ steps) ahof-d62/reward = (fun x₂ => fun previous => step previous) steps (optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update steps ahof-d62/reward))
  where iterate := optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update 0 ahof-d62/reward
  where step := optimization/general-descent-step ahof-o13/direction ahof-o13/step-size ahof-o31/update

ahof-o13/general-descent :
  → proposition/conjunction (conjunction) (proposition/conjunction (iterate = ahof-d62/reward) (∀ (steps : ℕ), optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update (data/succ steps) ahof-d62/reward = (fun x₄ => fun previous => step previous) steps (optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update steps ahof-d62/reward)))
  where conjunction := proposition/conjunction (optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update 1 ahof-d62/reward = signed/from-nnrat 1/2) (proposition/conjunction (optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update 2 ahof-d62/reward = signed/from-nnrat 0) (optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update 3 ahof-d62/reward = signed/make 0 1/2))
  where iterate := optimization/general-descent-iterate ahof-o13/direction ahof-o13/step-size ahof-o31/update 0 ahof-d62/reward
  where step := optimization/general-descent-step ahof-o13/direction ahof-o13/step-size ahof-o31/update