Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.prob-robust

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

AHoF O75 Probabilistic Robust Optimization: satisfy constraints with high probability under uncertainty; a design is chance-feasible when its violation probability is within the risk level alpha: chance-feasible? violation-probability alpha = decide (violation-probability <= alpha). Proved native and axiom-free (decision, two positive instances, at-most certificate, negative instance). Requires audit/decide-nnrat-at-most, nnrat/at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 4 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.prob-robust` prints this classification.

prob-robust/chance-feasible? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

prob-robust/low-risk-feasible :
  → lis/extends? 1/4 1/2 = data/true

prob-robust/boundary-feasible :
  → lis/extends? 1/2 1/2 = data/true

prob-robust/chance-certificate :
  → 1/4 ≤ 1/2

prob-robust/high-risk-infeasible :
  → lis/extends? 3/4 1/2 = data/false