Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.baseline-subtraction

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

AHoF D48 Baseline Subtraction: the variance-reduction wrapper for policy-gradient estimators. Subtracting a state-dependent baseline from the return before weighting the score leaves the gradient unbiased but reduces its variance. The baselined per-trajectory contribution weights the score by the ADVANTAGE (return minus baseline): contribution advantage score = advantage * score over exact nonnegative rationals, where the advantage = return - baseline is supplied (its sign handling and the optimal-baseline choice are executable). Proved native and axiom-free: the contribution unfolds to advantage * score for all advantages and scores, and two worked instances (3 * 4 = 12, and a zero advantage 0 * 9 = 0) that reduce by reflexivity on the exact arithmetic. Unbiasedness and variance reduction are the classical properties of the baseline; they are not proved here. Requires nnrat/multiply and nnrat/at-most (in the D63 checkpoint). 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.baseline-subtraction` prints this classification.

baseline/contribution :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

baseline/contribution-unfold :
  (advantage score : ℚ≥0)
  → baseline/contribution advantage score = advantage · score

baseline/contribution-example :
  → baseline/contribution 3 4 = 12

baseline/zero-advantage-cancels :
  → baseline/contribution 0 9 = 0