Reference · Algorithm guarantees

rainbow.algorithms.proofs.differential-evolution

Algorithm guaranteessrc/rainbow/algorithms/proofs/differential_evolution.clj2 definitions, 4 theorems

AHoF O44 Differential Evolution: the differential mutation over vector-valued population members. The DE/rand/1 mutation perturbs a base vector by a scaled difference of two other population vectors: donor = F * (b - c) mutant = base + donor Every term is an operation from the finite-vector capability (subtract, scale, add), so this reuses the n-dimensional vector state introduced for particle swarm. The scale factor is a general nonnegative rational; the population's stochastic index draws of the textbook algorithm are supplied as concrete population vectors in the worked instance, so what is proved is the deterministic mutation recurrence and a worked two-dimensional instance, not the stochastic population dynamics (which stay an executable-only concern). Scope (measured by the kernel): this module has 3 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.differential-evolution` prints this classification.

Depends onmath.finite.vector

evolution/scaled-difference :
  (x₁ : ℚ≥0) (x₂ x₃ : List ℚ)
  → List ℚ

evolution/differential-mutation :
  (x₁ : List ℚ) (x₂ : ℚ≥0) (x₃ x₄ : List ℚ)
  → List ℚ

evolution/mutation-unfold :
  (base : List ℚ) (f : ℚ≥0) (b c : List ℚ)
  → evolution/differential-mutation base f b c = vector/add base (evolution/scaled-difference f b c)

evolution/scaled-difference-example :
  → evolution/scaled-difference 2 [signed/from-nnrat 1, signed/from-nnrat 2] [signed/from-nnrat 0, signed/from-nnrat 0] = [signed/from-nnrat 2, signed/from-nnrat 4]

evolution/mutation-example :
  → evolution/differential-mutation [signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 3, signed/from-nnrat 2] [signed/from-nnrat 0, signed/from-nnrat 0] = [signed/from-nnrat 3, signed/from-nnrat 2]

evolution/unit-mutation-example :
  → evolution/differential-mutation [signed/from-nnrat 1, signed/from-nnrat 1] 1 [signed/from-nnrat 2, signed/from-nnrat 3] [signed/from-nnrat 0, signed/from-nnrat 0] = [signed/from-nnrat 3, signed/from-nnrat 4]