Hiển thị hai hàm fibonacci khác nhau là tương đương

Question

Tôi đang cố gắng tìm hiểu chính xác ý nghĩa của chương trình để chứng minh một chương trình. Tôi bắt đầu từ đầu và bị treo lên trên các bước đầu tiên/giới thiệu về chủ đề.

Trong this paper trên tổng số lập trình hàm, hai định nghĩa của hàm fibonacci được đưa ra. Các truyền thống một:

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? 

và một phiên bản đệ quy đuôi tôi chưa bao giờ thấy trước đây:

fib' n = f n 0 1 
f 0 a b = a 
f n a b = f (n-1) b (a+b) 

giấy này sau đó tuyên bố rằng nó là "đơn giản" để chứng minh bằng quy nạp rằng cả hai chức năng trả lại kết quả tương tự cho tất cả các số nguyên dương n. Đây là lần đầu tiên tôi nghĩ đến việc phân tích các chương trình như thế này. Nó khá thú vị khi nghĩ rằng bạn có thể chứng minh rằng hai chương trình là tương đương, vì vậy tôi ngay lập tức đã cố gắng để làm bằng chứng này bằng cảm ứng bản thân mình. Kỹ năng toán học của tôi bị gỉ hoặc nhiệm vụ không thực sự đơn giản.

tôi đã chứng minh cho 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 

tôi đã n = k giả định

fib' k = fib k 
f k 0 1 = fib k 

tôi bắt đầu cố gắng để chứng minh rằng nếu giả định đúng, sau đó các chức năng cũng equivilant cho n = k + 1 (và do đó tất cả chúng đều tương đương với tất cả n> = 1 QED)

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

Tôi đã thử nhiều thao tác khác nhau ion, thay thế giả định vào đúng thời điểm và vân vân, nhưng tôi không thể lấy LHS bằng RHS và do đó chứng minh rằng các hàm/chương trình là tương đương nhau. Tôi đang thiếu gì? Bài viết đề cập rằng tác vụ tương đương với việc chứng minh

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

bằng cảm ứng cho tùy ý p. Nhưng tôi không thấy nó thật sự như thế nào. Các tác giả đã đến phương trình này như thế nào? Đó là một biến đổi hợp lệ trên phương trình chỉ khi p = 0. Tôi không thấy nó có nghĩa là nó hoạt động như thế nào cho p. Để chứng minh nó cho p tùy ý yêu cầu bạn phải trải qua một lớp cảm ứng khác. Chắc chắn công thức chính xác để chứng minh là

fib' (n+p) = fib (n+p) 
f (n+p) 0 1 = fib (n+p) 

Cho đến nay cũng không giúp được gì. Bất cứ ai có thể chỉ cho tôi cách cảm ứng sẽ được thực hiện? Hoặc liên kết đến một trang hiển thị bằng chứng (tôi đã tìm kiếm, không thể tìm thấy bất kỳ điều gì).

Answer 1

Tôi không thể truy cập vào giấy được đề cập ở trên, nhưng định lý tổng quát của chúng là một cách tốt để đi. Hai giá trị 0 và 1 trong số f n 0 1 âm thanh như số ma thuật; tuy nhiên nếu bạn tổng quát chúng thành các số Fibonacci, một bằng chứng sẽ dễ thực hiện hơn nhiều.

Để tránh nhầm lẫn khi đọc bằng chứng, fib k được viết là F(k) và một số dấu ngoặc đơn không cần thiết cũng bị xóa. Chúng tôi có một định lý tổng quát: forall k. fib' n F(k) F(k+1) = F(k+n) và chứng minh nó bằng cách cảm ứng trên n.

trường hợp cơ sở với n = 1:

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

Inductive bước:

Chúng tôi có giả thuyết cảm ứng nơi:

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

Và chúng ta phải chứng minh:

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

Bằng chứng bắt đầu từ phía bên trái:

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 

Chúng tôi đã hoàn thành bằng chứng tổng quát. Ví dụ của bạn cũng được chứng minh bởi vì nó là một trường hợp cụ thể của định lý trên với k=0.

Như một lưu ý phụ, fib' không lạ chút nào; nó là phiên bản đệ quy đuôi của fib.

Answer 2

Tôi tin rằng bằng chứng của bạn sẽ dễ dàng nhận ra với Strong Induction:

... trong bước thứ hai chúng ta có thể giả định không chỉ rằng tuyên bố giữ cho n = m mà còn là nó là đúng cho tất cả n nhỏ hơn hoặc bằng m.

Bạn đang bị mắc kẹt ở đây:

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

.. một phần vì bạn cần phải có cả các bước từ k+1 để k mà còn k+1 để k-1.

Xin lỗi điều này không thuyết phục hơn, đã là năm vì tôi đã thực hiện bằng chứng thực sự.

Answer 3

Nếu giấy nói nó tương đương với

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

chúng ta nên bắt đầu bằng cách chứng minh rằng. Chìa khóa ở đây là sử dụng cảm ứng được tổng quát hóa, nghĩa là, theo dõi lượng định lượng không xác định của bạn.

Đầu tiên chúng ta chứng tỏ

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

Bây giờ, chúng tôi giả định giả thuyết quy nạp

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

và hiển thị

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

Vì vậy, cho thấy bổ đề.

Điều đó giúp bạn dễ dàng chứng minh mục tiêu của mình. Nếu bạn có

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

Btw, nếu bạn quan tâm đến loại điều này, tôi khuyên bạn nên xem sách miễn phí của Benjamin Pierce trên "Nền tảng phần mềm". Đây là sách giáo khoa cho một khóa học về ngôn ngữ lập trình sử dụng trợ lý chứng minh Coq. Coq giống như một Haskell xấu hơn, trung bình hơn và mạnh mẽ hơn, cho phép bạn chứng minh tính chất của các chức năng của mình. Nó là đủ tốt để làm toán học thực tế (chứng minh của bốn định lý màu), nhưng điều tự nhiên nhất để làm trong nó được chứng minh các chương trình chức năng chính xác. Tôi tìm thấy nó tốt đẹp để có một máy tính kiểm tra công việc của tôi. Và, tất cả các chức năng trong Coq là tổng số ...

Answer 4

Đôi khi một ý tưởng hay là không bắt đầu quá trang trọng. Tôi nghĩ rằng ngay sau khi bạn thấy rằng phiên bản đệ quy đuôi chỉ đơn giản là vượt qua F (n-2) và F (n-1) xung quanh để tránh tính toán lại trong mỗi bước, điều này mang lại cho bạn một ý tưởng bằng chứng, sau đó bạn chính thức hóa.

Answer 5

Phiên bản máy kiểm tra chứng minh pad trong 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