Reference · Algorithm guarantees

rainbow.algorithms.proofs.full-factorial

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

AHoF O58 Full Factorial Sampling: the design size is the product of the per-dimension level counts. Full-factorial sampling evaluates the objective at every point of the Cartesian product of the per-dimension level sets, so with level counts [n_1, ..., n_k] the design has exactly prod n_i points: design-size levels = fold multiply 1 levels This is the MAP-OVER cardinality underlying `(map evaluate (cartesian-product levels))`; it is an exact natural-number fold (`nat/multiply` over the list, identity 1), so the count is proved data, not a floating estimate. The actual enumeration of sample points stays an executable concern; what is proved here is the design-size recurrence and worked instances that reduce by reflexivity (concrete nat products). Scope (measured by the kernel): this module has 3 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.full-factorial` prints this classification.

full-factorial/design-size :
  (x₁ : List ℕ)
  → ℕ

full-factorial/design-size-unfold :
  (levels : List ℕ)
  → full-factorial/design-size levels = full-factorial/design-size levels

full-factorial/design-size-2x3-example :
  → full-factorial/design-size [2, 3] = 6

full-factorial/design-size-2x3x2-example :
  → full-factorial/design-size [2, 3, 2] = 12

full-factorial/design-size-empty-example :
  → full-factorial/design-size [] = 1