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 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 spousty i bez VS vzdělání, od skutečného a mnohem lépe placeného IT experta, c 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, potřebné úrovně formality a diskuze konstruktivnosti důkazů. * Správný formální zápis postupu - algoritmu, ve světle matematických formalismů. Petr Hliněný, Fl MU Brno, 2011 1/16 Fl: IB000: Základní formalismy :f—;- 1.1 Uvod 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, c • Uvažme matematickou větu (neboli tvrzení) tvaru „Jestliže platí předpoklady, pak platí závěr", c • Důkaz této věty je konečná posloupnost tvrzení, kde každé tvrzení je bud' - 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, c 0 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 jen celou problematiku uvedeme názornými příklady. Petr Hliněný, Fl MU Brno, 2011 2/16 Fl: IB000: Základní formalismy 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 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. c 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 = 21 + 1, l celé předpoklade 3) X = a + b = 2k + 2l + l + l 1,2) a komutativita sčítání (axiom)c 4) X = 2{k + l) + 2-l 3) a distributivnost násobenie 5) X = 2{k + l + l) 4) a opět distributivnost násobenie 6) X = 2m, m celé 5)am = fc + Z + lje celé číslo (axiom) □ Petr Hliněný, Fl MU Brno, 2011 3/16 Fl: IB000: Základní formalismy 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 které platí x < z < y. Důkaz po krocích (s již trochu méně formálním zápisem) zní: 1) Nechť z = ^ =x+'^ =y-y^. 2) Číslo zje racionální, neboť x a y jsou racionální. 3) Platí z > x, neboť ^ > 0. 4) Dále platí z < y, neboť opět ^ > 0. 5) Celkem x < z < y. □ Poznámka. Alternativní formulace Věty z Příkladu 1.3 mohou znít: - Pro každé x, y G (Q, kde x < y, existuje z e (Q takové, že x < z < y. - Množina racionálních čísel je hustá. Petr Hliněný, Fl MU Brno, 2011 4/16 Fl: IB000: Základni formalismy 1.2 Význam matematických vět • První krok formálního důkazu je uvědomit si, co říká věta, která se má dokázat; tedy co je předpoklad a co závěr dokazovaného tvrzení. Pravdivost takového tvrzení pak je třeba 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ávěr tvrzení.^ • Příklady běžné formulace matematických vět: * Konečná množina má konečně mnoho podmnožin.c * sin2(a) +cos2(a) = l.c * Graf je rovinný, jestliže neobsahuje podrozdělení nebo K^^.t. • Co přesně nám uvedené matematické věty říkají? Často pomůže pouhé rozepsání definic pojmů, které se v dané větě vyskytují. • Všimněte si také, jaký je správný logický význam matematického tvrzení vysloveného touto formou implikace („jestliže ... , pak .. . "). Především, pokud předpoklady nejsou splněny nebo jsou sporné, tak celé tvrzení je platné bez ohledu na pravdivost závěru! Petr Hliněný, Fl MU Brno, 2011 5/16 Fl: IB000: Základní formalismy O pravdivosti implikace Příklad 1.4. Je pravdivé následující matematické tvrzení? Věta. Mějme dvě 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 obě kuličky ve skutečnosti zelené, c „ To přece 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 obě zelené? To je celé nějaká blbost... "c Ano, výše uvedené jsou typické laické reakce na uvedenou větu. Přesto však tato věta pravdivá je! Stačí se vrátit o kousek výše ke kritériu - Pro každou situaci, ve které jsou splněny všechny předpoklady, je platný i závěr tvrzení - které je zjevně naplněno. Nenaleznete totiž situaci, ve které by byly splněny oba předpoklady zároveň, a tudíž ve všech takových neexistujících situacích si můžete říkat cokoliv, třeba že kuličky jsou zelené. □ Petr Hliněný, Fl MU Brno, 2011 6/16 Fl: IB000: Základní formalismy Příklad 1.5. Anna a Klára přišly na přednášku a usadily se do lavic. Proč je pravdivé toto matematické tvrzení? Věta. Jestliže Anna sedí v první řadě lavic a zároveň Anna sedí v poslední řadě lavic, tak Klára nesedí v druhé řadě lavic, c Opět je třeba se hluboce zamyslet nad významem předpokladů a závěru, ale tentkrát není situace předpokladů tak triviálně sporná, jako v Příkladu 1.4. Kdy tedy nastávají oba předpoklady zároveň? Když první řada lavic je zároveň řadou poslední! Neboli posluchárna má jen (nejvýše) jednu řadu lavic a Klára tudíž v druhé řadě nemůže sedět. Důkaz je hotov. □ Petr Hliněný, Fl MU Brno, 2011 7/16 Fl: IB000: Základní formalismy 1.3 Struktura matematických vět a důkazů Jak „moc formální" mají správné matematické 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, c A jak na ten správný matematický důkaz máme přijít? • No. .., nnalézání matematických důkazů je tvůrčí činnost, která není vůbec snadná a vyžaduje od vás přímo „umělecké" vlohy. Přesto se jí alespoň trochu musíte přiučit. Petr Hliněný, Fl MU Brno, 2011 8/16 Fl: IB000: Základní formalismy Dokazovat či vyvracet tvrzení? Představme si, že našim úkolem je rozhodnout platnost matematického tvrzení. Jak matematicky správně zdůvodníme svou odpověď? • Záleží na odpovědi samotné. .. c • Pokud je to ANO, prostě podáme důkaz tvrzení podle uvedených zvyklostí. • Pokud je odpověď NE, tak naopak podáme důkaz negace daného tvrzeníx Poměrně častým případem pak je matematická věta T, která tvrdí nějaký závěr pro širokou oblast vstupních možností. Potom platí následující::: • Pokud T je pravdivá, nezbývá než podat vyčerpávající důkaz platnosti pro všechny vstupyx • Avšak pokud T je nepravdivá, stačí „uhodnout" vhodný vstupní protipříklad a jen pro něj dokázat, že závěr tvrzení není platný. Petr Hliněný, Fl MU Brno, 2011 9/16 Fl: IB000: Základní formalismy Příklad 1.6. Rozhodněte platnost následujícího tvrzení: Pro všechna reálná x platí x2 + 3x + 2 > O.c Důkaz: Standardními algebraickými postupy si můžeme upravit vztah na x2 + 3x + 2 = {x + 1) • {x + 2) > 0. Co nám z něj vyplývá? Například to, že k porušení daného tvrzení stačí volit x tak, aby jedna ze závorek byla kladná a druhá záporná. To nastane třeba pro x = —|. c Pro vyvrácení tvrzení nám tedy stačí začít volbou protipříkladu x = — | (není nutno zdůvodňovat, jak jsme jej „uhodli"!) a následně dokázat úpravou x2+3x + 2 = {x + 1).{x + 2) = (_3 + 1).(_3+2) = (-!).(+!) = -\<0.n Dané tvrzení není platné. a Petr Hliněný, Fl MU Brno, 2011 10/16 Fl: 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.3 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, c Příklad 1.7. čistě existenčního důkazu. Věta. Existuje program, který vypíše na obrazovku čísla tažená ve 45. tahu sportky v roce 2011.c Důkaz: Existuje pouze konečně mnoho možných výsledků losování 45. tahu sportky v roce 2011. Pro každý možný výsledek existuje program, který tento daný výsledek výpise na obrazovku. Mezi těmito programy je tedy jistě ten, který vypíše právě ten výsledek, který bude ve 45. tahu sportky v roce 2011 skutečně vylosován, c a To je ale „podvod", že? nA přece není... Formálně správně to je prostě tak a tečka. Petr Hliněný, Fl MU Brno, 2011 11/16 Fl: 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í, c 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.8. „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á, c 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í |.) Pravděpodobnost, že zvolených n bodů vyjde jednobarevných, je jen ^ — 21~™. c Pro n2 podmnožin tak je pravděpodobnost, že některá z nich vyjde jednobarevná, shora ohraničená součtem TI 21-™ + ... + 21-™ =--->0. ---' 2™-1 n2 Jelikož je toto číslo (pravděpodobnost) pro n > 7 menší než 1, bude existovat obarvení bez jednobarevných zvolených podmnožin. r- Petr Hliněný, Fl MU Brno, 2011 12/16 Fl: IB000: Základní formalismy 1.4 Formální popis algoritmu Nakonec si položme 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. c Konvence 1.9. Zjednodušeně zde algoritmem rozumíme konečnou posloupnost elementárních výpočetních kroků, ve které každý další krok vhodně využívá (neboli závisí na) vstupní údaje či hodnoty vypočtené v předchozích krocích. Tuto závislost přitom pojímáme zcela obecně nejen na operandy, ale i na vykonávané instrukce v krocích. Pro zápis algoritmu a jeho zpřehlednění a zkrácení využíváme řídící konstrukce - podmíněná větvení a cykly, c Vidíte, jak blízké si jsou konstruktivní matematické důkazy a algoritmy v našem pojetí? Jedná se nakonec o jeden ze záměrů našeho přístupu.. . Petr Hliněný, Fl MU Brno, 2011 13/16 Fl: IB000: Základní formalismy Příklad algoritmického zápisu Příklad 1.10. Zápis algoritmu pro výpočet průměru z daného pole a[] s n prvky, • Inicializujeme sum <— 0 ; • postupně pro ±=0,1,2, . . . ,n-l provedeme * sum <— sum+a[i] ; • vypíšeme podíl (sum/n) . ^ Ve „vyšší úrovni" formálnosti se totéž dá zapsat jako: Algoritmus 1.11. Průměr z daného pole a [] s n prvky sum <— 0; foreach i<—0,1,2,...,n-l do sum <— sum+a[i] ; done res sum/n; output res; Petr Hliněný, Fl MU Brno, 2011 14/16 Fl: IB000: Základní formalismy Symbolický zápis algoritmů Značení. Pro potřeby symbolického formálního zápisu algoritmu v předmětu Fl: IB000 si zavedeme následovnou konvenci: • Proměnné nebudeme deklarovat ani typovat, pole odlišíme závorkami p []. • Prirazení 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, c • 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 f i). • Pevný cyklus uvedeme klíčovými slovy foreach ... do ... done, kde část za foreach 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, c • V zápise používáme jasné odsazování (zleva) podle úrovně zanoření řídících struktur (což jsou if, foreach, 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ý, Fl MU Brno, 2011 15/16 Fl: 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ů?__ zcela formální běžná úroveň matematika formální rozepsání všech elem. kroků (Příklad 1.2) strukturovaný a matem, přesný text v běžném jazyce algoritmy rozepsání všech elem. kroků strukturovaný rozpis kroků (Algoritmus 1.11), i s využitím běžného jazyka ve výpočetním modelu programováni assembler / strojový kód (kde se s ním dnes běžně setkáte?) „vyšší" (strukturované) programovací jazyky, například Java 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.. . Petr Hliněný, Fl MU Brno, 2011 16/16 Fl: IB000: Základní formalismy