Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.weighted-sum

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/weighted_sum.clj3 definitions, 4 theorems

AHoF O66 Weighted Sum Method (multi-objective scalarization): collapse several objectives into one scalar by a weighted sum, then optimize the scalar: scalarize w1 f1 w2 f2 = w1 * f1 + w2 * f2. With balanced weights 1/2, 1/2 on objectives 1/2, 3/4 the scalarized value is 5/8; with weight only on the first objective (weights 1, 0) it is the first objective 1/2, so the weights genuinely steer the aggregate. Values are proved by cross- product equivalence. Proved native and axiom-free. 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.ahof.weighted-sum` prints this classification.

weighted-sum/scalarize :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

weighted-sum/balanced :
  → ℚ≥0

weighted-sum/objective-one-only :
  → ℚ≥0

weighted-sum/scalarize-unfold :
  (w1 f1 w2 f2 : ℚ≥0)
  → qmdp/value w1 f1 w2 f2 = w1 · f1 + w2 · f2

weighted-sum/balanced-is-five-eighths :
  → smc/balanced = 5/8

weighted-sum/objective-one-is-half :
  → smc/single = 1/2

weighted-sum/weighted-sum :
  → proposition/conjunction (smc/balanced = 5/8) (smc/single = 1/2)