Reference · Algorithm guarantees

rainbow.algorithms.proofs.argmax-index

Algorithm guaranteessrc/rainbow/algorithms/proofs/argmax_index.clj2 definitions, 3 theorems

Argmax over a list of nonnegative rationals, returning the INDEX of the maximum element (the first index attaining it): argmax-index [x0, x1, ...] = the i minimizing (-x_i), ties to the earliest. This is the primitive behind greedy policy extraction (pi(s) = argmax_a Q(s,a)), action selection in value/policy iteration, and best-arm identification in bandits -- wherever you need WHICH option is best, not just its value. It is proved as a native HIGHER-ORDER fold: a data/List.rec whose motive is the function type (nat -> Product nat nnrat), threading the running index forward and carrying the (best-index, best-value) pair; at each element the running index wins a tie-or-better against the best of the suffix (via logic/if-data over the decision audit/decide-nnrat-at-most). Proved axiom-free: the fold, the empty case, and worked argmaxes -- all reducing by reflexivity. Requires nnrat, nat, audit/decide-nnrat-at-most, logic/if-data, data/Product/pair/product, and data/List.rec (all in the D63 checkpoint). 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.argmax-index` prints this classification.

argmax-index/argmax-from :
  (x₁ : List ℚ≥0) (x₂ : ℕ)
  → data/Product ℕ ℚ≥0

argmax-index/argmax-index :
  (x₁ : List ℚ≥0)
  → ℕ

argmax-index/argmax-middle :
  → argmax-index/argmax-index [5, 7, 4] = 1

argmax-index/argmax-first :
  → argmax-index/argmax-index [8, 3, 2] = 0

argmax-index/argmax-last :
  → argmax-index/argmax-index [2, 4, 9] = 2