Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.policy-evaluation

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/policy_evaluation.clj2 definitions, 5 theorems

AHoF D20 specialization of bounded exact-rational policy evaluation. Scope (measured by the kernel): this module has 5 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.policy-evaluation` prints this classification.

ahof-d20/evaluate :
  (x₁ x₂ : ℕ)
  → ℚ≥0

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

ahof-d20/finite-horizon-recurrence :
  → proposition/conjunction (∀ (state : ℕ), data/Nat.rec (fun x₂₄ => ℕ → ℚ≥0) ahof-d22/initial-value (fun x₂₅ => fun previous-value => fun state₁ => policy previous-value state₁) 0 state = ahof-d22/initial-value state) (∀ (steps : ℕ), data/Nat.rec (fun x₂₉ => ℕ → ℚ≥0) ahof-d22/initial-value (fun x₃₀ => fun previous-value => fun state => policy previous-value state) (data/succ steps) = (fun x₃₁ => fun previous-value => fun state => policy previous-value state) steps (data/Nat.rec (fun x₃₅ => ℕ → ℚ≥0) ahof-d22/initial-value (fun x₃₆ => fun previous-value => fun state => policy previous-value state) steps))
  where policy := bellman/nnrat-fixed-policy ℕ ahof-d2/grid or-example/nnrat-deterministic-transition or-example/nnrat-identity-reward nnrat/half

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

ahof-d20/one-step-value :
  → proposition/conjunction (data/Nat.rec (fun x₂₆ => ℕ → ℚ≥0) ahof-d22/initial-value (fun x₂₇ => fun previous-value => fun state => policy previous-value state) 1 0 = 0) (data/Nat.rec (fun x₃₅ => ℕ → ℚ≥0) ahof-d22/initial-value (fun x₃₆ => fun previous-value => fun state => policy previous-value state) 1 1 = 1)
  where policy := bellman/nnrat-fixed-policy ℕ ahof-d2/grid or-example/nnrat-deterministic-transition or-example/nnrat-identity-reward nnrat/half

ahof-d20/two-step-value :
  → proposition/conjunction (or-example/nnrat-identity-reward 0 + nnrat/half · expectation = 0) (or-example/nnrat-identity-reward 1 + nnrat/half · expectation₁ = 3/2)
  where expectation := probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 0) or-example/nnrat-step-one-value
  where expectation₁ := probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 1) or-example/nnrat-step-one-value

ahof-d20/policy-evaluation :
  → proposition/conjunction (conjunction) (proposition/conjunction (proposition/conjunction (∀ (state : ℕ), data/Nat.rec (fun x₂₄₀ => ℕ → ℚ≥0) ahof-d22/initial-value (fun x₂₄₁ => fun previous-value => fun state₁ => policy previous-value state₁) 0 state = ahof-d22/initial-value state) (∀ (steps : ℕ), data/Nat.rec (fun x₂₄₅ => ℕ → ℚ≥0) ahof-d22/initial-value (fun x₂₄₆ => fun previous-value => fun state => policy previous-value state) (data/succ steps) = (fun x₂₄₇ => fun previous-value => fun state => policy previous-value state) steps (data/Nat.rec (fun x₂₅₁ => ℕ → ℚ≥0) ahof-d22/initial-value (fun x₂₅₂ => fun previous-value => fun state => policy previous-value state) steps))) (proposition/conjunction (data/Nat.rec (fun x₂₇₈ => ℕ → ℚ≥0) ahof-d22/initial-value (fun x₂₇₉ => fun previous-value => fun state => policy previous-value state) 1 0 = 0) (data/Nat.rec (fun x₂₈₇ => ℕ → ℚ≥0) ahof-d22/initial-value (fun x₂₈₈ => fun previous-value => fun state => policy previous-value state) 1 1 = 1)))
  where conjunction := proposition/conjunction (list/nnrat-map-sum ℕ (or-example/nnrat-deterministic-transition 0) (finset-data/enumeration ℕ ahof-d2/grid) = 1) (list/nnrat-map-sum ℕ (or-example/nnrat-deterministic-transition 1) (finset-data/enumeration ℕ ahof-d2/grid) = 1)
  where policy := bellman/nnrat-fixed-policy ℕ ahof-d2/grid or-example/nnrat-deterministic-transition or-example/nnrat-identity-reward nnrat/half