15

私は、プログラムが正しいことを証明することの意味を正確に学ぼうとしています。私はゼロから始めて、最初のステップ/トピックの紹介に夢中になっています。

トータル関数型プログラミングに関するこの論文では、フィボナッチ関数の2つの定義が与えられています。伝統的なもの：

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に対して同じ結果を返すことを帰納法によって証明することは「簡単」であると主張しました。このようなプログラムを分析することを考えたのはこれが初めてです。2つのプログラムが同等であることを証明できると考えるのは非常に興味深いので、私はすぐに帰納法によってこの証明を試みました。私の数学のスキルがさびているか、タスクが実際にはそれほど単純ではありません。

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のパッドのプルーフのマシンチェックバージョン：

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

私は上記の論文にアクセスできませんでしたが、彼らの一般化された定理は良い方法です。2つの値0と魔法の数字のよう1にf n 0 1聞こえます。ただし、それらをフィボナッチ数に一般化すると、証明を行うのがはるかに簡単になります。

証明を読むときの混乱を避けるために、fib kはとして書かれF(k)、いくつかの不要な括弧も削除されます。一般化された定理があります：forall k. fib' n F(k) F(k+1) = F(k+n)そしてそれをの誘導によって証明しnます。

n = 1の基本ケース：

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

帰納的ステップ：

ここで、誘導仮説があります。

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

そして、私たちは証明しなければなりません：

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

証明は左側から始まります。

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

一般化された証明を完成させました。あなたの例は、上記の定理の特定のケースであるため、証明されていk=0ます。

ちなみに、fib'まったく奇妙なことではありません。これは、の末尾再帰バージョンですfib。

于 2011-12-08T09:33:10.110 に答える
5

私はあなたの証明が強力な誘導で認識しやすいと信じています：

... 2番目のステップでは、ステートメントがn = mに当てはまるだけでなく、m以下のすべてのnにも当てはまると想定できます。

あなたはここで立ち往生していた：

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

k+1..部分的には、からへのステップkだけでなく、k+1へのステップも必要なためですk-1。

申し訳ありませんが、これはそれほど説得力がありません。私が実際の証明を行ってから何年も経ちました。

于 2011-12-08T09:13:51.433 に答える
4

論文がそれが同等であると言うならば

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

それを証明することから始めるべきです。ここで重要なのは、一般化された誘導を使用することです。つまり、すべての数量詞を追跡します。

最初に示します

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

ここで、帰納的仮説を仮定します

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

と表示

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))

だから、それは見出語を示しています。

それはあなたの目標を証明するのを簡単にします。あなたが持っている場合

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

ところで、この種のことに興味があるなら、BenjaminPierceの「SoftwareFoundations」に関する無料の本をチェックすることをお勧めします。Coq証明アシスタントを使用したプログラミング言語のコースの教科書です。Coqは、関数のプロパティを証明できる、醜く、意地悪で、より強力なHaskellのようなものです。実際の数学（四色定理の証明）を行うには十分ですが、その中で行う最も自然なことは、正しい機能プログラムであることが証明されています。コンピューターに自分の仕事をチェックしてもらうのはいいことだと思います。そして、Coqのすべての機能は合計です...

于 2011-12-08T09:32:55.270 に答える
3

あまりフォーマルに始めない方が良い場合があります。末尾再帰バージョンは、各ステップでの再計算を回避するためにF（n-2）とF（n-1）を渡すだけであることがわかるとすぐに、これにより証明のアイデアが得られ、それを形式化できます。

于 2011-12-08T10:20:15.890 に答える