Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.sarsa

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

AHoF D62 worked SARSA on-policy update over signed rationals. With learning rate 1/2, reward 1, discount 1, an on-policy next action value 0, and a current action value 0, the TD error is (1 + 1*0) - 0 = 1, and the SARSA update raises the value to 0 + (1/2)*1 = 1/2. The updated value is proved by signed cross-product equivalence, and the update is shown to coincide with the shared Q-update on the same bootstrap value. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.sarsa` prints this classification.

ahof-d62/rate :
  → ℚ≥0

ahof-d62/reward :
  → ℚ

ahof-d62/discount :
  → ℚ≥0

ahof-d62/next-value :
  → ℚ

ahof-d62/current :
  → ℚ

ahof-d62/updated :
  → ℚ

ahof-d62/updated-is-one-half :
  → ahof-d62/updated = signed/from-nnrat 1/2

ahof-d62/coincides-with-q-update :
  → update = update
  where update := learning/signed-q-update ahof-v40/lo ahof-d62/reward ahof-o20/beta ahof-d63/value ahof-d63/value

ahof-d62/sarsa :
  → proposition/conjunction (ahof-d62/updated = signed/from-nnrat 1/2) (update = update)
  where update := learning/signed-q-update ahof-v40/lo ahof-d62/reward ahof-o20/beta ahof-d63/value ahof-d63/value