我正在尝试学习证明程序正确的确切含义。我从零开始,但在第一步/主题介绍上遇到了困难。
在这篇关于完全函数式编程的论文中,给出了斐波那契函数的两个定义。传统的定义如下:
fib 0 = 0
fib 1 = 1
fib n = fib (n-1) + fib (n-2)
--fib (n+2) = fib (n+1) + fib (n+2) --The definition as given in the paper
--It seems incorrect to me. Typo?
还有一个尾递归版本,我以前从未见过:
fib' n = f n 0 1
f 0 a b = a
f n a b = f (n-1) b (a+b)
该论文声称通过归纳法很容易证明这两个函数对所有正整数n返回相同的结果。这是我第一次考虑分析程序。想到可以证明两个程序是等价的,这种想法真的很有趣,所以我立即尝试自己用归纳法证明。要么是我的数学技能有些生疏,要么这个任务并不像它声称的那么简单。
我证明了n = 1的情况。
fib' 1 = f 1 0 1
= f 0 1 1
= 1
fib 1 = 1 (By definition)
therefore
fib' n = fib n for n = 1
我做出了 n = k 的假设
fib' k = fib k
f k 0 1 = fib k
我开始尝试证明如果假设成立,那么函数在 n = k + 1 的情况下也是相等的(因此它们对于所有 n >= 1 都是相等的 QED)
fib' (k+1) = fib (k+1)
f (k+1) 0 1 = fib k + fib (k-1)
我尝试了各种操作,适时替换假设等,但我就是无法使左边等于右边,从而证明这些函数/程序是等价的。我错过了什么?论文提到这个任务等同于证明
f n (fib p) (fib (p+1)) = fib (p+n)
对于任意的p, 通过数学归纳法证明。但我完全看不出来这是正确的。作者是如何得出这个方程的呢?只有当p=0
时,这是该方程式上的有效转换。我不明白这意味着它适用于任意p。要证明它对任意p都成立,需要再进行一层归纳。肯定应该证明的正确公式是
fib' (n+p) = fib (n+p)
f (n+p) 0 1 = fib (n+p)
到目前为止,这并没有起到帮助的作用。有人可以向我展示如何进行归纳吗?或者链接到一个显示证明的页面(我搜索过,但找不到任何信息)。
fib (n+2) = fib (n+1) + fib (n+2)
显然是个打字错误,他们可能想表达的是fib (n+2) = fib (n+1) + fib n
,这是数学上正确的,但将被从有效的 Haskell 中移除。http://hackage.haskell.org/trac/haskell-prime/wiki/RemoveNPlusK - Philip JF