12

我想知道是否存在任何证明算法正确性的规则/方案？例如，我们在自然数上定义了一个函数 $F$，定义如下：

function F(n,k)
begin
  if k=0 then return 1
  else if (n mod 2 = 0) and (k mod 2 = 1) then return 0
  else return F(n div 2, k div 2);
end;

其中 $n \ \text{div}\ 2 = \left\lfloor\frac{n}{2}\right\rfloor$

任务是证明 $F(n,k)= \begin{cases} 1 \Leftrightarrow {n \choose k} \ \text{mod} \ 2 = 1 \ 0 \text{ else } \end{cases} $

它看起来不是很复杂（我错了吗？），但我不知道这种证明应该如何构建。我将非常感谢您的帮助。

4

3 回答 3

6

递归算法的正确性通常由数学归纳法证明。该方法由两部分组成：首先，建立基础，然后使用归纳步骤。

在您的情况下，基础是 k=0 或 k 为奇数但 n 为偶数时的所有情况。

归纳步骤需要证明 whenf(n,k)是正确的，f(2*n,2*k),f(2*n+1,2*k)和f(2*n,2*k+1)都是f(2*n+1,2*k+1)正确的。

于 2012-03-02T18:45:32.083 回答
6

除了在数学上证明你的逻辑（例如：归纳证明）之外，在计算科学中也有一些与此相关的结果。

您可以从这里开始概述主题：正确性
对于您的特定情况，您可能对部分正确性感兴趣，以表明答案是预期的。然后完全正确地表明程序终止。

霍尔逻辑可以解决您的部分正确性。

至于这个特定问题的终止：

如果 (n%2==0 and k%1==1) 或 (k==0) 程序终止，否则它递归到 n/2, k/2 的情况。
对 k使用强归纳，我们可以证明程序总是到达 k==0 的终端节点之一。（它可能在第一个子句之前终止，但我们只需要证明它完全终止，就是这样）

所以我把部分正确性的证明留给了你（因为我不知道那些东西）

于 2012-03-02T18:45:50.670 回答
2

一般来说，你会尝试通过归纳来证明正确性。这在证明递归函数的正确性时非常有效，因为您可以直接证明基本情况，然后可以使用该函数适用于“较小”输入的事实来证明它适用于下一个最大输入。

在这种情况下，我会尝试通过有根据的归纳来证明。具体来说，我会证明

  1. 该函数对于 (n, 0) 形式的所有输入都是正确的。
  2. 假设对于所有输入 (n', k') 使得 (n', k') 在字典上小于 (n, k)，则该函数是正确的，证明它对于 (n, k) 是正确的。

这个证明的细节需要利用函数的细节和二项式系数的 bahvaior，但一般模板如上所述。

希望这可以帮助！

于 2012-03-02T18:40:37.653 回答