Показаны две разные функции Фибоначчи эквивалентны

Question

Я пытаюсь точно понять, что значит доказать правильность программы. Я начинаю с нуля и зацикливаюсь на первых шагах / введении в тему.

В этой статье по полному функциональному программированию даны два определения функции Фибоначчи. Традиционный:

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, требуется пройти еще один слой индукции. Конечно, правильная формула для доказательства будет

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

Пока это тоже не помогло. Может кто-нибудь показать мне, как будет осуществляться индукция? Или ссылку на страницу с доказательством (я искал, ничего не нашел).

Answer 1

Проверенная машиной версия пэда в 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

Answer 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.

Answer 3

Я полагаю, что ваше доказательство будет легче распознать с помощью Сильная индукция :

... на втором шаге мы можем предположить не только, что утверждение верно для n = m, но также, что оно верно для всех n, меньших или равных m.

Вы застряли здесь:

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

.. частично, потому что вам нужно выполнить оба шага от k+1 до k, но также и k+1 до k-1.

Извините, это не более убедительно, прошло уже лет с тех пор, как я сделал реальные доказательства.

Answer 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

Кстати, если вы заинтересованы в такого рода вещах, я предлагаю вам проверить бесплатную книгу Бенджамина Пирса "Основы программного обеспечения".Это учебник для курса по языкам программирования, который использует Coq Proof Assistant.Coq похож на уродливый, злой и более мощный Haskell, который позволяет вам доказать свойства ваших функций.Это достаточно хорошо, чтобы заняться реальной математикой (доказать теорему о четырех цветах), но наиболее естественным для нее является проверенные правильные функциональные программы.Мне приятно, когда компьютер проверяет мою работу.И все функции в Coq всего ...

Answer 5

Иногда хорошая идея не начинать слишком формально. Я думаю, как только вы увидите, что хвостовая рекурсивная версия просто пропускает F (n-2) и F (n-1), чтобы избежать пересчета на каждом шаге, это дает вам проверочную идею, которую вы затем формализуете.