Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.natural-gradient

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

AHoF D50 Natural Gradient: the policy update that ascends along the natural gradient -- the ordinary gradient preconditioned by the inverse Fisher information matrix, so the step is invariant to the parameterization of the policy. Given the natural-gradient direction (F^{-1} grad, supplied as problem data), the parameters update by: update theta rate natural = theta + rate * natural over the finite-vector parameter state. The Fisher-information estimate and its inversion are executable / not exact-rational concerns; what is proved here is the deterministic natural-gradient update recurrence and worked instances from a zero-initialized parameter, where a unit-rate step lands exactly on the natural-gradient direction. Requires the shared finite-vector operations (vector/add, vector/scale) over signed rationals -- carried by the D63 checkpoint via the vector layer. Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.natural-gradient` prints this classification.

Depends onmath.finite.vector

natural-gradient/update :
  (x₁ : List ℚ) (x₂ : ℚ≥0) (x₃ : List ℚ)
  → List ℚ

natural-gradient/update-unfold :
  (theta : List ℚ) (rate : ℚ≥0) (natural : List ℚ)
  → mads/poll theta rate natural = vector/add theta (vector/scale rate natural)

natural-gradient/update-unit-2d-example :
  → mads/poll [signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 3, signed/from-nnrat 2] = [signed/from-nnrat 3, signed/from-nnrat 2]

natural-gradient/update-unit-3d-example :
  → mads/poll [signed/from-nnrat 0, signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6] = [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6]