Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.q-learning

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

AHoF D61 worked temporal-difference (Q-learning) update over signed rationals. A single state-action estimate starts overvalued at 1 with reward 0, discount 0, and next value 0, so the temporal-difference error is -1: the estimate is too high. With learning rate 1/2 the first Q-values are 1, 1/2, 1/4, halving toward the true value 0. Proved native and axiom-free: the TD error is -1 and the values after one and two steps are 1/2 and 1/4. Convergence of the trajectory is not proved here. Only signed rationals make the negative temporal-difference error representable. 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.q-learning` prints this classification.

ahof-d61/rate :
  → ℚ≥0

ahof-d61/reward :
  → ℚ

ahof-d61/discount :
  → ℚ≥0

ahof-d61/next-value :
  → ℚ

ahof-d61/initial :
  → ℚ

ahof-d61/trajectory :
  (x₁ : ℕ)
  → ℚ

ahof-d61/td-error-is-negative :
  → learning/signed-td-error ahof-d63/value ahof-d49/initial ahof-d63/value ahof-d62/reward = signed/make 0 1

ahof-d61/q-values :
  → proposition/conjunction (iterate = signed/from-nnrat 1/2) (iterate₁ = signed/from-nnrat 1/4)
  where iterate := learning/signed-q-iterate ahof-v40/lo ahof-d63/value ahof-d49/initial ahof-d63/value 1 ahof-d62/reward
  where iterate₁ := learning/signed-q-iterate ahof-v40/lo ahof-d63/value ahof-d49/initial ahof-d63/value 2 ahof-d62/reward

ahof-d61/q-learning :
  → proposition/conjunction (error = signed/make 0 1) (conjunction)
  where conjunction := proposition/conjunction (learning/signed-q-iterate ahof-v40/lo ahof-d63/value ahof-d49/initial ahof-d63/value 1 ahof-d62/reward = signed/from-nnrat 1/2) (learning/signed-q-iterate ahof-v40/lo ahof-d63/value ahof-d49/initial ahof-d63/value 2 ahof-d62/reward = signed/from-nnrat 1/4)
  where error := learning/signed-td-error ahof-d63/value ahof-d49/initial ahof-d63/value ahof-d62/reward