Reference · Algorithm guarantees

rainbow.algorithms.proofs.prefix-sum

Algorithm guaranteessrc/rainbow/algorithms/proofs/prefix_sum.clj2 definitions, 3 theorems

Cumulative sum (prefix-sum / scan): the running totals of a list, cumulative-sum [x0, x1, x2, ...] = [x0, x0+x1, x0+x1+x2, ...]. This is the scan primitive behind CDF construction for inverse-transform sampling (AHoF D5), roulette-wheel selection (genetic algorithms), and cumulative-reward / return-to-date accounting. It is proved as a native higher-order fold: List.rec whose motive is the function type (nat -> list nat), threading the running accumulator so that each output entry is the accumulator plus the current element. Proved axiom-free: the scan, its cons recurrence, and a worked running-total, all reducing by reflexivity. Requires nat, algebra/nat-add, and data/List.rec (all in the D63 checkpoint). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 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.prefix-sum` prints this classification.

prefix-sum/scan-from :
  (x₁ : List ℕ) (x₂ : ℕ)
  → List ℕ

prefix-sum/cumulative-sum :
  (x₁ : List ℕ)
  → List ℕ

prefix-sum/scan-cons :
  (acc head : ℕ) (tail : List ℕ)
  → prefix-sum/scan-from (data/cons ℕ head tail) acc = data/cons ℕ (algebra/nat-add acc head) (from)
  where from := prefix-sum/scan-from tail (algebra/nat-add acc head)

prefix-sum/cumulative-sum-example :
  → prefix-sum/cumulative-sum [1, 2, 3] = [1, 3, 6]

prefix-sum/cumulative-sum-empty :
  → prefix-sum/cumulative-sum [] = []