Petr Hliněný, FI MU Brno 1 FI: IB000: Základní formalismy
1 Základní formalismy: Důkaz a Algoritmus1 Základní formalismy: Důkaz a Algoritmus
Studium informatiky neznamená jen ,,naučit se nějaký programovací jazyk , nýbrž zahrnuje
celý soubor dalších relevantních předmětů, mezi nimiž najdeme i matematicko­
teoretické (formální) základy moderní informatiky.
Právě odborný nadhled nad celou informatikou včetně nezbytné formální teorie odliší
řadového ,,programátora , kterých jsou dnes mraky i bez VŠ vzdělání, od skutečného
(a mnohem lépe placeného) IT experta. 2
Stručný přehled lekce
* Pochopení formálního zápisu a významu matematických tvrzení (vět)
a jejich důkazů.
* Rozbor logické struktury matematických vět,
konstruktivnosti důkazů.
* Správný formální zápis postupu ­ algoritmu, ve světle matematických
formalismů.
Petr Hliněný, FI MU Brno 2 FI: IB000: Základní formalismy
1.1 Úvod do matematického dokazování1.1 Úvod do matematického dokazování
Matematika (a tudíž i teoretická informatika jako její součást) se vyznačuje
velmi přísnými formálními požadavky na korektnost argumentace. 2
* Uvažme matematickou větu (neboli tvrzení) tvaru
,,Jestliže platí předpoklady, pak platí závěr . 2
* Důkaz této věty je konečná posloupnost tvrzení, kde
 každé tvrzení je buď
­ předpoklad, nebo
­ obecně přijatá ,,pravda ­ axiom, nebo
­ plyne z předchozích a dříve dokázaných tvrzení podle nějakého ,,akceptovaného
logického principu ­ odvozovacího pravidla;
 poslední tvrzení je závěr. 2
O potřebné úrovni formality matematických důkazů a o běžných důkazových technikách
se dozvíme dále v této a příští lekci.. .
Nyní si prostě celou problematiku uvedeme názornými příklady.
Petr Hliněný, FI MU Brno 3 FI: IB000: Základní formalismy
Příklad 1.1. Uvažujme následující matematické tvrzení (které jistě už znáte).
Věta. Jestliže x je součtem dvou lichých čísel, pak x je sudé.
Poznámka pro připomenutí:
­ Sudé číslo je celé číslo dělitelné 2, tj. tvaru 2k.
­ Liché číslo je celé číslo nedělitelné 2, tj. tvaru 2k + 1. 2
Důkaz postupuje v následujících formálních krocích:
tvrzení zdůvodnění
1) a = 2k + 1, k celé předpoklad
2) b = 2l + 1, l celé předpoklad2
3) x = a + b = 2k + 2l + 1 + 1 1,2) a komutativita sčítání (axiom)
4) x = 2(k + l) + 2  1 3) a distributivnost násobení
5) x = 2(k + l + 1) 4) a opět distributivnost násobení
2
Petr Hliněný, FI MU Brno 4 FI: IB000: Základní formalismy
Příklad 1.2. Dokažte následující tvrzení:
Věta. Jestliže x a y jsou racionální čísla pro která platí x < y, pak existuje
racionální číslo z pro které platí x < z < y. 2
Důkaz po krocích (s již trochu méně formálním zápisem) zní:
* Nechť z = x+y
2 = x + y-x
2 = y - y-x
2 .
* Číslo z je racionální, neboť x a y jsou racionální.
* Platí z > x, neboť y-x
2 > 0.
* Dále platí z < y, opět neboť y-x
2 > 0.
* Celkem x < z < y. 2
2
Poznámka. Alternativní formulace Věty z Příkladu 1.2 mohou znít:
­ Pro každé x, y  É, kde x < y, existuje z  É takové, že x < z < y.
­ Množina racionálních čísel je hustá.
Petr Hliněný, FI MU Brno 5 FI: IB000: Základní formalismy
1.2 Struktura matematických vět a důkazů1.2 Struktura matematických vět a důkazů
* První krok formálního důkazu je uvědomit si, co se má dokázat, tedy co je
předpoklad a co závěr dokazovaného tvrzení. 2
* Příklady formulace matematických vět:
 Konečná množina má konečně mnoho podmnožin.2
 sin2
