Reference · The Applied Higher-Order Functions catalogue
rainbow.algorithms.proofs.ahof.composite-metric
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
ahof-v5/accuracy : → ℚ≥0
ℚ≥0 = nnrat/NonnegativeRational
ahof-v5/precision
ahof-v5/precision : → ℚ≥0
ℚ≥0 = nnrat/NonnegativeRational
ahof-v5/balanced-composite
ahof-v5/balanced-composite : → ℚ≥0
ℚ≥0 = nnrat/NonnegativeRational
ahof-v5/accuracy-weighted-composite
ahof-v5/accuracy-weighted-composite : → ℚ≥0
ℚ≥0 = nnrat/NonnegativeRational
ahof-v5/balanced-is-one-half
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
ahof-v5/accuracy-weighted-is-three-quarters : → ahof-v5/accuracy-weighted-composite = 3/4
= = nnrat/equivalent: equality of rational values
ahof-v5/composite-metric
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