Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.gradient-descent

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

AHoF O17 worked bounded gradient descent over signed rationals. A constant unit gradient with rate 1/2 from the signed point 1 produces the exact trajectory 1, 1/2, 0, -1/2: descent drives the parameter through zero and into negative values, which only signed rationals can represent. 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.gradient-descent` prints this classification.

ahof-o17/rate :
  → ℚ≥0

ahof-o17/gradient :
  (x₁ : ℚ)
  → ℚ≥0

ahof-o17/initial :
  → ℚ

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

ahof-o17/trajectory-values :
  → proposition/conjunction (iterate = signed/from-nnrat 1/2) (conjunction)
  where conjunction := proposition/conjunction (optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient 2 ahof-d62/reward = signed/from-nnrat 0) (optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient 3 ahof-d62/reward = signed/make 0 1/2)
  where iterate := optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient 1 ahof-d62/reward

ahof-o17/descent-recurrence :
  → proposition/conjunction (iterate = ahof-d62/reward) (∀ (steps : ℕ), optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient (data/succ steps) ahof-d62/reward = (fun x₂ => fun previous => step previous) steps (optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient steps ahof-d62/reward))
  where iterate := optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient 0 ahof-d62/reward
  where step := optimization/signed-descent-step ahof-d63/rate ahof-o17/gradient

ahof-o17/gradient-descent :
  → proposition/conjunction (conjunction) (proposition/conjunction (iterate = ahof-d62/reward) (∀ (steps : ℕ), optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient (data/succ steps) ahof-d62/reward = (fun x₄ => fun previous => step previous) steps (optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient steps ahof-d62/reward)))
  where conjunction := proposition/conjunction (optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient 1 ahof-d62/reward = signed/from-nnrat 1/2) (proposition/conjunction (optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient 2 ahof-d62/reward = signed/from-nnrat 0) (optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient 3 ahof-d62/reward = signed/make 0 1/2))
  where iterate := optimization/signed-descent-iterate ahof-d63/rate ahof-o17/gradient 0 ahof-d62/reward
  where step := optimization/signed-descent-step ahof-d63/rate ahof-o17/gradient