我正在尝试确切地了解证明程序正确的含义。我从头开始,开始关注第一步/主题介绍。
在这篇关于全函数式编程的论文中,给出了斐波那契函数的两个定义。传统的一种:
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)
我尝试了各种操作,在正确的时间替换假设等等,但我不能让 LHS 等于 RHS,因此证明函数/程序是等价的。我错过了什么?论文中提到任务相当于证明
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)
到目前为止,这也没有帮助。谁能告诉我如何进行感应?或链接到显示证明的页面(我进行了搜索,找不到任何东西)。