Skip to content
Rainbow docs menu

Reference · Algorithm guarantees

rainbow.algorithms.proofs.composite-metric

Algorithm guaranteessrc/rainbow/algorithms/proofs/composite_metric.clj1 definitions, 1 theorems

Composite evaluation metrics over exact rationals. A composite metric is a weighted combination of atomic metrics: given weights and atomic metric values, the composite is `w1 * m1 + w2 * m2`. This composes exact-rational multiplication and addition to aggregate several atomic metrics into one score (AHoF V5). When the weights sum to one the composite is a weighted average of the metrics. Scope (measured by the kernel): this module has 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.composite-metric` prints this classification.

validation/composite-metric

DefinitionSource, line 37

validation/composite-metric :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

validation/composite-metric-unfold

TheoremHolds by unfolding a definitionNo axiomsSource, line 50

validation/composite-metric-unfold :
  (weight-a metric-a weight-b metric-b : ℚ≥0)
  → estimation/weighted-sum weight-a metric-a weight-b metric-b = weight-a · metric-a + weight-b · metric-b

+ = nnrat/add= = equality/Eq· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational