Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.actor-critic

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/actor_critic.clj3 definitions, 4 theorems

AHoF D53 Actor-Critic: the critic bootstraps a temporal-difference target from the immediate reward plus the discounted value of the next state, and the actor is updated toward it. The bootstrap target is: td-target reward discount next-value = reward + discount * next-value. A reward 1/4 with discount 1/2 and next-value 1/2 gives the target 1/4 + 1/4 = 1/2; an undiscounted reward-only target (discount 0) is the reward 1/4. Values are proved by cross-product equivalence. Proved native and axiom-free. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values) and 1 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.ahof.actor-critic` prints this classification.

actor-critic/td-target :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

actor-critic/bootstrap-target :
  → ℚ≥0

actor-critic/reward-only-target :
  → ℚ≥0

actor-critic/td-target-unfold :
  (reward discount next-value : ℚ≥0)
  → actor-critic/td-target reward discount next-value = reward + discount · next-value

actor-critic/bootstrap-is-half :
  → actor-critic/bootstrap-target = 1/2

actor-critic/reward-only-is-reward :
  → actor-critic/reward-only-target = 1/4

actor-critic/actor-critic :
  → proposition/conjunction (actor-critic/bootstrap-target = 1/2) (actor-critic/reward-only-target = 1/4)