Reference · Finite types, distributions and Markov chains

rainbow.math.finite.value-iteration

Finite types, distributions and Markov chainssrc/rainbow/math/finite/value_iteration.clj4 definitions, 7 theorems

Finite Bellman optimality and bounded value iteration over exact rationals.

bellman/nnrat-action-backup.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (value : S → ℚ≥0) (x₁ : S) (x₂ : A)
  → ℚ≥0

value/nnrat-greedy-action.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0) (x₁ : S)
  → A

value/nnrat-optimality-step.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0) (x₁ : S)
  → ℚ≥0

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

bellman/nnrat-action-backup-unfold.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (value : S → ℚ≥0) (state : S) (action : A)
  → bellman/nnrat-action-backup S A states transition reward discount value state action = reward state action + discount · probability/nnrat-expectation S states (transition state action) value

value/nnrat-greedy-action-is-admissible.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0)
  (fallback-admissible : ∀ (current : S), fallback current ∈ actions)
  (value : S → ℚ≥0) (state : S)
  → value/nnrat-greedy-action S A actions fallback backup value state ∈ actions

value/nnrat-optimality-step-dominates.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0) (state : S) (candidate : A)
  (candidate-member : candidate ∈ actions)
  → backup value state candidate ≤ value/nnrat-optimality-step S A actions fallback backup value state

value/nnrat-optimality-step-unfold.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0) (state : S)
  → value/nnrat-optimality-step S A actions fallback backup value state = backup value state (value/nnrat-greedy-action S A actions fallback backup value state)

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

value/nnrat-iterate-successor.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (steps : ℕ) (initial : S → ℚ≥0)
  → iterate (data/succ steps) initial = (fun x₁ => fun value => fun state => value/nnrat-optimality-step S A actions fallback backup value state) steps (iterate steps initial)
  where iterate := value/nnrat-iterate S A actions fallback backup

value/nnrat-optimality-state-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-state right-state : S)
  (left-action : A)
  (left-member : left-action ∈ actions)
  (right-action : A)
  (right-member : right-action ∈ actions)
  → proposition/conjunction (backup value left-state left-action ≤ step₁) (backup value right-state right-action ≤ 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