什么算法的正式证明 return

Question

我需要正式证明下面的算法 return 1 for n = 1 and 0 in other cases。

function K( n: word): word;
begin
   if (n < 2) then K := n
   else K := K(n − 1) * K(n − 2);
end;

有人能帮忙吗？谢谢

Answer 1

对于 n=1，通过调用算法，答案是 K=n=1，所以我们已经完成了这种情况。
对于 n=0，根据定义，K(0) = 0。

对于n>1的情况，我们可以归纳求解：

基础：对于n=2，我们得到：K(2) = K(1)*K(0) = 1*0 = 0
对于 n=3，我们得到： K(3) = K(2)*K(1) = 0*1 = 0 注意 K(2)=0 因为我们只显示了一行。
声明：对于任何1<k<n，我们得到K(k) = 0
对于任何 n>3 的证明：K(n) = K(n-1)*K(n-2) =(1) 0*0 = 0

(1)：归纳假设，因为K(n-1),K(n-2)都适用，因为n-1,n-2>1

P.S。请注意，声明对于非负数是正确的，例如，如果您允许 n=-5，您将得到 K(-5)=-5 - 这是声明的反例。

Answer 2

说 n = 0。由于 0 < 2 我们得到 0 作为结果。

说 n = 1。由于 1 < 2 我们得到 1 作为结果。

说 n = 2. K(2) = K(1)*K(0)。由于 K(0) = 0 我们得到 0 作为结果。

对于 n > 2 现在我们假设关于算法的陈述是正确的，即 K(n) = 0。现在证明对于 n + 1:

也是如此

K(n + 1) = K(n)*K(n - 1)。由于 K(n) = 0 很明显 K(n)*K(n - 1) = 0.

Answer 3

这可以通过归纳法证明，但正如之前的发帖人所展示的那样，在证明中直接引用 K 时很难在形式上正确。

这是我的建议：让 P(n) 成为我们要显示的属性：

P(n) 持有当且仅当 K(n) 对 n = 1 产生 1，对 n ≠ 1 产生 0.

现在我们可以清楚的表达我们想要展示的内容了：Ɐn.P(n)

基本情况： n ≤ 2

案例分析的简单检查：

P(0) 没问题，因为 K(0) = 0
P(1) 没问题，因为 K(1) = 1
归纳假设：

P(n) 对所有 2 ≤ n < c.
归纳步：证明P(c)成立
1. 根据 K 的定义，我们有 K(c) = K(c-1) × K(c-2)
2. 由归纳假设，我们知道P(c-1)和P(c-2)等一下。
3. 因为最多 K(c-1) 和 K(c-2)可以为1（另一个必须为0）乘积为0.
4. 这意味着 P(c) 成立

Qed.

什么算法的正式证明 return

Formal proof for what algorithm return

algorithm

proof

fibonacci