Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.momentum

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

AHoF O19 worked Polyak momentum over signed rationals with pair state. Momentum coefficient 1 and rate 1 with a constant unit gradient, starting from position 0 and velocity 2. One step gives velocity `1 * 2 - 1 * 1 = 1` and position `0 + 1 = 1`: the momentum term `1 * 2 = 2` carries the previous velocity, which plain gradient descent lacks. The signed values are proved by cross-product equivalence; the recurrence is the generic iterate zero/successor. 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.momentum` prints this classification.

ahof-o19/beta :
  → ℚ≥0

ahof-o19/rate :
  → ℚ≥0

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

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

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

ahof-o19/first-velocity-is-one :
  → product/second ℚ ℚ (iterate) = signed/from-nnrat 1
  where iterate := optimization/momentum-iterate ahof-o20/beta ahof-o20/beta ahof-o17/gradient 1 ahof-o19/initial

ahof-o19/first-position-is-one :
  → product/first ℚ ℚ (iterate) = signed/from-nnrat 1
  where iterate := optimization/momentum-iterate ahof-o20/beta ahof-o20/beta ahof-o17/gradient 1 ahof-o19/initial

ahof-o19/momentum-recurrence :
  → proposition/conjunction (iterate = ahof-o19/initial) (∀ (steps : ℕ), optimization/momentum-iterate ahof-o20/beta ahof-o20/beta ahof-o17/gradient (data/succ steps) ahof-o19/initial = (fun x₂ => fun previous => step previous) steps (optimization/momentum-iterate ahof-o20/beta ahof-o20/beta ahof-o17/gradient steps ahof-o19/initial))
  where iterate := optimization/momentum-iterate ahof-o20/beta ahof-o20/beta ahof-o17/gradient 0 ahof-o19/initial
  where step := optimization/momentum-step ahof-o20/beta ahof-o20/beta ahof-o17/gradient

ahof-o19/momentum :
  → proposition/conjunction (second = signed/from-nnrat 1) (proposition/conjunction (first = signed/from-nnrat 1) (proposition/conjunction (iterate = ahof-o19/initial) (∀ (steps : ℕ), optimization/momentum-iterate ahof-o20/beta ahof-o20/beta ahof-o17/gradient (data/succ steps) ahof-o19/initial = (fun x₈ => fun previous => step previous) steps (optimization/momentum-iterate ahof-o20/beta ahof-o20/beta ahof-o17/gradient steps ahof-o19/initial))))
  where first := product/first ℚ ℚ (optimization/momentum-iterate ahof-o20/beta ahof-o20/beta ahof-o17/gradient 1 ahof-o19/initial)
  where iterate := optimization/momentum-iterate ahof-o20/beta ahof-o20/beta ahof-o17/gradient 0 ahof-o19/initial
  where second := product/second ℚ ℚ (optimization/momentum-iterate ahof-o20/beta ahof-o20/beta ahof-o17/gradient 1 ahof-o19/initial)
  where step := optimization/momentum-step ahof-o20/beta ahof-o20/beta ahof-o17/gradient