Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.kadane

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

AHoF Kadane's Algorithm: find the maximum-sum contiguous subarray in a single O(n) pass. It tracks the best subarray sum ending at the current position; at each element it decides whether to EXTEND the previous subarray (if that still helps) or RESTART at the current element -- the best-ending-here value is best-ending element extended = max(element, extended) where extended = previous-best-ending + element; extending wins exactly when the extended sum is at least the element alone (i.e. the previous best-ending was non-negative): extend? extended element = decide (element <= extended) over exact-rational (non-negative) values. Proved native and axiom-free: the extend/restart decision; that extending wins when it helps; the certificate that a chosen extension is at least the element alone (native nnrat/at-most); and that a non-helpful extension restarts. The running maximum over positions is executable; what is proved is the extend-vs-restart decision. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound (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.ahof.kadane` prints this classification.

kadane/extend? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

kadane/extending-helps :
  → bo/is-safe 7 5 = data/true

kadane/extension-at-least-element :
  → 5 ≤ 7

kadane/restart-when-not-helpful :
  → bo/is-safe 2 5 = data/false