Reference · Foundations

rainbow.math.temporal-difference

Foundationssrc/rainbow/math/temporal_difference.clj4 definitions, 3 theorems

Bounded temporal-difference (Q-learning) updates over signed rationals. The temporal-difference error `reward + discount * next - current` is a signed quantity that can be negative when the current estimate is too high, and the update nudges the estimate by the rate-scaled error: `current + rate * error`. Signed rationals make the negative correction representable without any kernel primitive subtraction. The update rule is the shared ITERATE skeleton of AHoF D61 Q-learning, D62 Sarsa, and Expected Sarsa (only the target differs).

signed/scale :
  (x₁ : ℚ≥0) (x₂ : ℚ)
  → ℚ

learning/signed-td-error :
  (x₁ : ℚ) (x₂ : ℚ≥0) (x₃ x₄ : ℚ)
  → ℚ

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

learning/signed-q-iterate :
  (x₁ : ℚ≥0) (x₂ : ℚ) (x₃ : ℚ≥0) (x₄ : ℚ) (x₅ : ℕ) (x₆ : ℚ)
  → ℚ

learning/signed-td-error-unfold :
  (reward : ℚ) (discount : ℚ≥0) (next current : ℚ)
  → learning/signed-td-error reward discount next current = reward + signed/scale discount next - current

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

learning/signed-q-iterate-zero :
  (rate : ℚ≥0) (reward : ℚ) (discount : ℚ≥0) (next initial : ℚ)
  → learning/signed-q-iterate rate reward discount next 0 initial = initial