Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.greedy-policy

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

AHoF greedy policy extraction: given a state-action value function Q(s, .), the greedy policy chooses the action of maximal value, pi(s) = argmax_a Q(s, a), greedy-value(s) = max_a Q(s, a). This is the policy-improvement step at the heart of value iteration and policy iteration. Classically, when Q is the exact action-value function Q-pi of a policy pi, the policy greedy with respect to it is at least as good as pi itself (policy improvement, not proved here). That is improvement over the policy Q was computed for, not global optimality: being greedy with respect to an arbitrary Q, or even to an exact Q-pi, does not make a policy at least as good as every other one; only a greedy policy for the optimal Q* is optimal. Defined: the greedy action via the argmax-index fold and the greedy value via the list-maximum fold. Proved native and axiom-free, as worked instances for Q = [5,7,4]: the greedy action is 1, the greedy value is 7, and the worked certificates 5 <= 7 and 4 <= 7 (native nnrat/at-most). Dominance of the greedy value for every Q is not proved here. The Q-value estimates are executable / supplied. Requires argmax-index/argmax-index, list-maximum/maximum, nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and the D63 checkpoint. Scope (measured by the kernel): this module has 4 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.greedy-policy` prints this classification.

Depends onalgorithms.proofs.argmax-indexalgorithms.proofs.list-maximum

greedy/action :
  (x₁ : List ℚ≥0)
  → ℕ

greedy/value :
  (x₁ : List ℚ≥0)
  → ℚ≥0

greedy/action-example :
  → greedy/action [5, 7, 4] = 1

greedy/value-example :
  → greedy/value [5, 7, 4] = 7

greedy/dominates-action-zero :
  → 5 ≤ 7

greedy/dominates-action-two :
  → 4 ≤ 7