Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.conjugate-gradient

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

AHoF O18 worked conjugate gradient over signed rationals with pair state. Step size 1/2, conjugate coefficient 1, gradient the identity, starting from position 2 and direction 1. The new direction is -gradient(2) + 1 * 1 = -2 + 1 = -1 (the remembered direction 1 is folded in), and the position moves 2 + (1/2)(-1) = 3/2. Plain steepest descent would ignore the remembered direction; momentum would move the position by the full new direction rather than the half step. The signed values are proved by cross-product equivalence. Scope (measured by the kernel): this module has 4 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.conjugate-gradient` prints this classification.

ahof-o18/alpha :
  → ℚ≥0

ahof-o18/beta :
  → ℚ≥0

ahof-o18/gradient :
  (x₁ : ℚ)
  → ℚ

ahof-o18/initial :
  → data/Product ℚ ℚ

ahof-o18/trajectory :
  (x₁ : ℕ)
  → data/Product ℚ ℚ

ahof-o18/first-direction-is-negative-one :
  → product/second ℚ ℚ (iterate) = signed/make 0 1
  where iterate := optimization/conjugate-iterate ahof-d63/rate ahof-o20/beta ahof-o18/gradient 1 ahof-o18/initial

ahof-o18/first-position-is-three-halves :
  → product/first ℚ ℚ (iterate) = signed/from-nnrat 3/2
  where iterate := optimization/conjugate-iterate ahof-d63/rate ahof-o20/beta ahof-o18/gradient 1 ahof-o18/initial

ahof-o18/conjugate-recurrence :
  → proposition/conjunction (iterate₁ = ahof-o18/initial) (iterate = step)
  where iterate := optimization/conjugate-iterate ahof-d63/rate ahof-o20/beta ahof-o18/gradient 1 ahof-o18/initial
  where iterate₁ := optimization/conjugate-iterate ahof-d63/rate ahof-o20/beta ahof-o18/gradient 0 ahof-o18/initial
  where step := optimization/conjugate-step ahof-d63/rate ahof-o20/beta ahof-o18/gradient ahof-o18/initial

ahof-o18/conjugate-gradient :
  → proposition/conjunction (second = signed/make 0 1) (conjunction)
  where conjunction := proposition/conjunction (product/first ℚ ℚ (optimization/conjugate-iterate ahof-d63/rate ahof-o20/beta ahof-o18/gradient 1 ahof-o18/initial) = signed/from-nnrat 3/2) (proposition/conjunction (optimization/conjugate-iterate ahof-d63/rate ahof-o20/beta ahof-o18/gradient 0 ahof-o18/initial = ahof-o18/initial) (optimization/conjugate-iterate ahof-d63/rate ahof-o20/beta ahof-o18/gradient 1 ahof-o18/initial = optimization/conjugate-step ahof-d63/rate ahof-o20/beta ahof-o18/gradient ahof-o18/initial))
  where second := product/second ℚ ℚ (optimization/conjugate-iterate ahof-d63/rate ahof-o20/beta ahof-o18/gradient 1 ahof-o18/initial)