Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.failure-probability-monitor

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

AHoF V64 worked failure-probability monitor over exact rationals with risk threshold 1/2. A failure-probability estimate of 1/4 stays at or below the threshold, so the system is safe and no alarm is raised. An estimate of 3/4 exceeds the threshold, so the system is unsafe and the alarm trips. Proved native and axiom-free. Scope (measured by the kernel): this module has 5 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.failure-probability-monitor` prints this classification.

Depends onalgorithms.proofs.failure-probability-monitor

ahof-v64/threshold :
  → ℚ≥0

ahof-v64/low-is-safe :
  → ce-is/elite? 1/4 ahof-d63/rate = data/true

ahof-v64/low-no-alarm :
  → failmon/alarm? 1/4 ahof-d63/rate = data/false

ahof-v64/high-is-unsafe :
  → ce-is/elite? 3/4 ahof-d63/rate = data/false

ahof-v64/high-alarms :
  → failmon/alarm? 3/4 ahof-d63/rate = data/true

ahof-v64/failure-monitor :
  → proposition/conjunction (failmon/alarm? 1/4 ahof-d63/rate = data/false) (failmon/alarm? 3/4 ahof-d63/rate = data/true)