Reference · Algorithm guarantees

rainbow.algorithms.proofs.histogram-bin

Algorithm guaranteessrc/rainbow/algorithms/proofs/histogram_bin.clj1 definitions, 4 theorems

AHoF histogram / kernel-density bin count: the number of sample values that fall inside a half-open-style bin [lo, hi], count-in-range lo hi xs = |{ x in xs : lo <= x and x <= hi }|, the primitive behind histograms and (boxcar-kernel) density estimation. It is a fold over the sample list that increments a natural counter exactly when both decidable rational comparisons hold, expressed as nested if-data (no boolean connective needed): count (x :: rest) = if (lo <= x) then (if (x <= hi) then succ (count rest) else count rest) else count rest. Exact naturals and the decidable rational order, so the bin count is proved data. Sweeping bins into a full histogram or normalizing into a density is an executable concern; what is proved here is the bin-count fold and worked counts. Requires nat, the decidable nnrat order (audit/decide-nnrat-at-most), logic/if-data, and data/List.rec (all carried by the D63 checkpoint). Scope (measured by the kernel): this module has 1 worked instances (statements about specific values) and 3 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.histogram-bin` prints this classification.

histogram/count-in-range :
  (x₁ x₂ : ℚ≥0) (x₃ : List ℚ≥0)
  → ℕ

histogram/cons-in-bin-increments :
  (xs : List ℚ≥0)
  → histogram/count-in-range 2 6 (data/cons ℚ≥0 4 xs) = data/succ (histogram/count-in-range 2 6 xs)

histogram/cons-below-bin-preserves :
  (xs : List ℚ≥0)
  → histogram/count-in-range 2 6 (data/cons ℚ≥0 1 xs) = histogram/count-in-range 2 6 xs

histogram/cons-above-bin-preserves :
  (xs : List ℚ≥0)
  → histogram/count-in-range 2 6 (data/cons ℚ≥0 7 xs) = histogram/count-in-range 2 6 xs

histogram/count-example :
  → histogram/count-in-range 2 6 [1, 4, 7, 5] = 2