Reference · Algorithm guarantees

rainbow.algorithms.proofs.tournament-selection

Algorithm guaranteessrc/rainbow/algorithms/proofs/tournament_selection.clj2 definitions, 3 theorems

AHoF O43 Genetic Algorithm -- tournament selection operator: from a sampled tournament of candidate fitnesses the fittest (maximum) entrant is selected to reproduce. Selection is the max-fold of the tournament's fitnesses: winner fitnesses = fold nnrat-max 0 fitnesses where the pairwise nnrat-max keeps the larger of two fitnesses using the decidable rational order. Proved: worked instances -- max 2 7 = 7, the tournament [3,7,2] selects 7, and the worked certificate 3 <= winner [3,7,2] (a native nnrat/at-most). The stochastic sampling of which candidates enter a tournament is an executable concern; what is proved here is the max-fold selection at these instances. That the winner dominates every entrant for all tournaments, and the selection pressure it gives the GA, are not proved here. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and logic/if-data (all carried by the D63 checkpoint, as used by nearest_neighbor and the geometric-convergence bounds). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.tournament-selection` prints this classification.

tournament/nnrat-max :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

tournament/winner :
  (x₁ : List ℚ≥0)
  → ℚ≥0

tournament/max-keeps-larger :
  → tournament/nnrat-max 2 7 = 7

tournament/winner-example :
  → tournament/winner [3, 7, 2] = 7

tournament/winner-dominates-entrant :
  → 3 ≤ tournament/winner [3, 7, 2]