1   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 predmetu, mezi nimiž najdeme i matematicko-teoreticke (formalní) základy moderní informatiky.
Prave odborny nadhled nad celou informatikou vcetne nezbytne formalní teorie odliší radoveho „programatora", kterych jsou dnes spousty i bez VŠ vzdelaní, od skutecneho a mnohem lepe placeneho IT experta. c
Stručný přehled lekce
* Pochopení formálního zápisu a významu matematických tvrzení (vet) a jejich dUkazU.
* Rozbor logicke struktury matematických vet, potrebne Urovne formality a diskuze konstruktivnosti dukazu.
* Spravný formalní zapis postupu - algoritmu, ve svetle matematických formalismu.
1.1   Úvod do matematického dokazování
Matematika (a tudíž i teoretická informatika jako její součást) se vyznačuje velmi prísnymi formalními poZadavky na korektnost argumentace. c
• UvaZme matematickou vetu (neboli tvrzení) tvaru
„JestliZe platí předpoklady, pak platí zaver". c
• Důkaz teto vety je konečna posloupnost tvrzení, kde
* kazde tvrzení je bud'
- předpoklad, nebo
- obecne přijata „pravda" - axiom, nebo
- plyne z předchozích a drive dokazanych tvrzení podle nejakeho „ak-ceptovaneho" logickeho principu - odvozovacího pravidla;
* poslední tvrzení je záver. c
O potřebné urovni formality matematických dukazu a o beznych dukazovych technikach se dozvíme dale v teto a prístí lekci.. .
Nyní si proste celou problematiku uvedeme nazornymi príklady.
Petr Hliněný,  FI MU Brno__: IB000: Základní formalismy
r.
^
Příklad 1.2. 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 sude. Poznámka pro připomenut í:
- Sude číslo je cele číslo dělitelné 2, tj. tvaru 2k.
- Lichí číslo je cele číslo nedelitelne 2, tj. tvaru 2k + 1. c
Důkaz postupuje v následujících formálních krocích:
	tvrzení		zduvodnení