() + cos2() = 1.2
 Graf je rovinný jestliže neobsahuje podrozdělení K5 nebo K3,3.2
* Často pomůže pouhé rozepsání definic pojmů, které se v dané větě vyskytují.
2
* Jak ,,moc formální mají důkazy vlastně být?
 Záleží na tom, komu je důkaz určen -- ,,konzument musí být schopen
,,snadno ověřit korektnost každého tvrzení v důkazu a plně pochopit,
z čeho vyplývá.
 Je tedy hlavně na vás zvolit tu správnou úroveň formálnosti zápisu vět
i důkazů podle situace.
Petr Hliněný, FI MU Brno 6 FI: IB000: Základní formalismy
Konstruktivní a existenční důkazy
Z hlediska praktické využitelnosti je potřeba rozlišit tyto dvě kategorie důkazů
(třebaže z formálně­matematického pohledu mezi nimi kvalitativní rozdíl není).
* Důkaz Věty 1.2 je konstruktivní. Dokázali jsme nejen, že číslo z existuje,
ale podali jsme také návod, jak ho pro dané x a y sestrojit.
* Existenční důkaz je takový, kde se prokáže existence nějakého objektu bez
toho, aby byl podán návod na jeho konstrukci. 2
Příklad 1.3. čistě existenčního důkazu.
Věta. Existuje program, který vypíše na obrazovku čísla tažená v 45. tahu
sportky v roce 2007.2
Důkaz: Existuje pouze konečně mnoho možných výsledků losování 45. tahu
sportky v roce 2007. Pro každý možný výsledek existuje program, který tento
daný výsledek vypíše na obrazovku. Mezi těmito programy je tedy jistě ten,
který vypíše právě ten výsledek, který bude v 25. tahu sportky v roce 2007
skutečně vylosován. 2
2
To je ale ,,podvod , že? 2A přece není. . .
Formálně správně to je prostě tak a tečka.
Petr Hliněný, FI MU Brno 7 FI: IB000: Základní formalismy
Fakt. Pro informatické i další aplikované disciplíny je důležitá konstruktivnost
důkazů vět, které se zde objevují. 2
V matematice ale jsou mnohé příklady užitečných a nenahraditelných existenčních
důkazů, třeba tzv. pravděpodobnostní důkazy.
Příklad 1.4. ,,pravděpodobnostního existenčního důkazu.
Věta. Na dané množině bodů je zvoleno libovolně n2 podmnožin, každá
o n prvcích. Dokažte pro dostatečně velká n, že všechny body lze obarvit
dvěma barvami tak, aby žádná množina nebyla jednobarevná. 2
Důkaz: U každého bodu si ,,hodíme mincí a podle výsledku zvolíme barvu červeně
nebo modře. (Nezávislé volby s pravděpodobností 1
2 .) Pravděpodobnost, že zvolených
n bodů vyjde jednobarevných, je jen 2
2n = 21-n
.
Pro n2
podmnožin tak je pravděpodobnost, že některá z nich vyjde jednobarevná, shora
ohraničená součtem
21-n
+ . . . + 21-n
n2
=
n2
2n-1
 0 .
