Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.dec-pomdp-dp

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

AHoF D82 Dec-POMDP (Dynamic Programming): back up joint-policy values, keeping the larger of two candidate joint-policy values: prefers-joint-zero? v0 v1 = decide (v1 <= v0) backup-value v0 v1 = if (v1 <= v0) then v0 else v1 over exact rationals. Proved native and axiom-free: preference decision, max value, switch. 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.dec-pomdp-dp` prints this classification.

dec-pomdp/prefers-joint-zero? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

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

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

dec-pomdp/value-is-maximum :
  → ac-mcts/node-value 3/4 1/2 = 3/4

dec-pomdp/switches :
  → bo/is-safe 1/2 3/4 = data/false