Reference · Finite types, distributions and Markov chains

rainbow.math.finite.async-value-iteration

Finite types, distributions and Markov chainssrc/rainbow/math/finite/async_value_iteration.clj2 definitions, 6 theorems

Asynchronous (Gauss-Seidel) finite Bellman value iteration. The Bellman optimality operator is exactly the one proved for D22 finite value iteration; the only new content is a pluggable state-selection strategy. A `choose?` predicate delegates, per state, whether this stroke applies the optimality backup (selected states) or preserves the previous value (non-selected states). Bounded asynchronous iteration folds a schedule of such selectors over Nat recursion, so the selection order is a first-class strategy rather than a fixed synchronous sweep.

value/nnrat-async-update.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (choose : S → data/Bool) (value : S → ℚ≥0) (x₁ : S)
  → ℚ≥0

value/nnrat-async-iterate.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (schedule : ℕ → S → data/Bool) (x₁ : ℕ)
  (x₂ : S → ℚ≥0) (x₃ : S)
  → ℚ≥0

value/nnrat-async-update-selected.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (choose : S → data/Bool) (value : S → ℚ≥0)
  (state : S)
  (selected : choose state = data/true)
  → value/nnrat-async-update S A actions fallback backup choose value state = value/nnrat-optimality-step S A actions fallback backup value state

value/nnrat-async-update-preserved.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (choose : S → data/Bool) (value : S → ℚ≥0)
  (state : S)
  (non-selected : choose state = data/false)
  → value/nnrat-async-update S A actions fallback backup choose value state = value state

value/nnrat-async-iterate-zero.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (schedule : ℕ → S → data/Bool) (initial : S → ℚ≥0)
  (state : S)
  → value/nnrat-async-iterate S A actions fallback backup schedule 0 initial state = initial state

value/nnrat-async-iterate-successor.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (schedule : ℕ → S → data/Bool) (steps : ℕ)
  (initial : S → ℚ≥0)
  → iterate (data/succ steps) initial = (fun step-index => fun previous => value/nnrat-async-update S A actions fallback backup (schedule step-index) previous) steps (iterate steps initial)
  where iterate := value/nnrat-async-iterate S A actions fallback backup schedule

value/nnrat-async-update-selected-dominates.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (choose : S → data/Bool) (value : S → ℚ≥0)
  (state : S)
  (selected : choose state = data/true)
  (candidate : A)
  (candidate-member : candidate ∈ actions)
  → backup value state candidate ≤ value/nnrat-async-update S A actions fallback backup choose value state

value/nnrat-async-state-schedule-transfer.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0)
  (left-schedule right-schedule : S → data/Bool) (left-state right-state : S)
  (left-selected : left-schedule left-state = data/true)
  (right-selected : right-schedule right-state = data/true)
  → proposition/conjunction (update₁ = step₃) (update = step)
  where step := value/nnrat-optimality-step S A actions fallback backup value right-state
  where step₃ := value/nnrat-optimality-step S A actions fallback backup value left-state
  where update := value/nnrat-async-update S A actions fallback backup right-schedule value right-state
  where update₁ := value/nnrat-async-update S A actions fallback backup left-schedule value left-state