Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.eligibility-traces

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

AHoF D63 worked eligibility traces (TD(lambda)) over exact rationals. With a decay factor gamma*lambda = 1/2 and a current trace 1, the visited state's trace becomes (1/2)*1 + 1 = 3/2. With learning rate 1/2, a TD error 1, and a current value 0, the trace-weighted update raises the value by (1/2)*1 to 1/2. The trace and the updated value are proved by cross-product equivalence. 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.eligibility-traces` prints this classification.

ahof-d63/decay :
  → ℚ≥0

ahof-d63/trace :
  → ℚ≥0

ahof-d63/rate :
  → ℚ≥0

ahof-d63/td-error :
  → ℚ

ahof-d63/value :
  → ℚ

ahof-d63/updated-trace :
  → ℚ≥0

ahof-d63/updated-value :
  → ℚ

ahof-d63/trace-is-three-halves :
  → ahof-d63/updated-trace = 3/2

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

ahof-d63/eligibility-traces :
  → proposition/conjunction (ahof-d63/updated-trace = 3/2) (ahof-d63/updated-value = signed/from-nnrat 1/2)