Reference · Algorithm guarantees

rainbow.algorithms.proofs.list-maximum

Algorithm guaranteessrc/rainbow/algorithms/proofs/list_maximum.clj2 definitions, 4 theorems

Maximum of a list of nonnegative rationals, as a native fold: list-maximum [x0, x1, ...] = max(x0, max(x1, ... max(xn, 0))). This is the reduction behind greedy best-of selection, maximum-fitness in evolutionary methods, Chebyshev / max-norm scalarization of multi-objective problems, and the max operator in value iteration over a finite action set. It is proved as a native List.rec fold of the decidable rational max (nnrat-max a b = if a <= b then b else a, built on logic/if-data over the decision audit/decide-nnrat-at-most). Proved axiom-free: the max operator, the fold, the empty and cons recurrences, and a worked maximum -- all reducing by reflexivity. Requires nnrat, audit/decide-nnrat-at-most, logic/if-data, and data/List.rec (all in the D63 checkpoint). 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.list-maximum` prints this classification.

list-maximum/nnrat-max :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

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

list-maximum/nnrat-max-example :
  → list-maximum/nnrat-max 3 7 = 7

list-maximum/maximum-empty :
  → list-maximum/maximum [] = 0

list-maximum/maximum-cons :
  (head : ℚ≥0) (tail : List ℚ≥0)
  → list-maximum/maximum (data/cons ℚ≥0 head tail) = list-maximum/nnrat-max head (list-maximum/maximum tail)

list-maximum/maximum-example :
  → list-maximum/maximum [3, 7, 2] = 7