斐波那契功能的正確性的歸納法證明

Question

Haskell的實現熟悉的斐波那契功能

fibSlow n

| n == 0 = 1 --fib.1

| n == 1 = 1 --fib.2

| otherwise = fibSlow(n-1) + fibSlow(n-2) --fib.3

什麼是正確的爲fibSlow感應證明？

Answer 1

要通過歸納證明函數對自然數的正確性，您應該證明它對於某些基本情況是正確的，並且假設它對於較低值是正確的，則對於較高值的參數是正確的。所以你首先要驗證fibSlow 0 = 1，然後fibSlow 1 = 1，然後對於n> 1，fibSlow n等於第（n-1）斐波納契數加上第（n-2）斐波納契數。在這裏，您可以假設這些數字是fibSlow (n-1)和fibSlow (n-2)，因爲fibSlow對於歸納假設的所有小於n的輸入都是正確的。

這看起來似乎很平凡......因爲它是！ Haskell中這樣一個例子的重點在於你可以編寫明顯正確的代碼。當你去證明它是正確的，證明只是寫自己，並等於看代碼，並指出它清楚地說明了你想要證明什麼。這是像Haskell這樣的聲明性語言的一個很好的屬性。

Answer 2

道歉我還沒有正式看過這種材料一段時間，所以如果這是家庭作業，你可能最好看其他來源。

我想你想展示描述遞歸「進度」的單調函數的存在。這種情況應該非常簡單：參數本身是單調遞減的。對於非負n，遞歸調用將使用較小的n'進行，並且n'永遠不會小於零。

您還可以使用電源感應來辯論該功能是在所有的n上定義的。您已將其定義爲0和1，並且足以說明如果它定義於n和n + 1，則它定義在n + 2。遞歸調用的定義很明顯。

我想你可能會在Jech's Set Theory一書的正文部分閱讀一些手續。