Reference · Finite types, distributions and Markov chains

rainbow.math.finite.policy-iteration

Finite types, distributions and Markov chainssrc/rainbow/math/finite/policy_iteration.clj2 definitions, 7 theorems

Finite exact-rational policy improvement and one composed iteration step.

policy/nnrat-improve.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (current : S → A) (score : S → A → ℚ≥0)
  (x₁ : S)
  → A

policy/nnrat-iteration-step.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (current : S → A)
  (evaluate : (S → A) → S → ℚ≥0) (action-score : (S → ℚ≥0) → S → A → ℚ≥0) (x₁ : S)
  → A

nnrat/equivalent-to-at-most :
  (left right : ℚ≥0)
  (same : left = right)
  → left ≤ right

nnrat/at-most-respects-equivalence :
  (left equivalent-left right equivalent-right : ℚ≥0)
  (same-left : left = equivalent-left)
  (same-right : right = equivalent-right)
  (ordered : equivalent-left ≤ equivalent-right)
  → left ≤ right

policy/nnrat-improve-is-admissible.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (current : S → A) (score : S → A → ℚ≥0)
  (current-admissible : ∀ (state : S), current state ∈ actions)
  (state : S)
  → policy/nnrat-improve S A actions current score state ∈ actions

policy/nnrat-improve-dominates.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (current : S → A) (score : S → A → ℚ≥0)
  (state : S) (candidate : A)
  (member : candidate ∈ actions)
  → score state candidate ≤ score state (policy/nnrat-improve S A actions current score state)

policy/nnrat-iteration-step-unfold.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (current : S → A)
  (evaluate : (S → A) → S → ℚ≥0) (action-score : (S → ℚ≥0) → S → A → ℚ≥0) (state : S)
  → policy/nnrat-iteration-step S A actions current evaluate action-score state = policy/nnrat-improve S A actions current (action-score (evaluate current)) state

policy/nnrat-improvement-model-transfer.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (current : S → A)
  (left-score right-score : S → A → ℚ≥0)
  (same-score : ∀ (state : S), ∀ (action : A), left-score state action = right-score state action)
  (state : S) (candidate : A)
  (member : candidate ∈ actions)
  → right-score state candidate ≤ right-score state (policy/nnrat-improve S A actions current left-score state)

policy/nnrat-improvement-state-transfer.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (current : S → A) (score : S → A → ℚ≥0)
  (current-admissible : ∀ (state : S), current state ∈ actions)
  (state : S)
  → proposition/conjunction (improve ∈ actions) (∀ (candidate : A), ∀ (member : candidate ∈ actions), score state candidate ≤ score state (improve))
  where improve := policy/nnrat-improve S A actions current score state