Reference · Algorithm guarantees

rainbow.algorithms.proofs.particle-swarm

Algorithm guaranteessrc/rainbow/algorithms/proofs/particle_swarm.clj3 definitions, 5 theorems

AHoF O45 Particle Swarm Optimization: the per-particle velocity and position update over genuinely n-dimensional vector state. Each particle carries a position and a velocity vector; the velocity is pulled by inertia toward its own momentum, cognitively toward its personal best, and socially toward the swarm's global best: v' = w*v + c1*(pbest - x) + c2*(gbest - x) x' = x + v' Every term is an operation from the finite-vector capability (scale, subtract, add), so this is the first optimizer whose state is a true vector rather than a scalar or a fixed-arity pair. The coefficients are general nonnegative rationals; the stochastic weights of the textbook algorithm are supplied as concrete rationals in the worked instance, so what is proved here is the deterministic update recurrence and a worked two-dimensional step, not the stochastic convergence (which stays an executable-only concern). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values) and 2 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.particle-swarm` prints this classification.

Depends onmath.finite.vector

swarm/velocity-update :
  (x₁ x₂ x₃ : ℚ≥0) (x₄ x₅ x₆ x₇ : List ℚ)
  → List ℚ

swarm/position-update :
  (x₁ x₂ : List ℚ)
  → List ℚ

swarm/step :
  (x₁ x₂ x₃ : ℚ≥0) (x₄ x₅ x₆ x₇ : List ℚ)
  → List ℚ

swarm/position-update-unfold :
  (position velocity : List ℚ)
  → noisy/wrap position velocity = vector/add position velocity

swarm/step-unfold :
  (w c1 c2 : ℚ≥0) (velocity position pbest gbest : List ℚ)
  → swarm/step w c1 c2 velocity position pbest gbest = noisy/wrap position (update)
  where update := swarm/velocity-update w c1 c2 velocity position pbest gbest

swarm/velocity-update-example :
  → swarm/velocity-update 1 1 1 [signed/from-nnrat 1, signed/from-nnrat 0] [signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 2, signed/from-nnrat 0] [signed/from-nnrat 0, signed/from-nnrat 2] = [signed/from-nnrat 3, signed/from-nnrat 2]

swarm/position-update-example :
  → noisy/wrap [signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 3, signed/from-nnrat 2] = [signed/from-nnrat 3, signed/from-nnrat 2]

swarm/step-example :
  → swarm/step 1 1 1 [signed/from-nnrat 1, signed/from-nnrat 0] [signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 2, signed/from-nnrat 0] [signed/from-nnrat 0, signed/from-nnrat 2] = [signed/from-nnrat 3, signed/from-nnrat 2]