Haskell Hero

Na první pohled může vylekat její délka. Pro lepší porozumění se v prvních odstavcích snažím dojít k tomu, proč vlastně indukci potřebujeme. Od naivního postupu v první metodě až po indukci v metodě třetí. Koho tato motivační část nezajímá, může ji přeskočit a začít číst až odstavec Začínáme.

Zadání

Dokažte, že funkce fact

fact   ::  Int -> Integer
fact 0  =  1
fact n  =  n * fact (n - 1)

počítá faktoriál nezáporného čísla. Jinými slovy, že výraz fact n se vyhodnotí na n!.

První metoda

Dokázat korektnost definice funkce znamená ukázat, že funkce počítá, co má, pro každou vstupní hodnotu. Naivní přístup by tedy mohl vypadat následovně:

Chceme ukázat, že fact 0 ~>* 0!
fact 0 se podle první klauzule vyhodnotí na 1, což je 0!. Funkce fact je tedy korektně definována pro n = 0.
Chceme ukázat, že fact 1 ~>* 1!
fact 1 se vyhodnotí následovně:
```
fact 1 ~> 1 * fact 0 ~> 1 * 1 ~> 1
```
což je 1!. Funkce fact je tedy korektně definována pro n = 1.
Chceme ukázat, že fact 2 ~>* 2!
fact 2 se vyhodnotí následovně:
```
fact 2 ~> 2 * fact 1 ~> 2 * 1 * fact 0 ~> 2 * 1 * 1 ~>* 2
```
což je 2!. Funkce fact je tedy korektně definována pro n = 2.
Chceme ukázat, že fact 3 ~>* 3!
fact 3 se vyhodnotí následovně:
```
   fact 3
~> 3 * fact 2
~> 3 * 2 * fact 1
~> 3 * 2 * 1 * fact 0
~> 3 * 2 * 1 * 1
~>* 6
```
což je 3!. Funkce fact je tedy korektně definována pro n = 3.
Chceme ukázat, že fact 4 ~>* 4!
fact 4 se vyhodnotí následovně:
```
   fact 4
~> 4 * fact 3
~> 4 * 3 * fact 2
~> 4 * 3 * 2 * fact 1
~> 4 * 3 * 2 * 1 * fact 0
~> 4 * 3 * 2 * 1 * 1
~>* 24
```
což je 4!. Funkce fact je tedy korektně definována pro n = 4.
Chceme ukázat, že fact 5 ~>* 5!
...
...

Takto bychom mohli pokračovat do konce života a stejně by se našel nějaký šťoural, který by našel číslo, pro které jsme korektnost funkce nedokázali.

Druhá metoda

Musíme ukázat, že se fact n vyhodnotí na n!, to se nemění. Půjdeme na to ale trošku jinou cestou.

Dokazujeme, že fact 0 ~>* 0!
fact 0 se podle první klauzule vyhodnotí na 1, což je 0!. Funkce fact je tedy korektně definována pro n = 0.
Dokazujeme, že fact 1 ~>* 1!
fact 1 se vyhodnotí následovně:
```
fact 1 ~> 1 * fact 0
```
Podle předchozího pozorování víme, že se fact 0 vyhodnotí na 0!, tím pádem fact 1 ~> 1 * 0!, což je 1!. Funkce fact je tedy korektně definována pro n = 1.
Dokazujeme, že fact 2 ~>* 2!
fact 1 se vyhodnotí následovně:
```
fact 2 ~> 2 * fact 1
```
Podle předchozího pozorování víme, že se fact 1 vyhodnotí na 1!, tím pádem fact 2 ~> 2 * 1!, což je 2!. Funkce fact je tedy korektně definována pro n = 2.
Dokazujeme, že fact 3 ~>* 3!
fact 3 se vyhodnotí následovně:
```
fact 3 ~> 3 * fact 2
```
Podle předchozího pozorování víme, že se fact 2 vyhodnotí na 2!, tím pádem fact 3 ~> 3 * 2!, což je 3!. Funkce fact je tedy korektně definována pro n = 3.
Dokazujeme, že fact 4 ~>* 4!
fact 4 se vyhodnotí následovně:
```
fact 4 ~> 4 * fact 3
```
Podle předchozího pozorování víme, že se fact 3 vyhodnotí na 3!, tím pádem fact 4 ~> 4 * 3!, což je 4!. Funkce fact je tedy korektně definována pro n = 4.
Dokazujeme, že fact 5 ~>* 5!
...
...

