दो अलग-अलग फाइबोनैकी कार्यों को समतुल्य

Question

दिखा रहा है मैं एक प्रोग्राम को सही साबित करने के लिए वास्तव में क्या सीखने का प्रयास कर रहा हूं। मैं खरोंच से शुरू कर रहा हूं और पहले चरण/विषय के परिचय पर लटका रहा हूं।

कुल कार्यात्मक प्रोग्रामिंग पर this paper में, फाइबोनैकी फ़ंक्शन की दो परिभाषाएं दी जाती हैं। पारंपरिक एक:

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 के लिए साबित कर दिया = 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 

मैं एन = कश्मीर धारणा

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

मैं साबित होता है कि इस धारणा सच है, तो कार्य भी कर रहे हैं के लिए बराबर की कोशिश कर रहा शुरू कर दिया एन = k + 1 (और इसलिए वे सभी सभी n के लिए बराबर हैं> = 1 QED)

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

मैं कोशिश की है विभिन्न manipulat आयनों, सही समय पर धारणा को प्रतिस्थापित कर रहा है, लेकिन मुझे केवल एलएचएस बराबर आरएचएस नहीं मिल सकता है और इसलिए साबित होता है कि कार्य/कार्यक्रम बराबर हैं। मैं क्या खो रहा हूँ? पेपर का उल्लेख है कि यह कार्य

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

मनमाने ढंग से पी के लिए प्रेरण के बराबर है। लेकिन मैं नहीं देखता कि यह कैसे सच है। लेखकों ने इस समीकरण पर कैसे पहुंचे? यह केवल p = 0 पर समीकरण पर एक वैध परिवर्तन है। मैं नहीं देखता कि इसका मतलब है कि यह मनमाने ढंग से पी के लिए काम करता है। मनमाने ढंग से पी के लिए इसे साबित करने के लिए आपको प्रेरण की एक और परत से गुजरना होगा। निश्चित रूप से साबित करने के लिए सही सूत्र

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

अभी तक इससे कोई मदद नहीं मिली है। क्या कोई मुझे दिखा सकता है कि प्रेरण कैसे किया जाएगा? या एक पृष्ठ से लिंक जो सबूत दिखाता है (मैंने खोज की, कुछ भी नहीं मिला)।

Answer 1

मैं उपर्युक्त कागज करने के लिए उपयोग नहीं कर सका, लेकिन उनके सामान्यीकृत प्रमेय जाने के लिए एक अच्छा तरीका है। f n 0 1 में दो मान 0 और 1 जादू संख्याओं की तरह ध्वनि; हालांकि यदि आप उन्हें फिबोनाची संख्याओं में सामान्यीकृत करते हैं, तो सबूत आयोजित करना बहुत आसान होता है।

सबूत पढ़ने पर भ्रम से बचने के लिए, fib kF(k) के रूप में लिखा गया है और कुछ अनावश्यक कोष्ठक भी हटा दिए गए हैं। हमारे पास एक सामान्यीकृत प्रमेय है: forall k. fib' n F(k) F(k+1) = F(k+n) और इसे n पर प्रेरण से साबित करें।

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) 

और हम साबित करना है:

n = 1 के साथ

बेस मामले

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 का एक पूंछ-पुनरावर्ती संस्करण है।

Answer 2

मेरा मानना ​​है कि अपने प्रमाण Strong Induction साथ पहचान करने के लिए आसान होगा:

... दूसरे चरण में हम यह मान सकते हैं कि न केवल बयान n = m के लिए रखती है, लेकिन यह भी कि यह सब के लिए सच है कि मीटर से कम या बराबर।

आप यहाँ अटक गया:

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

.. भाग में, क्योंकि आप k+1 से k के लिए बल्कि k+1k-1 के दोनों चरणों की आवश्यकता है।

क्षमा करें यह अधिक विश्वसनीय नहीं है, यह वर्ष है क्योंकि मैंने वास्तविक सबूत किए हैं।

Answer 3

कागज इसे करने के लिए

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 

Btw है, तो अगर आप बात इस तरह का में रुचि रखते हैं, मैं तुम्हें पर बेंजामिन पियर्स के नि: शुल्क पुस्तक की जाँच का सुझाव "सॉफ्टवेयर मूलाधार।" यह प्रोग्रामिंग भाषाओं पर पाठ्यक्रम के लिए पाठ्यपुस्तक है जो कोक सबूत सहायक का उपयोग करता है। Coq एक उग्र, अर्थपूर्ण, और अधिक शक्तिशाली हैस्केल की तरह है जो आपको अपने कार्यों के गुण साबित करने देता है। असली गणित (चार रंग प्रमेय का साबित) करने के लिए पर्याप्त है, लेकिन इसमें सबसे प्राकृतिक चीज सही कार्यात्मक कार्यक्रम साबित हुई है। मुझे लगता है कि कंप्यूटर मेरे काम की जांच करना अच्छा लगता है। और, Coq में सभी कार्यों की कुल रहे हैं ...

Answer 4

कभी-कभी औपचारिक रूप से शुरू नहीं करना एक अच्छा विचार है। मुझे लगता है जैसे ही आप देखते हैं कि पूंछ रिकर्सिव संस्करण प्रत्येक चरण में पुनर्मूल्यांकन से बचने के लिए बस एफ (एन -2) और एफ (एन -1) पास करता है, यह आपको एक सबूत विचार देता है, जिसे आप औपचारिक रूप से लागू करते हैं।

Answer 5

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