Reference · Algorithm guarantees

rainbow.algorithms.proofs.cuckoo-search

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

AHoF O47 Cuckoo Search: the Levy-flight step over vector-valued state. A cuckoo lays an egg (a new candidate solution) by taking a scaled step from its current position in a random Levy-flight direction: position' = position + rate * direction a finite-vector scale and add. The heavy-tailed Levy direction and the nest abandonment / replacement (keep the better of the new and a random nest) are the sampler's and selector's concern (executable); the rate is a concrete nonnegative rational in the worked instance, so what is proved is the deterministic flight recurrence and worked instances. Requires the finite-vector capability. 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.cuckoo-search` prints this classification.

Depends onmath.finite.vector

cuckoo/levy-step :
  (x₁ : List ℚ) (x₂ : ℚ≥0) (x₃ : List ℚ)
  → List ℚ

cuckoo/levy-step-unfold :
  (position : List ℚ) (rate : ℚ≥0) (direction : List ℚ)
  → cuckoo/levy-step position rate direction = vector/add position (vector/scale rate direction)

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

cuckoo/scaled-flight-example :
  → cuckoo/levy-step [signed/from-nnrat 0, signed/from-nnrat 0] 2 [signed/from-nnrat 1, signed/from-nnrat 2] = [signed/from-nnrat 2, signed/from-nnrat 4]