Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.alpha-vector

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

AHoF D71 Alpha Vector (Exact POMDP value function): the optimal value at a belief b is the maximum over the alpha-vector set of the inner products <alpha, b>. With two alpha vectors the value picks the larger of the two dot products, and the dominant vector is the one whose value is at least the other's: selects-dominant? v0 v1 = decide (v1 <= v0) best-value v0 v1 = if (v1 <= v0) then v0 else v1 (the larger value) over exact rationals. Proved native and axiom-free: the dominance decision, the best-value (max) selection, and the switch when the second vector dominates. 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.alpha-vector` prints this classification.

alpha-vector/selects-dominant? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

alpha-vector/best-value :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

alpha-vector/dominant-vector-selected :
  → estimation/mle-prefers 3/4 1/2 = data/true

alpha-vector/value-is-maximum :
  → ac-mcts/node-value 3/4 1/2 = 3/4

alpha-vector/switches-dominance :
  → estimation/mle-prefers 1/2 3/4 = data/false