algorithm - 如何证明以下代码的正确性？

Question

我遇到了以下问题:

编写一个函数，给定一个列表 l 和一个 int c，返回 min(|c+x1+x2|)，其中 x1 和 x2 是列表中的一些值。 [也有可能 x1=x2]

我有一段代码显然可以解决这个问题:

let bestSum l c =
  let rec f l lr res =
    match (l,lr) with
    | ([],lr) -> res
    | (l,[]) -> res
    | (h1::t1, h2::t2) -> if (h1+h2+c)>0 then f l t2 (min res (h1+h2+c)) else
                            f t1 lr (min res (-(h1+h2+c))) in
  f l (rev l) (abs (2* (hd l) + c));;

凭直觉，我知道它的工作原理和原因，但我不确定它是否适用于所有可能的情况。那么如何正式证明呢？

编辑:是的，我忘了添加，列表已排序，抱歉。

Answer 1

我将假定您的列表已排序，否则它不起作用。这是对您的算法的描述，应该清楚说明您的程序为何有效。假设您的数字是 x[0], x[1], ... , x[n]。目标是找到两个数字 x[i] 和 x[j]，使它们的总和尽可能接近 -c。让我们通过 (n + 1) 网格在 (n + 1) 中绘制值 x[i] + x[j] + c ，用 + 标记正值，用 - 标记负值(示例见下文)。目标是找到具有最小绝对值的单元格。

Example where c = 0, x = [-3, -2, 1, 4].

       x[0] x[1] x[2] x[3]

x[0]     -    -    -   (+)
x[1]     -    -   (-)  (+)
x[2]    (-)  (-)  (+)   + 
x[3]    (+)   +    +    + 

您会注意到 - 和 + 分为两个区域，确实必须如此，因为每个单元格的值都较小而不是正下方或右侧的单元格。根据该观察，唯一可以优化的单元格是位于 - 和 + 之间边界的单元格。

您的算法基本上遵循此边界(您的算法考虑的单元格标记在括号中)。让我们来看看几个步骤:

首先，考虑x[3] + x[0]。我们看到它是 +，所以 x[3] + x[1] 不可能更好，试试 x[2] + x[0] 接下来。

       x[0] x[1] x[2] x[3]

x[0]     ?    ?    ?    ?
x[1]     ?    ?    ?    ?
x[2]     *    ?    ?    ? 
x[3]    (+)   X    X    X 

* = thing to try next
X = ruled out

x[2] + x[0] 是负数，所以 x[1] + x[0] 不可能更好。接下来尝试 x[2] + x[1]。

       x[0] x[1] x[2] x[3]

x[0]     X    ?    ?    ?
x[1]     X    ?    ?    ?
x[2]    (-)   *    ?    ? 
x[3]    (+)   X    X    X 

x[2] + x[1] 是负数，所以 x[1] + x[1] 不能更好了。接下来尝试 x[2] + x[2]。

       x[0] x[1] x[2] x[3]

x[0]     X    X    ?    ?
x[1]     X    X    ?    ?
x[2]    (-)  (-)   *    ? 
x[3]    (+)   X    X    X 

...等等。