Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.pomdp-online

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

Kochenderfer 'Algorithms for Decision Making' Ch.21-23 online / point-based / controller POMDP cores as higher-order-function compositions, proved axiom-free (each with its most distinctive structural property), extending the 222 AHoF catalog: D21.8 Perseus (randomized PBVI) : backup keeps the better alpha -> value never decreases D22.3 DESPOT (anytime search) : maintains a lower<=upper value bracket D21.16 Freudenthal grid VI : barycentric interpolation, bounded by the corners D23.3 controller policy iteration : finite-state-controller node = expected successor value Reuses nnrat-minmax (monotone backup, bracket via transitivity) and nnrat/wsum2 + convex-at-most-max (interpolation / expectation). Native and axiom-free; chains nnrat-convex on d63.

Depends onmath.rational.nnrat.convex

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

pomdp/despot-lower :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

pomdp/despot-upper :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

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

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

pomdp/perseus-improves :
  (old candidate : ℚ≥0)
  → old ≤ mo/vega-select old candidate

pomdp/despot-bracket :
  (l u : ℚ≥0)
  → opt/ldp-min-norm l u ≤ mo/vega-select l u

pomdp/freudenthal-within-corners :
  (w0 w1 v0 v1 : ℚ≥0)
  (hw : w0 + w1 = 1)
  → bo/bootstrap-632 w0 w1 v0 v1 ≤ minmax/max v0 v1

pomdp/controller-node-value-example :
  → bo/bootstrap-632 1/2 1/2 1 0 = 1/2