Вот моя реализация алгоритма Кадане, которую я написал для OCaml:
let rec helper max_now max_so_far f n index =
if n < index then max_so_far
else if max_now + f index < 0
then helper 0 max_so_far f n (index+1)
else helper (max_now + (f index))
(max max_so_far (max_now + (f index))) f n (index+1)
let max_sum f n = helper 0 0 f n 1
Теперь я хочу формально доказать, что это правильно. Спецификация моего кода:
Функция f для аргументов от 1 до n возвращает целое число. Функция max_sum с параметрами f n должна возвращать наибольшую сумму сумм:
Где 1‹=a‹=b‹=n.
Вам не нужно анализировать мой код — я просто пытаюсь доказать, что алгоритм Кадане работает с помощью индукции. Проблема в том, что я не знаю, как подойти к этой проблеме — доказательство простых процедур, таких как разложение на множители или факториалы, довольно просто, но когда дело доходит до чего-то более абстрактного, такого как поиск подмассива с максимальной суммой, я даже не знаю, с чего начать. Любые подсказки?
