Reference · Finite types, distributions and Markov chains

rainbow.math.finite.greedy-optimal

Finite types, distributions and Markov chainssrc/rainbow/math/finite/greedy_optimal.clj0 definitions, 3 theorems

Greedy policy extraction from a finite nnrat Bellman fixed point. The key proof transports the optimality fixed-point proposition across the opaque optimality-step unfold equality. It never reduces greedy action or finite argmax. The second theorem isolates the only remaining semantic ingredient: uniqueness of fixed points for the extracted policy operator. Native and axiom-free on D63.

Depends onmath.finite.bellman-value-optimality

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

value/nnrat-greedy-bellman-policy-fixes-optimal-value.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ≥0) (discount : ℚ≥0)
  (fallback : S → A) (normalized : markov/nnrat-rows-normalized S A states transition)
  (optimal-value : S → ℚ≥0)
  (optimal-fixed-point : ∀ (state : S), value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) optimal-value state = optimal-value state)
  (state : S)
  → bellman/nnrat-action-backup S A states transition reward discount optimal-value state (action) = optimal-value state
  where action := value/nnrat-greedy-action S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) optimal-value state

value/nnrat-greedy-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) (optimal-value : S → ℚ≥0)
  (optimal-fixed-point : ∀ (state : S), value/nnrat-optimality-step S A actions fallback backup optimal-value state = optimal-value state)
  (policy-value : S → ℚ≥0)
  (policy-value-fixed : ∀ (state : S), backup policy-value state (action state) = policy-value state)
  (fixed-points-unique : ∀ (left : S → ℚ≥0), ∀ (right : S → ℚ≥0), ∀ (left-fixed : ∀ (state : S), backup left state (action state) = left state), ∀ (right-fixed : ∀ (state : S), backup right state (action state) = right state), ∀ (state : S), left state = right state)
  (state : S)
  → policy-value state = optimal-value state
  where action := value/nnrat-greedy-action S A actions fallback backup optimal-value