Skip to content
Rainbow docs menu

Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.composite-metric

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/composite_metric.clj4 definitions, 3 theorems

AHoF V5 worked composite metric over exact rationals, combining an accuracy of 3/4 and a precision of 1/4. With balanced weights 1/2 and 1/2 the composite is (1/2)(3/4) + (1/2)(1/4) = 1/2. With accuracy-only weights 1 and 0 the composite is (1)(3/4) + (0)(1/4) = 3/4, so the weighting genuinely changes the aggregate. The composite values are proved by cross-product equivalence. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.composite-metric` prints this classification.

ahof-v5/accuracy

DefinitionSource, line 59

ahof-v5/accuracy :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

ahof-v5/precision

DefinitionSource, line 63

ahof-v5/precision :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

ahof-v5/balanced-composite

DefinitionSource, line 67

ahof-v5/balanced-composite :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

ahof-v5/accuracy-weighted-composite

DefinitionSource, line 72

ahof-v5/accuracy-weighted-composite :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

ahof-v5/balanced-is-one-half

TheoremWorked exampleNo axiomsSource, line 84

ahof-v5/balanced-is-one-half :
  → ahof-v5/balanced-composite = 1/2

= = nnrat/equivalent: equality of rational values

ahof-v5/accuracy-weighted-is-three-quarters

TheoremWorked exampleNo axiomsSource, line 92

ahof-v5/accuracy-weighted-is-three-quarters :
  → ahof-v5/accuracy-weighted-composite = 3/4

= = nnrat/equivalent: equality of rational values

ahof-v5/composite-metric

TheoremWorked exampleNo axiomsSource, line 103

ahof-v5/composite-metric :
  → proposition/conjunction (ahof-v5/balanced-composite = 1/2) (ahof-v5/accuracy-weighted-composite = 3/4)

= = nnrat/equivalent: equality of rational values