Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.gae

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

AHoF D42 Generalized Advantage Estimation: estimate the advantage function as an exponentially-weighted (by gamma*lambda) sum of temporal-difference errors, A_t = delta_t + (gamma*lambda) delta_{t+1} + (gamma*lambda)^2 delta_{t+2} + ... trading bias against variance via lambda. A truncated two-step estimate is gae2 d0 d1 w = d0 + w * d1 (w = gamma*lambda) over exact-rational TD errors and weight. Proved native and axiom-free: the weighted-advantage combination; a worked estimate; and that with weight 0 the advantage collapses to the one-step TD error delta_t (the high-bias / TD(0) end of the lambda spectrum) -- reducing by reflexivity. The TD errors and the value baseline are executable; what is proved is the geometrically-weighted advantage combination. Requires nnrat/add, nnrat/multiply (both in the D63 checkpoint). Scope (measured by the kernel): this module has 2 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.gae` prints this classification.

gae/gae2 :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

gae/gae2-example :
  → gae/gae2 1 1 1/2 = 3/2

gae/collapses-to-td :
  → gae/gae2 2 5 0 = 2