Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-greedy-policy

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

Greedy policy extraction from a signed Bellman fixed point. For the concrete Bellman model with ordinary nnrat transitions and arbitrary signed rewards/values, the runtime finite argmax defines a statewise policy. The policy is admissible whenever the fallback is admissible. At an assumed Bellman fixed value, the backup selected by that policy is pointwise equivalent to the fixed value, because the signed optimality operator is definitionally the backup at its greedy action. This is a mathematical optimal-action certificate. It does not construct a fixed point, verify a policy-evaluation executable, or connect to running Clojure code. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-residual-certificate

value/nnrat-transition-signed-greedy-policy-is-admissible.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (discount : ℚ≥0)
  (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (fixed-value : S → ℚ) (state : S)
  → (fun state₁ => value/signed-greedy-action S A actions fallback (fun value => fun state₂ => fun action => backup value state₂ action) fixed-value state₁) state ∈ actions
  where backup := bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (transition state₃ action₁ next-state)) reward (signed/from-nnrat discount)

value/nnrat-transition-signed-greedy-policy-attains-fixed-value.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (discount : ℚ≥0)
  (fallback : S → A) (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => backup value state₁ action) fixed-value state = fixed-value state)
  (state : S)
  → (fun value => fun state₁ => fun action => backup value state₁ action) fixed-value state ((fun state₁ => value/signed-greedy-action S A actions fallback (fun value => fun state₂ => fun action => backup₁ value state₂ action) fixed-value state₁) state) = fixed-value state
  where backup := bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount)
  where backup₁ := bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (transition state₃ action₁ next-state)) reward (signed/from-nnrat discount)

value/nnrat-transition-signed-greedy-fixed-point-policy-certificate.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (discount : ℚ≥0)
  (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => backup value state₁ action) fixed-value state = fixed-value state)
  → proposition/conjunction (∀ (state : S), (fun state₁ => action state₁) state ∈ actions) (∀ (state : S), (fun value => fun state₁ => fun action => backup value state₁ action) fixed-value state ((fun state₁ => action₁ state₁) state) = fixed-value state)
  where action := value/signed-greedy-action S A actions fallback (fun value => fun state₂ => fun action => bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount) value state₂ action) fixed-value
  where action₁ := value/signed-greedy-action S A actions fallback (fun value => fun state₂ => fun action => bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => …⟨1⟩ …⟨7⟩) reward (signed/from-nnrat discount) value state₂ action) fixed-value
  where backup := bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount)