Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.multiobjective

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/multiobjective.clj4 definitions, 7 theorems

Kochenderfer 'Algorithms for Optimization' Ch.15-16 multiobjective / sampling-plan selection rules as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: O15.3 non-dominated sorting : a Pareto-dominates b iff a1>=b1 AND a2>=b2 O15.4 VEGA : per-objective subpopulation selection = max fitness O16.8 greedy subset select : pick the point of minimum distance metric O16.9 exchange subset select: accept a swap only when it reduces the metric Pareto dominance is a boolean-AND of two decidable >= tests; its soundness (dominates=true entails both objective inequalities) reuses rainbow.math.logic.boolean-and exactly as interval-membership-soundness does. Selection reuses nnrat-minmax. Native and axiom-free; chains boolean-and and nnrat-minmax on d63.

Depends onmath.logic.boolean-andmath.rational.nnrat.minmax

mo/dominates :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → data/Bool

mo/vega-select :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

mo/greedy-nearest :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

mo/exchange-step :
  (x₁ : data/Bool) (x₂ x₃ : ℚ≥0)
  → ℚ≥0

mo/dominates-sound :
  (a1 a2 b1 b2 : ℚ≥0)
  (h : mo/dominates a1 a2 b1 b2 = data/true)
  → proposition/conjunction (b1 ≤ a1) (b2 ≤ a2)

mo/vega-keeps-fittest-left :
  (fa fb : ℚ≥0)
  → fa ≤ mo/vega-select fa fb

mo/vega-keeps-fittest-right :
  (fa fb : ℚ≥0)
  → fb ≤ mo/vega-select fa fb

mo/greedy-nearest-below-left :
  (d0 d1 : ℚ≥0)
  → opt/ldp-min-norm d0 d1 ≤ d0

mo/greedy-nearest-below-right :
  (d0 d1 : ℚ≥0)
  → opt/ldp-min-norm d0 d1 ≤ d1

mo/exchange-accepts :
  (candidate current : ℚ≥0)
  → mo/exchange-step data/true candidate current = candidate

mo/exchange-rejects :
  (candidate current : ℚ≥0)
  → mo/exchange-step data/false candidate current = current