Reference · Finite types, distributions and Markov chains

rainbow.math.finite.policy-evaluation

Finite types, distributions and Markov chainssrc/rainbow/math/finite/policy_evaluation.clj0 definitions, 6 theorems

AHoF D20: bounded finite-policy evaluation over exact rational data.

nat/recursor-successor-constant.{u} :
  (C : Type u) (initial : C) (step : ℕ → C → C) (count : ℕ)
  → data/Nat.rec (fun x₄ => C) initial step (data/succ count) = step count (data/Nat.rec (fun x₈ => C) initial step count)

bellman/nnrat-value-iterate-successor.{u} :
  (A : Type u) (source : Finset A) (transition : A → A → ℚ≥0) (reward : A → ℚ≥0)
  (discount : ℚ≥0) (steps : ℕ) (initial : A → ℚ≥0)
  → data/Nat.rec (fun x₆ => A → ℚ≥0) initial (fun x₇ => fun previous-value => fun state => policy previous-value state) (data/succ steps) = (fun x₈ => fun previous-value => fun candidate => policy previous-value candidate) steps (data/Nat.rec (fun x₁₄ => A → ℚ≥0) initial (fun x₁₅ => fun previous-value => fun state => policy previous-value state) steps)
  where policy := bellman/nnrat-fixed-policy A source transition reward discount

nat/iterate-related.{u} :
  (C : Type u) (R : C → C → Prop) (left-initial right-initial : C)
  (left-step right-step : ℕ → C → C) (same-initial : R left-initial right-initial)
  (same-step : ∀ (count : ℕ), ∀ (left : C), ∀ (right : C), ∀ (same : R left right), R (left-step count left) (right-step count right))
  (count : ℕ)
  → (fun count₁ => R (data/Nat.rec (fun x₃ => C) left-initial left-step count₁) (data/Nat.rec (fun x₆ => C) right-initial right-step count₁)) count

bellman/nnrat-value-iterate-congruent.{u} :
  (A : Type u) (source : Finset A) (transition equivalent-transition : A → A → ℚ≥0)
  (reward equivalent-reward : A → ℚ≥0) (discount equivalent-discount : ℚ≥0)
  (initial equivalent-initial : A → ℚ≥0)
  (same-transition : ∀ (state : A), ∀ (next : A), transition state next = equivalent-transition state next)
  (same-reward : ∀ (state : A), reward state = equivalent-reward state)
  (same-discount : discount = equivalent-discount)
  (same-initial : ∀ (state : A), initial state = equivalent-initial state)
  (steps : ℕ) (state : A)
  → data/Nat.rec (fun x₈ => A → ℚ≥0) initial (fun x₉ => fun previous-value => fun state₁ => policy₁ previous-value state₁) steps state = data/Nat.rec (fun x₁₇ => A → ℚ≥0) equivalent-initial (fun x₁₈ => fun previous-value => fun state₁ => policy previous-value state₁) steps state
  where policy := bellman/nnrat-fixed-policy A source equivalent-transition equivalent-reward equivalent-discount
  where policy₁ := bellman/nnrat-fixed-policy A source transition reward discount

bellman/nnrat-value-iterate-model-transfer.{u} :
  (A : Type u) (source : Finset A) (transition equivalent-transition : A → A → ℚ≥0)
  (reward equivalent-reward : A → ℚ≥0) (discount equivalent-discount : ℚ≥0)
  (initial : A → ℚ≥0)
  (same-transition : ∀ (state : A), ∀ (next : A), transition state next = equivalent-transition state next)
  (same-reward : ∀ (state : A), reward state = equivalent-reward state)
  (same-discount : discount = equivalent-discount)
  (steps : ℕ) (state : A)
  → data/Nat.rec (fun x₈ => A → ℚ≥0) initial (fun x₉ => fun previous-value => fun state₁ => policy₁ previous-value state₁) steps state = data/Nat.rec (fun x₁₇ => A → ℚ≥0) initial (fun x₁₈ => fun previous-value => fun state₁ => policy previous-value state₁) steps state
  where policy := bellman/nnrat-fixed-policy A source equivalent-transition equivalent-reward equivalent-discount
  where policy₁ := bellman/nnrat-fixed-policy A source transition reward discount

bellman/nnrat-value-iterate-initial-transfer.{u} :
  (A : Type u) (source : Finset A) (transition : A → A → ℚ≥0) (reward : A → ℚ≥0)
  (discount : ℚ≥0) (initial equivalent-initial : A → ℚ≥0)
  (same-initial : ∀ (state : A), initial state = equivalent-initial state)
  (steps : ℕ) (state : A)
  → data/Nat.rec (fun x₈ => A → ℚ≥0) initial (fun x₉ => fun previous-value => fun state₁ => policy previous-value state₁) steps state = data/Nat.rec (fun x₁₇ => A → ℚ≥0) equivalent-initial (fun x₁₈ => fun previous-value => fun state₁ => policy previous-value state₁) steps state
  where policy := bellman/nnrat-fixed-policy A source transition reward discount