Jak vidíme, už nám délka důkazu nenarůstá s rostoucím argumentem, ale stále bychom při této technice museli tento důkaz napsat pro všechna přirozená čísla včetně nuly.

Třetí metoda

V druhé metodě jsme ukázali následující:

funkce fact n je korektně definována pro n = 0
funkce fact n je korektně definována pro n = 1 za předpokladu, že je korektně definována pro n = 0
funkce fact n je korektně definována pro n = 2 za předpokladu, že je korektně definována pro n = 1
funkce fact n je korektně definována pro n = 3 za předpokladu, že je korektně definována pro n = 2
funkce fact n je korektně definována pro n = 4 za předpokladu, že je korektně definována pro n = 3
...

Protože se důkaz korektnosti funkce fact n dokazuje pomocí předpokladu, že funkce je korektní pro hodnotu o jedna menší, můžeme předchozí důkaz zobecnit pro každé přirozené číslo:

Dokážeme, že se fact 0vyhodnotí na 0!.
Dokážeme, že se fact (k + 1) vyhodnotí na (k + 1)! za předpokladu, že fact k se vyhodnotí na k!.

Pak, když za námi přijde nějaký nedůvěřivec a řekne:

"Ukaž mi, že fact 0 opravdu počítá 0! !"

A my mu na to řekneme:

"Tak se podívej, fact 0 ~> 1, což je 0! ."

Přímo jsme odpověděli na jeho otázku. Tím pádem mu nezbývá, než nám odpovědět:

"Dobrá, teď už ti věřím."

A bude s otázkami pokračovat:

Jak víš, že fact 1 počítá 1! ?
- Protože fact 1 ~> 1 * fact 0 a fact 0 ~>* 0! . Takže fact 1 ~>* 1 * 0! , což je 1! .
No jo, ale jak víš, že fact 0 počítá 0! ?
- To ti klidně ukážu: fact 0 ~> 1, což je 0! .
Dobrá, teď už ti věřím.

A bude pokračovat:

Jak víš, že fact 2 počítá 2! ?
- Protože fact 2 ~> 2 * fact 1 a fact 1 ~>* 1! . Takže fact 2 ~>* 2 * 1! , což je 2! .
No jo, ale jak víš, že fact 1 počítá 1! ?
- Protože fact 1 ~> 1 * fact 0 a fact 0 ~>* 0! . Takže fact 1 ~>* 1 * 0! , což je 1! .
No jo, ale jak víš, že fact 0 počítá 0! ?
- To ti klidně ukážu: fact 0 ~> 1 , což je 0! .
Dobrá, teď už ti věřím.

A bude pokračovat:

Jak víš, že fact 3 počítá 3! ?
- Protože fact 3 ~> 3 * fact 2 a fact 2 ~>* 2! . Takže fact 3 ~>* 3 * 2! , což je 3! .
No jo, ale jak víš, že fact 2 počítá 2! ?
- Protože fact 2 ~> 2 * fact 1 a fact 1 ~>* 1! . Takže fact 2 ~>* 2 * 1! , což je 2! .
No jo, ale jak víš, že fact 1 počítá 1! ?
- Protože fact 1 ~> 1 * fact 0 a fact 0 ~>* 0! . Takže fact 1 ~>* 1 * 0! , což je 1! .
No jo, ale jak víš, že fact 0 počítá 0! ?
- To ti klidně ukážu: fact 0 ~> 1 , což je 0! .
Dobrá, teď už ti věřím.

...
A bude pokračovat:
...

Jak víš, že fact 100 počítá 100! ?
- Protože fact 100 ~> 100 * fact 99 a fact 99 ~>* 99! . Takže fact 100 ~>* 100 * 99! , což je 100! .
No jo, ale jak víš, že fact 99 počítá 99! ?
- Protože fact 99 ~> 99 * fact 98 a fact 98 ~>* 98! . Takže fact 99 ~>* 99 * 98! , což je 99! .
...
No jo, ale jak víš, že fact 0 počítá 0! ?
- To ti klidně ukážu: fact 0 ~> 1, což je 0! .
Dobrá, teď už ti věřím.

Protože vidíme, že tvrzení můžeme v konečném čase pro libovolné přirozené číslo, můžeme tuto důkazovou techniku zahrnout do naší teorie a říkáme jí matematická indukce.