1)	a	= 2k + 1, k cele	predpoklad
2)	b	= 21 + 1, l cele	predpoklade
3)	x	= a + b = 2k + 21 + 1 + 1	1,2) a komutativita scítaní (axiom)c
4)	x	= 2(k + 1) +2 • 1	3) a distributivnost nasobeníc
5)	x	= 2(k +1 + 1)	4) a opet distributivnost nasoben íc
6)	x	= 2m, m cele	5) a m = k + 1 + 1 je cele c íslo (axiom)
□
Petr Hliněný,  FI MU Brno
Příklad 1.3. 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 ktere platí x < z < y. c
Důkaz po kroc ích (s již trochu méně formaln ím zápisem) zn í:
• Nechť z = ^=x + ^=y-^f.
• C íslo z je racionáln í, nebol! x á y jsou racionáln í.
• Platí z > x, neboť ^ > 0.
• Dále platí z < y, opět neboť       > 0.
• Celkem x < z < y. c
Poznámka. Alternativn í formulace Vety z Príkladu 1.3 mohou zn ít:
- Pro kázde x,y G Q, kde x < y, existuje z G Q tákove, ze x < z <y.
- Mnozina racionáln ích c ísel je hustá.
□
Petr Hliněný,  FI MU Brno
FI: IB000: Základní formalismy
1.2   Význam matematických vět
• První krok formálního důkazu je uvědomit si, co říká veta, která se má dokázat; tedy co je předpoklad a co závěr dokazovaneho tvrzení. Pravdivost takoveho tvrzení pak je treba chápat v následujácím významu:
Pro každou situaci, ve která jsou splněny všechny předpoklady, je platná i záver tvrzení.
• Příklady bezne formulace matematických vet:
* Konecna mnozina ma konecne mnoho podmnozin.c
* sin2(a) +cos2(a) = 1.c
* Graf je rovinný jestlize neobsahuje podrozdelení K5 nebo K3;3.c
• Casto pomuze pouhe rozepsaní definic pojmu, ktere se v dane vete výskytu^'.
• Vsimnete si take, jaká je správny logická váznam matematickeho tvrzení vysloveneho touto formou implikace (jestlize .. ., pak ..."). Predevsím, pokud predpoklady nejsou splneny nebo jsou sporne, tak cele tvrzení je platne bez ohledu na pravdivost záveru!
Petr Hliněný,  FI MU Brno_5_FI: IB000: Základní formalismy
Příklad 1.4. Je pravdivé následující matematické tvrzení?
Věta. Mejme dve kuličky, Červenou a modrou. Jestliže Červené kulička je těžší než modré a zároveň je modré kulička těžší než ta červené, tak jsou obe kuličky ve skutečnosti želené. c
„To prece nemůže být pravda, jak může být jedna kulička těžší než druhá a naopak zároveň? Jak mohou být nakonec obe želene? To je nejaká blbost..."
Ano, výše uvedene jsou týpicke laicke reakce na uvedenou vetu. Pňesto však tato veta pravdivý je!
Stací se vrátit o kousek výše ke kriteriu - Pro každou situaci, ve ktere jsou splnený vsechný pňedpokladý, je platný i žáver tvržení- ktere je žjevne naplneno. Nenaležnete totiž situaci, ve ktere bý býlý splnený oba predpokladý žaroveň, a tudíž ve vsech takových neexistujících situacích si mužete ňíkat cokoliv, treba že kulický jsou želene. □
1.3   Struktura matematických vět a důkazů
Jak „moc formální" mají správné matematické důkazy vlastně být?
• ZáleZí na tom, komů je důkaz ůrCen — „konzument" můsí byt schopen „snadno" oveřit korektnost kaZdeho tvrzení v důkazů a plne pochopit, z Ceho vyplývá.
• Je tedy hlavne na vás zvolit tů správnoů ároveř formálnosti zápisů vet i důkazů podle sitůace. □
A jak na správny matematická důkaz mohů přijít?
• No..., □nalezání matematických důkazů je tvůrci cinnost, která není vůbec snadná a vyzadůje od vás prímo „ůmelecke" vlohy. Přesto se jí alespoř trochů můsíte naůát.
r.
Konstruktivní a existenční důkazy
Z hlediska praktické využitelnosti je potreba rozlišit tyto dve kategorie důkazů (třebaže z formálně-matematického pohledu mezi nimi kvalitativní rozdíl není).
• Důkaz Vety 1.3 je konstruktivní. Dokázali jsme nejen, ze Číslo z existuje, ale podali jsme take návod, jak ho pro dane x a y sestrojit.
• Existenční důkaz je takovy, kde se prokáze existence nejakeho objektu bez toho, aby byl podán návod na jeho konstrukci. c
Príklad 1.5. čiste existenčního důkazu.
Veta. Existuje program, který vypíse na obrazovku čísla tažená ve 45. tahu
sportky v roce 2010.c Důkaz: Existuje pouze konecne mnoho mozných výsledku losováná 45. tahu sportky v roce 2010. Pro kazdá mozná vásledek existuje program, která tento dany výsledek vypíše na obrazovku. Mezi temito programy je tedy jiste ten, ktery vypíše prave ten vysledek, ktery bude ve 45. tahu sportky v roce 2010
skutecne vylosovan. c
□
To je ale „podvod", že? nA prece není.. . Formálne správne to je proste tak a teCka.
Petr Hlinený,  FI MU Brno_
Fakt. Pro informaticke i dalsí aplikovane disciplíny je duleZita konstruktivnost dukazu vet, ktere se zde objevují. c
V matematice ale jsou mnohe příklady uzitecnych a nenahraditelných exis-tencních dukazu, třeba tzv. pravdepodobnostná dukazý.
Příklad 1.6. „pravdepodobnostního" existenčního dukazu.
Věta. Na dane množine bodu je zvoleno libovolne n 2 podmnožin, každé o n prvcích. Dokazte pro dostatečné velká n, če vsechný bodý lze obarvit dvema barvami tak, abý zádna mnozina nebýla jednobarevná. c
Důkaz: U kazdeho bodu si „hodíme mincí" a podle výsledku zvolíme barvu cervene nebo modře. (Nezávislé volby s pravděpodobností ^.) Pravděpodobnost, že zvolených n bodů vyjde jednobarevných, je jen ^ = 21~™.
Pro n2 podmnozin tak je pravdepodobnost, ze nekterí z nich vyjde jednobarevna, shora ohranicenía souctem
2
21-" + --- + 21-" = ~^—r -►(). n2
Jelikoz je toto císlo (pravdepodobnost) pro n > 7 mensí nez 1, bude existovat obarvení bez jednobarevnych zvolenych podmnozin. □
Petr Hliněný,  FI MU Brno___IB000: Zýkladní formalismy
1.4   Fořmainí popis algoritmu
Položme si otažku, co je vlastne algoritmus?
Poznámka: Za definici algoritmu je obecne prijímana tžv. Churčh-Turingova teže tvrd ící, že vsechný algoritmý lže „simulovat" na Turingove stroji. Jedna se sice o presnou, ale žnacne nepraktickou definici.
Mimo Turingova stroje existuj í i jine matematičke modely výpočtů, jako treba stroj RAM, který je abstrakc í skutecneho strojového kodu. c
Konvěncě 1.7. Zjednodusene žde algoritmem rožum íme konecnou posloupnost elementarn ích výpocetn ích kroku, ve ktere každý dalsí krok vhodne výuž íva (neboli žavisí na) vstupn í udaje ci hodnotý výpoctene v pňedchož ích krocích. Tuto žavislost pňitom poj ímame žcela obecne nejen na operandý, ale i na výkonavane instrukce v krocích.
Pro žapis algoritmu a jeho žprehlednen í a žkracen í výuž ívame řidiči konstrukče - podm ínena vetven í a cýklý. c
Vid íte, jak bl ížke si jsou konstruktivn í matematicke dukažý a algoritmý v nasem pojet í? Jedna se nakonec o jeden že žameru naseho prístupu...
Petr Hliněný,  FI MU Brno__: IB000: Základní formalismy
Příklad 1.8. Zápis algoritmu pro výpočet průměru z daního pole a[] s n prvky.
• Inicializujeme sum — 0 ;
• postupne pro i=0,1,2, ...,n-1 provedeme
* sum —sum+a[i];
• vypíšeme podíl (sum/n) . □ G
Ve „vyssí urovni" formalnosti (s jasnejsím vyznacením řídících struktur algoritmu) se totez da zapsat jako:
Algoritmus 1.9. Přůméř
z daneho pole a[] s n prvky.
sum — 0;
foreach   i — 0,1,2,...,n-1 do sum — sum+a[i];
done
res — sum/n; output res;
Petr Hliněný,  FI MU Brno
Značení. Pro potřeby symbolického formáln ího zápisu algoritmů v předmětu Fl: IB000 si zavedeme následovnou konvenci:
• Proměnné nebudeme deklarovat ani typovat, pole odliSíme závorkami p [].
• Přiřazeni hodnoty zapisujeme a — b, připadne a := b, ale nikdy ne a=b.
• Jako elem. operace je moZne pouZ ít jakekoliv aritmetické výrazy v beZnem matematickem zapise. Rozsahem a presnost í C ísel se zde nezabývame. c
• Podm ínene větveni uvedeme kl iCovymi slovy if ... then . . . else ... fi, kde else vetev lze vynechat (a nekdy, na jednom řadku, i fi).
• Pevny cyklus uvedeme kl icovymi slovy foreach ... do ... done, kde cast za foreach musí obsahovat predem danou mnozinu hodnot pro přirazovan í do ríd íc í promenne.
• Podmíněný cyklus uvedeme kl icovymi slovy while ... do ... done. Zde se muze za while vyskytovat jakakoliv logicka podm ínka. c
• V zapise pouz ívame jasne odsazovan i (zleva) podle urovne zanoren í ríd íc ích struktur (coz jsou if, foreach, while).
• Pokud je to dostateřcnře jasne, elementarn i operace nebo podm inky muzeme i ve formaln ím zapise popsat beznym jazykem.
Petr Hliněný,  FI MU Brno
Malé srovnání závěrem
Jak to tedy je s vhodnou a únosnou mírou formalizace u matematických důkazů
	zcela formální	běžná úroveň
matematika algoritmy programování	formální   rozepsání všech elem. kroků (Příklad 1.2) rozepsání všech elem. kroků ve výpočetním modelu assembler / strojový kód (kde se s ním dnes běžně setkáte?)	strukturovaný a matem, přesný text v běžném jazyce strukturovaný rozpis kroků (Algoritmus 1.9), i s využitím běžného jazyka „vyšší" (strukturované) programovací jazyky, například Java
Pochopitelne se ve vsech trech bodech obvykle drzíme drůheho prístůpů, tedy bezne ůrovne formality, pokůd si specificke podmínky vyslovne nevyzadůjí prístůp nejvyssí formality. ..
^----Petr Hliněný,  FI MU Brno_13_