Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.sequential-decision

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

Kochenderfer 'Algorithms for Decision Making' game-theory + model-based-RL cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: D24.8 iterated best response : best-response value = max over own actions (dominates) D16.7 R-MAX : optimistic value = max(realistic, Vmax); optimism bound D16.5 prioritized sweeping : sweep the state of maximum Bellman-residual priority D16.4 model-based RL (Dyna) : certainty-equivalence value = expectation over model D17.6 Q-learning w/ replay : replay target = reward + discount * max_a Q(s',a) Selection/optimism/priority reuse nnrat-minmax; the certainty-equivalence value and the replay Bellman target reuse nnrat/wsum2 and nnrat add/multiply. Native and axiom-free; chains nnrat-convex (-> wsum2, minmax) on d63.

Depends onmath.rational.nnrat.convex

game/best-response-value :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

rl/rmax-value :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

rl/sweep-priority :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

rl/model-based-value :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

rl/replay-target :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

game/best-response-dominates :
  (p0 p1 : ℚ≥0)
  → p0 ≤ rl/rmax-value p0 p1

rl/rmax-optimistic :
  (realistic vmax : ℚ≥0)
  → realistic ≤ rl/rmax-value realistic vmax

rl/sweep-picks-max-priority :
  (r0 r1 : ℚ≥0)
  → r1 ≤ rl/rmax-value r0 r1

rl/model-based-example :
  → eda/pipe-update 1/2 1/2 1 0 = 1/2

rl/replay-target-example :
  → rl/replay-target 1 1/2 1 0 = 3/2