Reference · Algorithm guarantees

rainbow.algorithms.proofs.eligibility-traces

Algorithm guaranteessrc/rainbow/algorithms/proofs/eligibility_traces.clj2 definitions, 2 theorems

Eligibility traces (TD(lambda)) over exact rationals. Each state keeps a nonnegative eligibility trace that decays by the discount-times-lambda factor and is incremented when the state is visited: `e' = (gamma*lambda) * e + 1`. On a temporal-difference error the state value is updated in proportion to its trace: `value' = value + rate * trace * td-error`, spreading credit back over recently visited states (AHoF D63). The trace is a nonnegative rational and the update reuses signed scaling of the TD error. Scope (measured by the kernel): this module has 2 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.eligibility-traces` prints this classification.

learning/eligibility-trace-update :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

learning/trace-weighted-update :
  (x₁ x₂ : ℚ≥0) (x₃ x₄ : ℚ)
  → ℚ

learning/eligibility-trace-update-unfold :
  (decay trace : ℚ≥0)
  → learning/eligibility-trace-update decay trace = decay · trace + 1

learning/trace-weighted-update-unfold :
  (rate trace : ℚ≥0) (td-error value : ℚ)
  → learning/trace-weighted-update rate trace td-error value = value + signed/scale (rate · trace) td-error