Začínáme

Jako první musíme zvolit, vůči čemu indukci povedeme. Jinými slovy, co bude prvkem, pro jehož libovolnou velikost máme korektnost funkce dokázat. V našem příkladě máme unární funkci fact n, takže je náš výběr jednoduchý – indukci povedeme vůči jejímu argumentu n.

Indukční báze

Nejprve přímo ukážeme, že funkce počítá to, co má, pro nejmenší hodnotu argumentu. V našem příkladě ukážeme, že funkce fact n je korektní pro n = 0, tedy že fact 0 se vyhodnotí na 0! .

fact 0 se podle první klauzule vyhodnotí na 1, což je 0! .

Můžeme tedy říct, že báze indukce platí.

Indukční předpoklad

Korektnost fact 0 máme dokázanou v bázi.
Korektnost fact 1 dokážeme pomocí předpokladu, že fact 0 počítá 0! .
Korektnost fact 2 dokážeme pomocí předpokladu, že fact 1 počítá 1! .
Korektnost fact 3 dokážeme pomocí předpokladu, že fact 2 počítá 2! .
...

A právě tento předpoklad musíme zapsat. Takový zápis by mohl vypadat následovně:

Předpokládejme, že funkce fact n je korektní pro nějaké kladné celé číslo k. Jinými slovy, že fact k se vyhodnotí na k! .

Indukční krok

Korektnost fact 0 máme dokázanou v bázi.
Korektnost fact 1 dokážeme pomocí předpokladu, že fact 0 počítá 0! .
Korektnost fact 2 dokážeme pomocí předpokladu, že fact 1 počítá 1! .
Korektnost fact 3 dokážeme pomocí předpokladu, že fact 2 počítá 2! .
...

Obecně chceme ukázat, že výraz fact (k + 1) se vyhodnotí na (k + 1)! pomocí předpokladu, že fact k se vyhodnotí na k! . Tak tedy dokazujme. Budeme postupně vyhodnocovat výraz fact (k + 1).

fact (k + 1)  ~>  (k + 1) * fact k

V tuto chvíli přichází na řadu indukční předpoklad. My totiž víme, že fact k se vyhodnotí na k! . Podle indukčního předpokladu tedy pokračujeme ve vyhodnocování.

~>  (k + 1) * k!

což je (k + 1)! .

Dokázali jsme tedy, že výraz fact (k + 1) se vyhodnotí na hodnotu (k + 1)! . Tímto je důkaz hotov.

Indukce na seznamech

Příklad

length       ::  [a] -> Int
length []     =  0
length (x:s)  =  1 + length s

Dokažte, že výraz length s se vyhodnotí na délku seznamu s.

Korektnost funkce fact n jsme dokazovali indukcí podle n. Indukce na seznamech se ve většině případů vede podle délky seznamu. I zde budeme korektnost funkce length s dokazovat podle délky seznamu s.

Indukční báze

Chceme ukázat, že funkce length je korektně definována pro nejmenší možný argument. V tomto případě pro prázdný seznam. Ukážeme tedy, že length [] se vyhodnotí na délku prázdného seznamu, což je nula.

length []  ~>  0

Báze tedy platí.

Indukční předpoklad

Předpokládejme tedy, že funkce je korektní pro všechny seznamy s, které mají délku k. To znamená, že length s se vyhodnotí na číslo k.

Indukční krok

U funkce fact jsme dokazovali, že je korektně definována pro nějaké k + 1. Zde bychom chtěli použít seznam, který je o jeden prvek delší než seznam s z indukčního předpokladu, který obsahuje k prvků. Přidejme tedy k seznamu s libovolný prvek x a dokazujme, že length (x:s) se vyhodnotí na k + 1.

length (x:s)  ~>  1 + length s

Podle indukčního předpokladu víme, že length s se vyhodnotí na k. Vyhodnocení bude podle indukčního předpokladu pokračovat následovně:

~>  1 + k

což jsme chtěli dokázat. Důkaz je u konce.

Poznámka

U prvního příkladu navíc předpokládáme, že argument funkce fact je pouze konečně velký. Stejně tak u druhého příkladu předpokládáme, že korektnost funkce length dokazujeme pro konečně dlouhý seznam.

<= Funkce nad Bool předchozí lekce následující lekce Vstup a výstup I =>