Reference · Algorithm guarantees

rainbow.algorithms.proofs.list-product

Algorithm guaranteessrc/rainbow/algorithms/proofs/list_product.clj1 definitions, 3 theorems

Product of a list of nonnegative rationals, as a native fold: list-product [x0, x1, ...] = x0 * x1 * ... * xn (empty product = 1). This is the reduction behind joint probability of independent events, the likelihood of an i.i.d. sample (a product of per-datum likelihoods, as in naive Bayes), series-system reliability (a product of component reliabilities), and any multiplicative accumulation. It is proved as a native List.rec fold of nnrat/multiply from the multiplicative identity nnrat/one. Proved axiom-free: the fold, the empty and cons recurrences, and a worked product -- all reducing by reflexivity. Requires nnrat, nnrat/multiply, nnrat/one, 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.list-product` prints this classification.

list-product/product :
  (x₁ : List ℚ≥0)
  → ℚ≥0

list-product/product-empty :
  → list-product/product [] = 1

list-product/product-cons :
  (head : ℚ≥0) (tail : List ℚ≥0)
  → list-product/product (data/cons ℚ≥0 head tail) = head · list-product/product tail

list-product/product-example :
  → list-product/product [2, 3, 2] = 12