Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.robustness-objective

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

AHoF V13 worked robustness-based falsification objective over signed rationals. A satisfying trajectory has robustness 2 (positive); its falsification objective is -2 (negative). A violating trajectory has robustness -1 (negative); its objective is 1 (positive). So maximizing the objective favours the violating trajectory -- the falsification framing. The values are proved by signed cross-product equivalence. 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.robustness-objective` prints this classification.

ahof-v13/satisfying-robustness :
  → ℚ

ahof-v13/violating-robustness :
  → ℚ

ahof-v13/satisfying-objective-is-negative-two :
  → validation/falsification-objective ahof-o31/initial = signed/make 0 2

ahof-v13/violating-objective-is-one :
  → validation/falsification-objective ahof-v13/violating-robustness = signed/from-nnrat 1

ahof-v13/robustness-objective :
  → proposition/conjunction (validation/falsification-objective ahof-o31/initial = signed/make 0 2) (validation/falsification-objective ahof-v13/violating-robustness = signed/from-nnrat 1)