Reference · Algorithm guarantees

rainbow.algorithms.proofs.firefly

Algorithm guaranteessrc/rainbow/algorithms/proofs/firefly.clj1 definitions, 3 theorems

AHoF O46 Firefly Algorithm: the attraction move over vector-valued state. A dimmer firefly moves toward a brighter one by a fraction of their separation: x' = x + beta * (bright - x) Every term is a finite-vector operation (subtract, scale, add), reusing the n-dimensional vector state introduced for the population methods. The textbook attractiveness beta = beta0 * exp(-gamma r^2) is distance-dependent and not exact-rational; the worked instance supplies beta as a concrete nonnegative rational, so what is proved is the deterministic attraction recurrence and a worked two-dimensional move, not the distance-weighted stochastic dynamics (which stay an executable-only concern). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 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.firefly` prints this classification.

Depends onmath.finite.vector

firefly/attraction-step :
  (x₁ x₂ : List ℚ) (x₃ : ℚ≥0)
  → List ℚ

firefly/attraction-unfold :
  (position bright : List ℚ) (beta : ℚ≥0)
  → firefly/attraction-step position bright beta = vector/add position (scale)
  where scale := vector/scale beta (vector/subtract bright position)

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

firefly/full-attraction-3d-example :
  → firefly/attraction-step [signed/from-nnrat 0, signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6] 1 = [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6]