Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.policy-iteration

The Applied Higher-Order Functions catalogue src/rainbow/algorithms/proofs/ahof/policy_iteration.clj7 definitions, 4 theorems

AHoF D21 worked bounded policy-iteration step.

ahof-d21/state-space

DefinitionSource, line 41

ahof-d21/state-space :
  → Finset ℕ

Finset = finset-data/Finsetℕ = data/Nat

ahof-d21/action-space

DefinitionSource, line 46

ahof-d21/action-space :
  → Finset ℕ

Finset = finset-data/Finsetℕ = data/Nat

ahof-d21/current-policy

DefinitionSource, line 51

ahof-d21/current-policy :
  (x₁ : ℕ)
  → ℕ

ℕ = data/Nat

ahof-d21/evaluate-policy

DefinitionSource, line 55

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

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

ahof-d21/action-score

DefinitionSource, line 63

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

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

ahof-d21/improved-policy

DefinitionSource, line 77

ahof-d21/improved-policy :
  (x₁ : ℕ)
  → ℕ

ℕ = data/Nat

ahof-d21/iteration-step

DefinitionSource, line 88

ahof-d21/iteration-step :
  (x₁ : ℕ)
  → ℕ

ℕ = data/Nat

ahof-d21/current-policy-admissible

TheoremFor all inputsNo axiomsSource, line 105

ahof-d21/current-policy-admissible :
  (state : ℕ)
  → ahof-d21/current-policy state ∈ ahof-d2/grid

ℕ = data/Nat∈ = finset-data/to-set: membership in a finite set

ahof-d21/evaluation-phase

TheoremWorked exampleNo axiomsSource, line 139

ahof-d21/evaluation-phase :
  → ahof-d21/evaluate-policy ahof-d21/current-policy = ahof-d21/evaluate-policy ahof-d21/current-policy

= = equality/Eq

ahof-d21/improvement-phase

TheoremWorked exampleNo axiomsSource, line 168

ahof-d21/improvement-phase :
  → proposition/conjunction (∀ (state : ℕ), improve state ∈ ahof-d2/grid) (∀ (state : ℕ), ∀ (candidate : ℕ), ∀ (candidate-member : candidate ∈ ahof-d2/grid), ahof-d21/action-score (ahof-d21/evaluate-policy ahof-d21/current-policy) state candidate ≤ ahof-d21/action-score (ahof-d21/evaluate-policy ahof-d21/current-policy) state (improve state))
  where improve := policy/nnrat-improve ℕ ℕ ahof-d2/grid ahof-d21/current-policy (ahof-d21/action-score (ahof-d21/evaluate-policy ahof-d21/current-policy))

ℕ = data/Nat∈ = finset-data/to-set: membership in a finite set≤ = nnrat/at-most

ahof-d21/policy-iteration-step

TheoremFor all inputsNo axiomsSource, line 203

ahof-d21/policy-iteration-step :
  (state : ℕ)
  → policy/nnrat-iteration-step ℕ ℕ ahof-d2/grid ahof-d21/current-policy ahof-d21/evaluate-policy ahof-d21/action-score state = policy/nnrat-improve ℕ ℕ ahof-d2/grid ahof-d21/current-policy (ahof-d21/action-score (ahof-d21/evaluate-policy ahof-d21/current-policy)) state

= = equality/Eqℕ = data/Nat