Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.pomdp-bounds

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/pomdp_bounds.clj5 definitions, 5 theorems

Kochenderfer 'Algorithms for Decision Making' Ch.21 offline POMDP value-function bounds, expressed as higher-order-function compositions over belief-weighted alpha-vector values and proved axiom-free, extending the 222 AHoF catalog: D21.2 QMDP : value = max_a sum_s b(s) Q(s,a) (upper bound) D21.3 fast informed bnd : max over observation-corrected action alpha-values D21.5 blind lower bound : value of a single fixed action forever (<= QMDP) D21.10 sawtooth iteration: belief value <= convex interpolation of corner values belief-action-value reuses nnrat/wsum2 (b0*q0 + b1*q1); the max/bounds reuse nnrat-minmax; the sawtooth upper bound reuses nnrat/convex-at-most-max. Native and axiom-free; chains nnrat-weighted-sum, nnrat-minmax, nnrat-convex on d63.

Depends onmath.rational.nnrat.convex

pomdp/belief-action-value :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

pomdp/qmdp-value :
  (x₁ x₂ x₃ x₄ x₅ x₆ : ℚ≥0)
  → ℚ≥0

pomdp/blind-value :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

pomdp/fib-value :
  (x₁ x₂ x₃ x₄ x₅ x₆ : ℚ≥0)
  → ℚ≥0

pomdp/sawtooth-interp :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

pomdp/qmdp-dominates-action0 :
  (b0 b1 q00 q10 q01 q11 : ℚ≥0)
  → bo/bootstrap-632 b0 b1 q00 q10 ≤ pomdp/fib-value b0 b1 q00 q10 q01 q11

pomdp/qmdp-dominates-action1 :
  (b0 b1 q00 q10 q01 q11 : ℚ≥0)
  → bo/bootstrap-632 b0 b1 q01 q11 ≤ pomdp/fib-value b0 b1 q00 q10 q01 q11

pomdp/blind-below-qmdp :
  (b0 b1 q00 q10 q01 q11 : ℚ≥0)
  → pomdp/blind-value b0 b1 q00 q10 ≤ pomdp/fib-value b0 b1 q00 q10 q01 q11

pomdp/fib-dominates-action0 :
  (b0 b1 c00 c10 c01 c11 : ℚ≥0)
  → bo/bootstrap-632 b0 b1 c00 c10 ≤ pomdp/fib-value b0 b1 c00 c10 c01 c11

pomdp/sawtooth-below-max-corner :
  (w0 w1 c0 c1 : ℚ≥0)
  (hw : w0 + w1 = 1)
  → bo/bootstrap-632 w0 w1 c0 c1 ≤ minmax/max c0 c1