Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.value-iteration

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/value_iteration.clj11 definitions, 7 theorems

AHoF D22 worked finite exact-rational value-iteration instance.

ahof-d22/state-space :
  → Finset ℕ

ahof-d22/action-space :
  → Finset ℕ

ahof-d22/fallback-action :
  (x₁ : ℕ)
  → ℕ

ahof-d22/transition :
  (x₁ x₂ x₃ : ℕ)
  → ℚ≥0

ahof-d22/reward :
  (x₁ x₂ : ℕ)
  → ℚ≥0

ahof-d22/initial-value :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d22/action-backup :
  (x₁ : ℕ → ℚ≥0) (x₂ x₃ : ℕ)
  → ℚ≥0

ahof-d22/optimality-step :
  (x₁ : ℕ → ℚ≥0) (x₂ : ℕ)
  → ℚ≥0

ahof-d22/value-sequence :
  (x₁ x₂ : ℕ)
  → ℚ≥0

ahof-d22/one-step-value :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d22/two-step-value-function :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d22/fallback-action-admissible :
  (state : ℕ)
  → ahof-d21/current-policy state ∈ ahof-d22/action-space

ahof-d22/action-backup-correspondence :
  (value : ℕ → ℚ≥0) (state action : ℕ)
  → bellman/nnrat-action-backup ℕ ℕ ahof-d2/grid ahof-d22/transition ahof-d22/reward 0 value state action = ahof-d22/action-backup value state action

ahof-d22/normalized-transition-rows :
  (state : ℕ)
  → proposition/conjunction (sum = 1) (sum₁ = 1)
  where sum := list/nnrat-map-sum ℕ (ahof-d22/transition state 0) (finset-data/enumeration ℕ ahof-d2/grid)
  where sum₁ := list/nnrat-map-sum ℕ (ahof-d22/transition state 1) (finset-data/enumeration ℕ ahof-d2/grid)

ahof-d22/finite-horizon-recurrence :
  → proposition/conjunction (∀ (state : ℕ), iterate state = ahof-d22/initial-value state) (∀ (steps : ℕ), value/nnrat-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup (data/succ steps) ahof-d22/initial-value = (fun x₂ => fun previous => fun state => step previous state) steps (value/nnrat-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup steps ahof-d22/initial-value))
  where iterate := value/nnrat-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup 0 ahof-d22/initial-value
  where step := value/nnrat-optimality-step ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup

ahof-d22/greedy-actions :
  → proposition/conjunction (∀ (state : ℕ), action state ∈ ahof-d22/action-space) (∀ (state : ℕ), ∀ (candidate : ℕ), ∀ (candidate-member : candidate ∈ ahof-d22/action-space), ahof-d22/action-backup ahof-d22/one-step-value state candidate ≤ step state)
  where action := value/nnrat-greedy-action ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup ahof-d22/one-step-value
  where step := value/nnrat-optimality-step ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup ahof-d22/one-step-value

ahof-d22/two-step-value :
  → proposition/conjunction (ahof-d22/two-step-value-function 0 = 0) (ahof-d22/two-step-value-function 1 = 0)

ahof-d22/value-iteration :
  → proposition/conjunction (∀ (state : ℕ), proposition/conjunction (list/nnrat-map-sum ℕ (ahof-d22/transition state 0) (finset-data/enumeration ℕ ahof-d2/grid) = 1) (list/nnrat-map-sum ℕ (ahof-d22/transition state 1) (finset-data/enumeration ℕ ahof-d2/grid) = 1)) (proposition/conjunction (proposition/conjunction (∀ (state : ℕ), iterate state = ahof-d22/initial-value state) (∀ (steps : ℕ), value/nnrat-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup (data/succ steps) ahof-d22/initial-value = (fun x₈ => fun previous => fun state => value/nnrat-optimality-step ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup previous state) steps (value/nnrat-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup steps ahof-d22/initial-value))) (conjunction))
  where conjunction := proposition/conjunction (proposition/conjunction (∀ (state : ℕ), value/nnrat-greedy-action ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup ahof-d22/one-step-value state ∈ ahof-d22/action-space) (∀ (state : ℕ), ∀ (candidate : ℕ), ∀ (candidate-member : candidate ∈ ahof-d22/action-space), ahof-d22/action-backup ahof-d22/one-step-value state candidate ≤ value/nnrat-optimality-step ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup ahof-d22/one-step-value state)) (proposition/conjunction (ahof-d22/two-step-value-function 0 = 0) (ahof-d22/two-step-value-function 1 = 0))
  where iterate := value/nnrat-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup 0 ahof-d22/initial-value