Skip to content
Rainbow docs menu

Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.isotropic-es

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/isotropic_es.clj2 definitions, 3 theorems

AHoF D44 Isotropic Evolutionary Strategies: perturb with isotropic Gaussian noise and keep the fitter offspring; between two fitnesses it keeps the larger value: prefers-fitter? a b = decide ('b 'a) selected-fitness a b = if ('b 'a) then 'a else 'b over exact rationals. Proved native and axiom-free: the preference decision, the selected value, and the switch. Requires audit/decide-nnrat-at-most, logic/if-data (both in the D63 checkpoint). 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.ahof.isotropic-es` prints this classification.

iso-es/prefers-fitter?

DefinitionSource, line 40

iso-es/prefers-fitter? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

ℚ≥0 = nnrat/NonnegativeRational

iso-es/selected-fitness

DefinitionSource, line 45

iso-es/selected-fitness :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

iso-es/prefers-example

TheoremWorked exampleNo axiomsSource, line 54

iso-es/prefers-example :
  → bo/is-safe 3/4 1/2 = data/true

= = equality/Eq

iso-es/selected-value

TheoremWorked exampleNo axiomsSource, line 60

iso-es/selected-value :
  → fsc/node-value 3/4 1/2 = 3/4

= = equality/Eq

iso-es/switches

TheoremWorked exampleNo axiomsSource, line 66

iso-es/switches :
  → bo/is-safe 1/2 3/4 = data/false

= = equality/Eq