Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.particle-filter

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

AHoF D10 Particle Filter (sequential Monte Carlo): approximate a filtering distribution by a weighted set of particles, propagated and reweighted each step, then RESAMPLED to combat weight degeneracy. Resampling draws new particles in proportion to their normalized weights via inverse-transform sampling over the cumulative weight distribution: resamples? cumulative u = decide (u <= cumulative) over the exact-rational cumulative weight. Proved native and axiom-free, as worked instances: a draw of 4 against cumulative weight 6 resamples; the worked certificate 4 <= 6 (native nnrat/at-most); and a draw of 4 against cumulative weight 2 skips. That resampling is proportional to weight and keeps the approximation unbiased is the algorithm's classical property, not proved here; the cumulative weights, the propagation/likelihood models and RNG are executable. Requires nnrat/at-most, audit/decide-nnrat-at-most, 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.particle-filter` prints this classification.

particle-filter/resamples? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

particle-filter/resamples-particle :
  → bo/is-safe 6 4 = data/true

particle-filter/resample-is-proportional :
  → 4 ≤ 6

particle-filter/skips-below-draw :
  → bo/is-safe 2 4 = data/false