Jelikož je toto číslo (pravděpodobnost) pro n  7 menší než 1, bude existovat obarvení
bez jednobarevných zvolených podmnožin. 2
Petr Hliněný, FI MU Brno 8 FI: IB000: Základní formalismy
1.3 Formální popis algoritmu1.3 Formální popis algoritmu
Položme si otázku, co je vlastně algoritmus?
Poznámka: Za definici algoritmu je obecně přijímána tzv. Church­Turingova teze tvrdící,
že všechny algoritmy lze ,,simulovat na Turingově stroji. Jedná se sice o přesnou,
ale značně nepraktickou definici.
Mimo Turingova stroje existují i jiné matematické modely výpočtů, jako třeba stroj
RAM, který je abstrakcí skutečného strojového kódu. 2
Konvence 1.5. Zjednodušeně zde algoritmem rozumíme konečnou posloupnost
elementárních (výpočetních) kroků, ve které každý další krok využívá
vstupní údaje či hodnoty vypočtené v předchozích krocích.
Pro zpřehlednění a zkrácení zápisu algoritmu využíváme řídící konstrukce ­
podmíněná větvení a cykly.
2
Vidíte, jak blízké si jsou konstruktivní matematické důkazy a algoritmy (v našem pojetí)?
Petr Hliněný, FI MU Brno 9 FI: IB000: Základní formalismy
Příklad 1.6. Zápis algoritmu pro výpočet průměru z daného pole a[] s n prvky.
* Inicializujeme sum  0 ;
* postupně pro i=0,1,2,...,n-1 provedeme
 sum  sum+a[i];
* vypíšeme podíl (sum/n). 2
2
Ve ,,vyšší úrovni formálnosti (s jasnějším vyznačením řídících struktur algoritmu)
se totéž dá zapsat jako:
Algoritmus 1.7. Průměr
z daného pole a[] s n prvky.
sum  0;
for i  0,1,2,...,n-1 do
sum  sum+a[i];
done
res  sum/n;
output res;
Petr Hliněný, FI MU Brno 10 FI: IB000: Základní formalismy
Značení. Pro potřeby symbolického formálního popisu algoritmů v předmětu
FI: IB000 si zavedeme následovnou konvenci:
* Proměnné nebudeme deklarovat ani typovat, pole odlišíme závorkami p[].
* Přiřazení hodnoty zapisujeme a  b, případně a:=b, ale nikdy ne a=b.
* Jako elem. operace je možné použít jakékoliv aritmetické výrazy v běžném
matematickém zápise. Rozsahem a přesností čísel se zde nezabýváme. 2
* Podmíněné větvení uvedeme klíčovými slovy if ... then ... else
... fi , kde else větev lze vynechat (a někdy, na jednom řádku, i fi).
* Pevný cyklus uvedeme klíčovými slovy for ... do ... done , kde část
za for musí obsahovat předem danou množinu hodnot pro přiřazování do
řídící proměnné.
* Podmíněný cyklus uvedeme klíčovými slovy while ... do ... done .
Zde se může za while vyskytovat jakákoliv logická podmínka. 2
* V zápise používáme jasné odsazování (zleva) podle úrovně zanoření řídících
struktur (což jsou if, for, while).
* Pokud je to dostatečně jasné, elementární operace nebo podmínky můžeme
i ve formálním zápise popsat běžným jazykem.
Petr Hliněný, FI MU Brno 11 FI: IB000: Základní formalismy
Malé srovnání závěrem
Jak to tedy je s vhodnou a únosnou mírou formalizace u matematických důkazů
i u zápisu algoritmů? 2
zcela formální běžná úroveň
matematika formální rozepsání všech
elem. kroků (Příklad 1.1)
strukturovaný a matem.
přesný text v běžném jazyce
algoritmy rozepsání všech elem. kroků
ve výpočetním modelu
strukturovaný rozpis kroků
(Algoritmus 1.7), i s využitím
běžného jazyka
programování assembler / strojový kód
(kde se s ním dnes běžně se-
tkáte?)
,,vyšší (strukturované)
programovací jazyky,
například Java
2
Pochopitelně se ve všech třech bodech obvykle držíme druhého přístupu, tedy běžné
úrovně formality, pokud si specifické podmínky výslovně nevyžadují přístup nejvyšší
formality. . .