Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.rejection-sampling

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

AHoF V21 Rejection Sampling (for failure events): draw samples and keep only those consistent with the evidence / that hit the target event, rejecting the rest. A sample is accepted when its statistic is within the evidence tolerance: accepts? statistic tolerance = decide (statistic <= tolerance) over the decidable rational order. Proved native and axiom-free: the acceptance test and worked instances on concrete values -- statistic 2 against tolerance 5 is accepted; the worked certificate 2 <= 5 as a native nnrat/at-most; and statistic 8 against tolerance 5 is rejected. The proposal draws and the acceptance ratio (fraction retained) are executable concerns; what is proved here is the acceptance decision at these instances. That the retained samples form a valid conditional sample is the classical property of rejection sampling and is not proved here. Requires nnrat/at-most, audit/decide-nnrat-at-most, and nnrat/decide-at-most-true-sound (all 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.rejection-sampling` prints this classification.

rejection/accepts? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

rejection/accepts-consistent :
  → lis/extends? 2 5 = data/true

rejection/accepted-is-valid :
  → 2 ≤ 5

rejection/rejects-inconsistent :
  → lis/extends? 8 5 = data/false