Reference · Algorithm guarantees

rainbow.algorithms.proofs.particle-swarm-best-iterate

Algorithm guaranteessrc/rainbow/algorithms/proofs/particle_swarm_best_iterate.clj1 definitions, 6 theorems

Finite-horizon best-so-far recurrence and objective monotonicity.

Depends onalgorithms.proofs.particle-swarm-global-best

swarm/nnrat-best-iterate :
  (x₁ : List ℚ → ℚ≥0) (x₂ : ℕ → List ℚ → List ℚ) (x₃ : List ℚ) (x₄ : ℕ)
  → List ℚ

swarm/nnrat-best-iterate-zero :
  (objective : List ℚ → ℚ≥0) (proposal : ℕ → List ℚ → List ℚ) (initial : List ℚ)
  → swarm/nnrat-best-iterate objective proposal initial 0 = initial

swarm/nnrat-best-iterate-successor :
  (objective : List ℚ → ℚ≥0) (proposal : ℕ → List ℚ → List ℚ) (initial : List ℚ)
  (steps : ℕ)
  → swarm/nnrat-best-iterate objective proposal initial (data/succ steps) = swarm/nnrat-best-so-far objective (iterate) (proposal steps (iterate))
  where iterate := swarm/nnrat-best-iterate objective proposal initial steps

swarm/nnrat-best-iterate-successor-is-previous-or-proposal :
  (objective : List ℚ → ℚ≥0) (proposal : ℕ → List ℚ → List ℚ) (initial : List ℚ)
  (steps : ℕ)
  → proposition/disjunction (iterate = iterate₁) (iterate = proposal steps (iterate₁))
  where iterate := swarm/nnrat-best-iterate objective proposal initial (data/succ steps)
  where iterate₁ := swarm/nnrat-best-iterate objective proposal initial steps

swarm/nnrat-best-iterate-successor-bounds-previous :
  (objective : List ℚ → ℚ≥0) (proposal : ℕ → List ℚ → List ℚ) (initial : List ℚ)
  (steps : ℕ)
  → objective (iterate (data/succ steps)) ≤ objective (iterate steps)
  where iterate := swarm/nnrat-best-iterate objective proposal initial

swarm/nnrat-best-iterate-successor-bounds-proposal :
  (objective : List ℚ → ℚ≥0) (proposal : ℕ → List ℚ → List ℚ) (initial : List ℚ)
  (steps : ℕ)
  → objective (iterate (data/succ steps)) ≤ objective (proposal steps (iterate steps))
  where iterate := swarm/nnrat-best-iterate objective proposal initial

swarm/nnrat-best-iterate-bounds-initial :
  (objective : List ℚ → ℚ≥0) (proposal : ℕ → List ℚ → List ℚ) (initial : List ℚ)
  (steps : ℕ)
  → (fun steps₁ => objective (swarm/nnrat-best-iterate objective proposal initial steps₁) ≤ objective initial) steps