Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.policy-evaluation-backup

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

AHoF D-family Policy Evaluation: the evaluation half of policy iteration. For a fixed policy pi, the state value satisfies the linear Bellman expectation equation; a one-step backup is bellman-eval reward gamma next-value = reward + gamma * next-value where reward is the expected immediate reward under pi and next-value is the (discounted) value of the successor state. Classically, iterating this backup converges to the policy's value function (a contraction with modulus gamma < 1); that is not proved here. Proved native and axiom-free: the backup combination; a worked backup; and a worked myopic case (reward 4, discount 0, next-value 9 gives value 4: the immediate reward) -- reducing by reflexivity. The transition/reward model is executable; what is proved is the Bellman expectation backup. Requires nnrat/add, nnrat/multiply (both in the D63 checkpoint). NOTE ON THE NAMESPACE: this proof originally occupied `rainbow.algorithms.proofs.ahof.policy-evaluation`, whose previous contents it replaced. Those contents were the `ahof-d20/*` declarations that the AHoF D20 ledger entry names as its specification, so replacing them silently invalidated a credited catalog row. The original module is restored under its own name and this proof lives here. Scope (measured by the kernel): this module has 2 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.policy-evaluation-backup` prints this classification.

policy-eval/backup :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

policy-eval/backup-example :
  → pagerank/update 1 1/2 3 = 5/2

policy-eval/myopic-at-zero-discount :
  → pagerank/update 4 0 9 = 4