15

我正在尝试确切地了解证明程序正确的含义。我从头开始，开始关注第一步/主题介绍。

在这篇关于全函数式编程的论文中，给出了斐波那契函数的两个定义。传统的一种：

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)

到目前为止，这也没有帮助。谁能告诉我如何进行感应？或链接到显示证明的页面（我进行了搜索，找不到任何东西）。

4

5 回答 5

12

在 Agda 中的 pad 证明的机器检查版本：

module fibs where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

fib : ℕ → ℕ
fib 0 = 0
fib 1 = 1
fib (suc (suc n)) = fib n + fib (suc n)

f : ℕ → ℕ → ℕ → ℕ
f 0 a b = a
f (suc n) a b = f n b (a + b)

fib' : ℕ → ℕ
fib' n = f n 0 1

-- Exactly the theorem the user `pad` proposed:
Theorem : ℕ → Set
Theorem n = ∀ k → f n (fib k) (fib (suc k)) ≡ fib (k + n)

-- Helper theorems about natural numbers:
right-identity : ∀ k → k ≡ k + 0
right-identity zero = refl
right-identity (suc n) = cong suc (right-identity n)

1+m+n≡m+1+n : ∀ n k → suc (n + k) ≡ n + suc k
1+m+n≡m+1+n zero k = refl
1+m+n≡m+1+n (suc n) k = cong suc (1+m+n≡m+1+n n k)

-- The base case. 
-- Theorem 0 by definition expands to (∀ k → fib k ≡ fib (k + 0))
-- and we prove that using the right-identity theorem.
th-base : Theorem 0
th-base k = cong fib (right-identity k)

-- The inductive step.
-- The definitions are expanded automatically, so (Theorem (suc n)) is
--   (∀ k → f n (fib (suc k)) (fib (suc (suc k))) ≡ fib (k + suc n))
-- We can apply the induction hypothesis to rewrite the LHS to 
--   (fib (suc k + n))
-- which is equal to the RHS by the 1+m+n≡m+1+n theorem.
th-step : ∀ n → Theorem n → Theorem (suc n)
th-step n hyp k = trans (hyp (suc k)) (cong fib (1+m+n≡m+1+n k n))

-- The inductive proof of Theorem using th-base and th-step.
th : ∀ n → Theorem n
th zero = th-base
th (suc n) = th-step n (th n)

-- And the final proof:
fibs-equal : ∀ n → fib' n ≡ fib n
fibs-equal n = th n 0
于 2011-12-08T16:19:50.380 回答
10

I couldn't access to the above mentioned paper, but their generalized theorem is a good way to go. Two values 0 and 1 in f n 0 1 sound like magic numbers; however if you generalize them to Fibonacci numbers, a proof is much easier to be conducted.

To avoid confusion when reading the proof, fib k is written as F(k) and some unnecessary parentheses are also removed. We have a generalized theorem: forall k. fib' n F(k) F(k+1) = F(k+n) and prove it by induction on n.

Base case with n=1:

fib' 1 F(k) F(k+1) = F(k+1) // directly deduce from definition of fib'

Inductive step:

We have the induction hypothesis where:

forall k. fib' n F(k) F(k+1) = F(k+n)

And we have to prove:

forall k. fib' (n+1) F(k) F(k+1) = F(k+(n+1))

The proof starts from the left-hand side:

fib' (n+1) F(k) F(k+1)
= fib' n F(k+1) (F(k) + F(k+1)) // definition of fib'
= fib' n F(k+1) F(k+2) // definition of F (or fib)
= F((k+1)+n) // induction hypothesis
= F(k+(n+1)) // arithmetic

We completed the generalized proof. Your example is also proven because it is a specific case of the above theorem with k=0.

As a side note, fib' isn't strange at all; it is a tail-recursive version of fib.

于 2011-12-08T09:33:10.110 回答
5

I believe your proof would be easier to recognize with Strong Induction:

... in the second step we may assume not only that the statement holds for n = m but also that it is true for all n less than or equal to m.

You were getting stuck here:

fib' (k+1)  = fib (k+1)
f (k+1) 0 1 = fib k + fib (k-1)

.. in part because you need to have both the steps from k+1 to k but also k+1 to k-1.

Sorry this isn't more convincing, it's been years since I've done real proofs.

于 2011-12-08T09:13:51.433 回答
4

If the paper says it is equivalent to 

Lemma:
f n (fib p) (fib (p+1)) = fib (p+n)

we should start by proving that. The key here is use generalized induction, that is, keep track of your forall quantifiers.

First we show

forall p, f 0 (fib p) (fib (p+1)) = fib p = fib (p + 0)

Now, we assume the inductive hypothesis

forall p, f n (fib p) (fib (p+1)) = fib (p + n)

and show

forall p, f (n+1) (fib p) (fib (p+1)) = f n (fib (p+1)) (fib (p+1) + fib p)
                                      = f n (fib (p+1)) (fib (p + 2)) --By def of fib
                                      = fib ((p + 1) + n) --By induction hypothesis
                                      = fib (p + (n+1))

So, that shows the lemma.

That makes it easy to prove your goal. If you have

fib' n = f n 0 1
       = f n (fib 0) (fib (0 + 1)) --by def of fib
       = fib (n + 1) --by lemma

Btw, if you are interested in this kind of thing, I suggest you check out Benjamin Pierce's free book on "Software Foundations." It is the textbook for a course on programming languages that uses the Coq proof assistant. Coq is like an uglier, meaner, and more powerful Haskell that lets you prove properties of your functions. It is good enough to do real math (prove of four color theorem), but the most natural thing to do in it is proven correct functional programs. I find it nice to have a computer check my work. And, all functions in Coq are total...

于 2011-12-08T09:32:55.270 回答
3

有时不要一开始就太正式是个好主意。我认为一旦你看到尾递归版本只是简单地传递 F(n-2) 和 F(n-1) 以避免在每一步中重新计算，这会给你一个证明想法，然后你将其形式化。

于 2011-12-08T10:20:15.890 回答