Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.rollout

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

AHoF D32 Rollout with Heuristic: estimate a state's value by simulating the rollout policy forward and averaging the returns. The return of a single simulated trajectory is the (discounted) sum of its rewards; here the two-step undiscounted return is trajectory-return r1 r2 = r1 + r2 over exact nonnegative rationals (the value estimate averages this over several simulations). Proved native and axiom-free: the trajectory return, and the guarantee that a return dominates each of its reward steps (r1 <= return), so a rollout with a nonnegative reward step never underestimates that step's contribution. The rollout policy, the simulation, and the mean over trajectories (a division) are executable concerns; what is proved here is the deterministic return accumulation. Requires nnrat/add, nnrat/at-most, and the decidable nnrat order (D63). Scope (measured by the kernel): this module has 2 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.rollout` prints this classification.

rollout/trajectory-return :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

rollout/trajectory-return-unfold :
  (r1 r2 : ℚ≥0)
  → astar/f-value r1 r2 = r1 + r2

rollout/trajectory-return-example :
  → astar/f-value 3 4 = 7

rollout/return-dominates-step :
  → 3 ≤ astar/f-value 3 4