Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.qmdp

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

AHoF D22 QMDP (POMDP planning approximation): approximate the value of an action under partial observability by weighting the fully-observable Q-values by the current belief over states, qmdp-value b0 q0 b1 q1 = b0 * Q(s0, a) + b1 * Q(s1, a) (a two-state belief; the general form sums over all states). QMDP acts as if all uncertainty resolves after one step -- cheap and often effective. Proved native and axiom-free: the belief-weighted value; a worked value (stated as rational equivalence via the cross-product certificate, since the mixed weights yield a non-lowest-terms pair); and that under a certain belief (b0 = 1) the value reduces to the single state's Q-value -- reducing by reflexivity. The underlying MDP Q-values and the belief update are executable; what is proved is the belief-weighted value combination. Requires nnrat/add, nnrat/multiply, nnrat/equivalent (all in the D63 checkpoint). 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.qmdp` prints this classification.

qmdp/value :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

qmdp/value-example :
  → qmdp/value 1/2 1 1/2 3 = 2

qmdp/certain-belief :
  → qmdp/value 1 5 0 9 = 5