Reference · Finite types, distributions and Markov chains

rainbow.math.finite.policy-iteration-optimal

Finite types, distributions and Markov chainssrc/rainbow/math/finite/policy_iteration_optimal.clj0 definitions, 2 theorems

Stationary finite-policy improvement implies the optimal Bellman equation. The proof keeps optimality-step and finite argmax opaque. Stationarity is represented by the two semantic facts it supplies at every state: the policy-value fixed-point equation and greedy consistency. Their transitive composition gives an optimality fixed point. A separate corollary isolates fixed-point uniqueness as the only additional ingredient needed to identify that value with an optimum. Native and axiom-free on D63.

Depends onmath.finite.greedy-optimal

value/nnrat-stationary-policy-satisfies-optimality-equation.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (policy : S → A) (value : S → ℚ≥0)
  (policy-fixed : ∀ (state : S), value state = backup value state (policy state))
  (greedy-consistent : ∀ (state : S), backup value state (policy state) = step state)
  (state : S)
  → value state = step state
  where step := value/nnrat-optimality-step S A actions fallback backup value

value/nnrat-stationary-policy-value-is-optimal-given-uniqueness.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (policy : S → A) (policy-value : S → ℚ≥0)
  (policy-value-fixed : ∀ (state : S), policy-value state = backup policy-value state (policy state))
  (greedy-consistent : ∀ (state : S), backup policy-value state (policy state) = step policy-value state)
  (optimal-value : S → ℚ≥0)
  (optimal-fixed : ∀ (state : S), step optimal-value state = optimal-value state)
  (optimality-fixed-points-unique : ∀ (left : S → ℚ≥0), ∀ (right : S → ℚ≥0), ∀ (left-fixed : ∀ (state : S), step left state = left state), ∀ (right-fixed : ∀ (state : S), step right state = right state), ∀ (state : S), left state = right state)
  (state : S)
  → policy-value state = optimal-value state
  where step := value/nnrat-optimality-step S A actions fallback backup