Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.robust-optimization

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

AHoF O74 Robust Optimization (set-based): optimize against the WORST case over an uncertainty set. With two scenario costs the worst case is their maximum, and a design is robustly acceptable when that worst case stays within the budget: worst-case c1 c2 = if (c1 <= c2) then c2 else c1 (maximum) robust-ok? worst budget = decide (worst <= budget) over exact rationals. Proved native and axiom-free: the worst-case (max) selection in both orders, and the robust-acceptance threshold decision. 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.robust-optimization` prints this classification.

robust-opt/worst-case :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

robust-opt/robust-ok? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

robust-opt/worst-case-is-larger :
  → knapsack/cell 1/2 3/4 = 3/4

robust-opt/worst-case-symmetric :
  → knapsack/cell 3/4 1/2 = 3/4

robust-opt/within-budget :
  → lis/extends? 3/4 1 = data/true