Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.async-value-iteration

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/async_value_iteration.clj4 definitions, 8 theorems

AHoF D23 worked asynchronous (Gauss-Seidel) value-iteration instance. Reuses the D22 worked finite MDP (two states, one action, zero reward, zero discount) so kernel normalization stays tractable, and adds a concrete single-state update schedule that always selects state 0 and preserves state 1. This exhibits the pluggable state-selection strategy: the selected-state update law and the non-selected-state preservation law both hold at the worked model, the schedule-prefix recurrence unfolds, and a bounded asynchronous execution is exact.

ahof-d23/schedule :
  (x₁ x₂ : ℕ)
  → data/Bool

ahof-d23/async-sequence :
  (x₁ x₂ : ℕ)
  → ℚ≥0

ahof-d23/one-step-async :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d23/two-step-async :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d23/schedule-selects-zero :
  (step : ℕ)
  → ahof-d23/schedule step 0 = data/true

ahof-d23/schedule-skips-one :
  (step : ℕ)
  → ahof-d23/schedule step 1 = data/false

ahof-d23/selected-update :
  (step : ℕ) (value : ℕ → ℚ≥0)
  → value/nnrat-async-update ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup (ahof-d23/schedule step) value 0 = value/nnrat-optimality-step ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup value 0

ahof-d23/preserved-update :
  (step : ℕ) (value : ℕ → ℚ≥0)
  → value/nnrat-async-update ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup (ahof-d23/schedule step) value 1 = value 1

ahof-d23/async-recurrence :
  → proposition/conjunction (∀ (state : ℕ), iterate state = ahof-d22/initial-value state) (∀ (steps : ℕ), value/nnrat-async-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup ahof-d23/schedule (data/succ steps) ahof-d22/initial-value = (fun step-index => fun previous => update (ahof-d23/schedule step-index) previous) steps (value/nnrat-async-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup ahof-d23/schedule steps ahof-d22/initial-value))
  where iterate := value/nnrat-async-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup ahof-d23/schedule 0 ahof-d22/initial-value
  where update := value/nnrat-async-update ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup

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

ahof-d23/two-step-async-values :
  → proposition/conjunction (ahof-d23/two-step-async 0 = 0) (ahof-d23/two-step-async 1 = 0)

ahof-d23/async-value-iteration :
  → proposition/conjunction (∀ (step : ℕ), ∀ (value : ℕ → ℚ≥0), value/nnrat-async-update ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup (ahof-d23/schedule step) value 0 = step value 0) (conjunction)
  where conjunction := proposition/conjunction (∀ (step : ℕ), ∀ (value : ℕ → ℚ≥0), value/nnrat-async-update ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup (ahof-d23/schedule step) value 1 = value 1) (proposition/conjunction (proposition/conjunction (∀ (state : ℕ), value/nnrat-async-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup ahof-d23/schedule 0 ahof-d22/initial-value state = ahof-d22/initial-value state) (∀ (steps : ℕ), value/nnrat-async-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup ahof-d23/schedule (data/succ steps) ahof-d22/initial-value = (fun step-index => fun previous => value/nnrat-async-update ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup (ahof-d23/schedule step-index) previous) steps (value/nnrat-async-iterate ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup ahof-d23/schedule steps ahof-d22/initial-value))) (proposition/conjunction (ahof-d23/two-step-async 0 = 0) (ahof-d23/two-step-async 1 = 0)))
  where step := value/nnrat-optimality-step ℕ ℕ ahof-d22/action-space ahof-d21/current-policy ahof-d22/action-backup