algorithm - 用归纳法证明线性最大子数组算法

Question

这是我编写 OCaml 的 Kadane 算法的实现:

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

现在我想正式证明它是正确的。我的代码规范:

参数 1 到 n 的函数 f 返回一个整数。参数为 f n 的函数 max_sum 应该返回最大的总和总和:

其中 1<=a<=b<=n。

您不需要分析我的代码 - 我只是想证明 Kadane 的算法使用归纳法有效。问题是我不知道如何解决这个问题——证明像因式分解或阶乘这样的简单过程非常简单，但是当涉及到更抽象的事情时，比如找到具有最大总和的子数组，我什至不知道从哪里开始。有什么提示吗？

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')