Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.pbvi

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

AHoF D72 PBVI (Point-Based Value Iteration for POMDPs): maintain value at a finite set of belief points, backing up each point's value as the maximum over candidate alpha vectors of the value at that belief. With two candidates the backup keeps the larger value, preferring candidate 0 when its value is at least candidate 1's: prefers-candidate-zero? v0 v1 = decide (v1 <= v0) backup-value v0 v1 = if (v1 <= v0) then v0 else v1 (the larger value) over exact rationals. Proved native and axiom-free: the preference decision, the backup (max) value, and the switch when candidate 1 is larger. Requires audit/decide-nnrat-at-most, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 3 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.pbvi` prints this classification.

pbvi/prefers-candidate-zero? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

pbvi/backup-value :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

pbvi/prefers-higher-candidate :
  → bo/is-safe 3/4 1/2 = data/true

pbvi/backup-is-maximum :
  → fsc/node-value 3/4 1/2 = 3/4

pbvi/switches-candidate :
  → bo/is-safe 1/2 3/4 = data/false