归纳证明伪代码

Question

我不太理解如何在伪代码上使用归纳法。它似乎与在数学方程式上使用的方式不同。

我试图计算数组中可被k整除的整数的数量。

Algorithm: divisibleByK (a, k)
Input: array a of n size, number to be divisible by k
Output: number of numbers divisible by k

int count = 0;
for i <- 0 to n do
    if (check(a[i],k) = true)
        count = count + 1
return count;


Algorithm: Check (a[i], k)
Input: specific number in array a,  number to be divisible by k
Output: boolean of true or false

if(a[i] % k == 0) then
    return true;
else    
    return false;

如何证明这是正确的？谢谢

- John Smith

---

归纳法通常用于证明递归方法，而不是迭代方法。 - Daniel

@Dani，它同样适用于迭代算法。 - aioobe

Answer 1

在这种情况下，我会将"inductively"解释为“对迭代次数进行归纳”。首先，我们要建立一个所谓的循环不变式。在这种情况下，循环不变式是： count存储小于i的具有k索引的数字数量。 该不变式在循环进入时成立，并确保在循环后（当i=n时）count保存整个数组中可被k整除的值的数量。

归纳过程如下：

1. 基本情况：循环不变量在循环进入时（0次迭代后）成立。

   由于i等于0，没有元素的索引低于i。因此，索引小于i的元素都不可被k整除。因此，由于count等于0，循环不变量成立。

2. 归纳假设：我们假设不变量在循环顶部成立。

3. 归纳步骤：我们展示不变量在循环体底部也成立。

   执行完循环体后，i已经增加了1。为了使循环不变量在循环结束时成立，必须相应地调整count。

   由于现在有一个更小的索引（新的i）对应着一个元素（a[i]），如果a[i]可以被k整除，则应将count增加1，这正是if语句所保证的。

   因此，循环不变量在执行完循环体后仍然成立。

证毕。

---

在Hoare-logic中，它被证明（正式地）如下（为了清晰起见，将其重写为while循环）：

{ I }
{ I[0 / i] }
i = 0
{ I }
while (i < n)
    { I ∧ i < n }
    if (check(a[i], k) = true)
        { I[i + 1 / i] ∧ check(a[i], k) = true }
        { I[i + 1 / i][count + 1 / count] }
        count = count + 1
        { I[i + 1 / i] }
    { I[i + 1 / i] }
    i = i + 1
    { I }
{ I ∧ i ≮ n }
{ count = ∑ 0 x < n;  1 if a[x] ∣ k, 0 otherwise. }

我（不变量）的定义如下：

     count = ∑_{x < i} 1，如果a[x]∣k，否则为0。

（对于任何两个连续的断言行（{...}），都有一个证明义务（第一个断言必须暗示下一个），我将其留给读者作为练习；-)

- aioobe

Answer 2

我们通过对数组元素数量n进行归纳来证明正确性。您的范围有误，应为0到n-1或1到n，而不是0到n。我们将假设为1到n。

在n=0（基本情况）的情况下，我们手动执行算法。计数器以值0初始化，循环不迭代，并返回计数器的值，正如我们所说，为0。这是正确的。

我们可以进行第二个基本情况（虽然这是不必要的，就像在常规数学中一样）。 n=1。计数器初始化为0。循环执行一次，在其中i取值为1，并且仅当a中的第一个值可被k整除时，我们增加counter（由于Check算法的显然正确性），因此如果a[1]不能被k整除，则返回0，否则返回1。这种情况也可以解决。

归纳很简单。我们假设n-1的正确性，并将其证明为n（再次，就像在常规数学中一样）。为了正确形式化，我们注意到计数器在循环的最后一次迭代之后保持正确的值，即我们将返回的值。

根据我们的假设，我们知道经过n-1次迭代后，计数器具有关于数组中前n-1个值的正确值。我们调用n=1的基本情况来证明它将在最后一个元素可被k整除时将1添加到此值，因此最终值为n的正确值。

证毕。

您只需要知道要对哪个变量进行归纳。通常，输入大小最有帮助。此外，有时需要假设小于n的所有自然数的正确性，有时仅假设n-1的正确性。再次，就像在常规数学中一样。

- davin

---

我们通过对数组中元素个数n进行归纳来证明正确性。但这种方法注定会失败。你无法通过假设算法对长度为k的数组有效，来展示它对长度为k+1的数组同样有效（程序将运行出两个完全不同的结果！）。更好的方法是假设数组长度固定，并对循环迭代次数进行归纳。 - aioobe

澄清一下：当你说“我们假设n-1是正确的”时，实际上是在说“我们假设算法对长度为n-1的数组有效”。这与说“对于长度为k的数组，该算法在索引n-1之前按预期工作”是不同的（当展示算法在索引n之前按预期工作时，这实际上是你需要假设的）。 - aioobe

@aioobe，这就是我在后面进一步澄清的内容，当我写道“为了得到适当的正式性……”。我需要在这里补充的唯一一件事是，在长度为n的数组上，我们只在k次迭代中引用前k个元素。 - davin

为了正式规范，您需要一个引理来说明：“如果算法适用于长度为k的数组，则在处理长度大于k的数组时，在k次迭代后，count将保持正确的值。” 然而，我认为这样的引理本身需要归纳证明。 - aioobe

@aioobe，没错。不过我还是会把我的答案留在这里——希望其他人能从中了解到其中的不准确之处并受益。 - davin