Используя индукцию, чтобы доказать линейный алгоритм максимального подмассив

Question

Вот моя реализация algorihm Kadane, что я написал 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 = а = Ь < < = п.

Вам не нужно анализировать мой код - я просто пытаюсь доказать, что алгоритм Кадане работает с использованием индукции. Проблема в том, что я не знаю, как подойти к этой проблеме. Простейшие процедуры, такие как факторинг или факториалы, довольно просты, но когда дело доходит до чего-то более абстрактного, например, для поиска субарама с максимальной суммой, я даже не знаю с чего начать. Любые намеки?

Answer 1

Основание индукции не будет проходить, поскольку алгоритм и спецификация не согласуются с тем, разрешен ли пустой подмассиво (с суммой 0). Я буду следовать спецификации, которая запрещает пустые подмассивы.

Индуктивный шаг заключается в следующем. Для всех k, определить

max_now = max_{a in 1..k } sum_{i in a..k } f(i) 
max_now' = max_{a in 1..k+1} sum_{i in a..k+1} f(i) 
max_so_far = max_{b in 1..k } max_{a in 1..b} sum_{i in a..b} f(i) 
max_so_far' = max_{b in 1..k+1} max_{a in 1..b} sum_{i in a..b} f(i). 

Мы должны показать, что

max_now' = max(max_now, 0) + f(k+1) 
max_so_far' = max(max_so_far, max_now'). 

Оба равенства доказываются путем разделения max.

max_now' =  max_{a in 1..k+1} sum_{i in a ..k+1} f(i) 
     = max(max_{a in 1..k } sum_{i in a ..k+1} f(i), 
            sum_{i in k+1..k+1} f(i)) 
     = max((max_{a in 1..k } sum_{i in a ..k } f(i)) + f(k+1), 
                   f(k+1)) 
     = max(max_now, 0) + f(k+1) 

max_so_far' =  max_{b in 1..k+1} max_{a in 1..b } sum_{i in a..b } f(i) 
      = max(max_{b in 1..k } max_{a in 1..b } sum_{i in a..b } f(i), 
            max_{a in 1..k+1} sum_{i in a..k+1} f(i)) 
      = max(max_so_far, max_now')