Reference · The Applied Higher-Order Functions catalogue
rainbow.algorithms.proofs.ahof.isotropic-es
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?
iso-es/prefers-fitter? : (x₁ x₂ : ℚ≥0) → data/Bool
ℚ≥0 = nnrat/NonnegativeRational
iso-es/selected-fitness
iso-es/selected-fitness : (x₁ x₂ : ℚ≥0) → ℚ≥0
ℚ≥0 = nnrat/NonnegativeRational
iso-es/prefers-example
iso-es/prefers-example : → bo/is-safe 3/4 1/2 = data/true
= = equality/Eq
iso-es/selected-value
iso-es/selected-value : → fsc/node-value 3/4 1/2 = 3/4
= = equality/Eq
iso-es/switches
iso-es/switches : → bo/is-safe 1/2 3/4 = data/false
= = equality/Eq