Reference · Algorithm guarantees

rainbow.algorithms.proofs.sarsa

Algorithm guaranteessrc/rainbow/algorithms/proofs/sarsa.clj1 definitions, 2 theorems

SARSA on-policy temporal-difference control over signed rationals. SARSA shares the temporal-difference update with Q-learning -- the new action value is the current value plus the learning rate times the TD error -- but bootstraps from the value of the action actually taken in the next state (on-policy) rather than from the greedy maximum (off-policy). So the SARSA update is exactly the shared Q-update fed the on-policy next value (AHoF D62); when that next value equals the greedy value the two updates coincide. 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.sarsa` prints this classification.

learning/signed-sarsa-update :
  (x₁ : ℚ≥0) (x₂ : ℚ) (x₃ : ℚ≥0) (x₄ x₅ : ℚ)
  → ℚ

learning/signed-sarsa-update-unfold :
  (rate : ℚ≥0) (reward : ℚ) (discount : ℚ≥0) (next-action-value current : ℚ)
  → learning/signed-q-update rate reward discount next-action-value current = current + signed/scale rate (error)
  where error := learning/signed-td-error reward discount next-action-value current

learning/signed-sarsa-equals-q-update :
  (rate : ℚ≥0) (reward : ℚ) (discount : ℚ≥0) (next-action-value current : ℚ)
  → update = update
  where update := learning/signed-q-update rate reward discount next-action-value current