Reference · Algorithm guarantees

rainbow.algorithms.proofs.reward-to-go

Algorithm guaranteessrc/rainbow/algorithms/proofs/reward_to_go.clj1 definitions, 4 theorems

AHoF D47 Reward-to-Go: the future-reward sum used by policy-gradient methods to reduce variance (REINFORCE uses the whole-trajectory return as the weight; reward-to-go replaces it with only the rewards from step t onward). The reward-to-go of a reward suffix is the fold-sum of that suffix: reward-to-go rewards = fold add 0 rewards and it satisfies the suffix recurrence that makes it computable in one backward pass: reward-to-go (r :: rest) = r + reward-to-go rest This is exact natural-number arithmetic (`algebra/nat-add` folded over the list, identity 0). Discounting and the score-function weighting stay an executable concern; what is proved here is the reward-to-go fold, its one-step suffix recurrence (by reflexivity through the List.rec computation rule), and worked suffix totals that reduce by reflexivity. Scope (measured by the kernel): this module has 3 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.reward-to-go` prints this classification.

reward-to-go/reward-to-go :
  (x₁ : List ℕ)
  → ℕ

reward-to-go/suffix-recurrence :
  (head : ℕ) (tail : List ℕ)
  → list/nat-sum (data/cons ℕ head tail) = algebra/nat-add head (list/nat-sum tail)

reward-to-go/full-return-example :
  → list/nat-sum [3, 2, 1] = 6

reward-to-go/suffix-return-example :
  → list/nat-sum [2, 1] = 3

reward-to-go/empty-return-example :
  → list/nat-sum [] = 0