Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bayes-adaptive-mdp

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

AHoF D60 Bayes-Adaptive MDP: plan in the belief-MDP over unknown model parameters, where the value of an action is the posterior-belief-weighted average of its value under each candidate model: expected-value b0 v0 b1 v1 = b0 * v0 + b1 * v1 (belief weights b0, b1 summing to one). With equal belief 1/2, 1/2 over model values 1/2, 3/4 the expected value is 5/8; with belief concentrated on the first model (weights 1, 0) it is that model's value 1/2. Values are proved by cross-product equivalence. Proved native and axiom-free. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.bayes-adaptive-mdp` prints this classification.

bamdp/expected-value :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

bamdp/balanced-belief :
  → ℚ≥0

bamdp/concentrated-belief :
  → ℚ≥0

bamdp/expected-value-unfold :
  (b0 v0 b1 v1 : ℚ≥0)
  → bamdp/expected-value b0 v0 b1 v1 = b0 · v0 + b1 · v1

bamdp/balanced-is-five-eighths :
  → bamdp/balanced-belief = 5/8

bamdp/concentrated-is-model-value :
  → bamdp/concentrated-belief = 1/2

bamdp/bayes-adaptive :
  → proposition/conjunction (bamdp/balanced-belief = 5/8) (bamdp/concentrated-belief = 1/2)