■r 11 Formalizace a důkazy pro algoritmy Je faktem, že situace, kdy programátorem zapsaný kód ve skutečnosti počítá něco trochu jiného, než si autor představuje, je snad nejčastější programátorskou chybou -o to zákeřnější, že ji žádný „chytrý" překladač nemůže odhalit. Proto již na počátku studia informatiky je žádoucí klást důraz na správné chápání zápisu algoritmů i na přesné důkazy jejich vlastností a správnosti. <š> Stručný přehled lekce Jednoduchá formalizace pojmu algoritmus. Jak dokazovat vlastnosti a správnost algoritmů. Indukce při dokazování algoritmů. Petr Hliněný, Fl MU Brno, 2020 1/24 Fl: IB000: Důkazy pro algoritmy 11.1 Formální popis algoritmu Před samotným závěrem kurzu si položme otázku, co je vlastně algoritmus? Poznámka: Za definici algoritmu je obecně přijímána tzv. Ch u rch-Tu ringová teze tvrdící, že všechny algoritmy lze „simulovat" na Turingově stroji. Jedná se sice o přesnou, ale značně nepraktickou definici. Mimo Tu ringová stroje existují i jiné matematické modely výpočtů, jako třeba stroj RAM, který je abstrakcí skutečného strojového kódu, nebo neprocedurální modely. Konvence 11.1. 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. 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, 2020 2/24 Fl: IB000: Důkazy pro algoritmy Ukázka algoritmického zápisu Příklad 11.2. Zápis algoritmu pro výpočet průměru daného pole a[] s n prvky. • Inicializujeme sum ^— 0 ; • postupně pro i=0,l,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 11.3. Průměr z daného pole a[] s n prvky. input pole a [] délky n > 1; 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, 2020 3/24 Fl: IB000: Důkazy pro algoritmy Symbolický zápis algoritmů Značení. Pro potřeby symbolického formálního zápisu algoritmů v předmětu Fl: IB000 si zavedeme následující pravidla: • Proměnné nebudeme deklarovat ani typovat, pole odlišíme závorkami p []. • Prirazení hod noty 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 y běžném matematickém zápise. Rozsahem a přesností čísel se zde nezabýváme. • Podmíněné větvení uvedeme klíčovými slovy if ... then . . . else ... f i , kde else větev lze vynechat (a někdy, na jednom řádku, i f i). • Pevný cyklus uvedeme klíčovými slovy f oreach ... do ... done, kde část za f oreach 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. • V zápise používáme jasné odsazování (zleva) podle úrovně zanoření řídících struktur (což jsou if, f oreach, 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, 2020 4/24 Fl: IB000: Důkazy pro algoritmy Co počítá následující algoritmus? Příklad 11.4. Je dán následující symbolicky zapsaný algoritmus. Co je jeho výstupem v závislosti na vstupech a, b? Algoritmus 11.5. input a, b; res ^— 7; foreach i 1,2, . . . ,b-l,b do res ^— res + a+2-b + 8; done output res . □ Vypočítáme hodnoty výsledku res v počátečních iteracích cyklu: 6 = 0: res — 7, 6 = 1: res = 7 + a + 26 + 8, 6 = 2: res = 7 + (a + 26 + 8) + (a + 26 + 8), .. . □ Co dále? Výčet hodnot naznačuje pravidelnost a závěr, že obecný výsledek po 6 iteracích cyklu bude mít hodnotu res = 7 + 6(a + 26 + 8) = ab + 262 + 86 + 7. □ Petr Hliněný, Fl MU Brno, 2020 5/24 Fl: IB000: Důkazy pro algoritmy 11.2 O „správnosti" a dokazování programů Jak se máme přesvědčit, zeje daný program počítá „správně"?c • Co třeba ladění programů? Jelikož počet možných vstupních hodnot je (v principu) neohraničený, nelze otestovat všechna možná vstupní data.c • Situace je zvláště komplikovaná v případě paralelních, randomizovaných, interaktivních a nekončících programů (operační systémy, systémy řízení provozu apod.). Takové systémy mají nedeterministické chování a opakované experimenty vedou k různým výsledkům. Nelze je tudíž ani rozumně ladit... t • V některých případech je však třeba mít naprostou jistotu, že program funguje tak jak má, případně že splňuje základní bezpečnostní požadavky.c * Pro „malé" algoritmy je možné podat přesný matematický důkazn. * Narůstající složitosti programových systémů si pak vynucují vývoj jiných „spolehlivých" formálních verifikačních metod. Mimochodem, co to vlastně znamená „počítat správně"? Petr Hliněný, Fl MU Brno, 2020 6/24 Fl: IB000: Důkazy pro algoritmy Ukázka formálního důkazu algoritmu Příklad 11.6. Je dán následující symbolicky zapsaný algoritmus. Dokažte, že jeho výsledkem je „ výměna " vstupních hodnot a,b. Algoritmus 11.7. input a, b; a i- a+b; b i- a-b; a ^— a-b; output a, b . Pro správný formální důkaz si musíme nejprve uvědomit, zeje třeba symbolicky odlišit od sebe proměnné a,b od jejich daných vstupních hodnot, třeba ha,h%. Nyní v krocích algoritmu počítáme hodnoty proměnných: * a = ha, b = hb, * a ^— a + b = ha + h0, b = h0, * a = ha + hb, b <- a - b = ha + hb - hb = ha, □ * a^a-b = ha + hb- ha = h, b = ha, Tímto jsme s důkazem hotovi. □ Petr Hliněný, Fl MU Brno, 2020 7/24 Fl: IB000: Důkazy pro algoritmy 11*3 Rekurzivní algoritmy * Rekurentní vztahy posloupností, stručně uvedené v Oddíle 5.1, mají svou přirozenou obdobu v rekurzivně zapsaných algoritmech. * Zjednodušeně řečeno to jsou algoritmy, které se v průběhu výpočtu odvolávají na výsledky sebe sama pro jiné (menší) vstupní hodnoty. * U takových algoritmů je zvláště důležité kontrolovat jejich správnost a také praktickou proveditelnost (časovou i paměťovou). Příklad 11.8. Symbolický zápis jednoduchého rekurzivního algoritmu. Algoritmus . function faktorial(x ) : if x < 1 then t <- 1; else t ^— x • faktorial(x-1); return t . Co je výsledkem výpočtu? Jednoduše řečeno, výsledkem je faktoriál nota x\ = x • (x — 1).....2-1. vstupní přirozené hodnoty x, tj. hod- □ Petr Hliněný, Fl MU Brno, 2020 8/24 Fl: IB000: Důkazy pro algoritmy Fibonacciho čísla Pro jiný příklad rekurze se vrátíme k Oddílu 5.1, kde byla zmíněna známá Fibonacciho posloupnost 1,1,2,3,5,8,13,21,34,55,89,144,.... Nyní tuto posloupnost budeme uvažovat již od jejího nultého členu, tj. jako 0,1,1,2,3,5,8,13,21,34,55,... . □ Algoritmus 11.9. Rekurzivní výpočet členů Fibonacciho posloupnosti. Pro dané přirozené x > 0 vypočítáme x-té Fibonacciho číslo následovně: function fibonacci(x ) : if x < 2 then t <— x; else t ^— fibonacci(x-1)+fibonacci(x-2); return t . Správnost Algoritmu 11.9 je víceméně zřejmá z jeho přímé podoby s rekurentním vzorcem v definici Fibonacciho čísel. Algoritmus 11.9 tudíž lze prohlásit za definiční, čili referenční implementaci výpočtu Fibonacciho čísel. Zamyslete se však, jak je to s praktickou „proveditelností" takového algoritmu... Co třeba fibonacci(40) nebo /ibonacci(50)? Petr Hliněný, Fl MU Brno, 2020 9/24 Fl: IB000: Důkazy pro algoritmy ■r Příklad 11.10. Nerekurzivní algoritmus pro Fibonacciho čísla. Dokazte, že následující algoritmus pro každé přirozené n počítá tutéž hodnotu jako rekurentní funkce f ibonacci (n) v Algoritmu 11.9. Algoritmus . input n; b[0] ^0; b[l] <- 1; foreach i 2,3, . . . ,n do b [i] 1 v ind. kroku předpokládáme platnost našeho indukčního předpokladu b[j] = fibonacci(j) pro j £ {i, i — 1}. * V (i + l)-ní iteraci cyklu pak nastane 6[z+l] ^— b[i]+b[i—1] = /ibonacci (i)+fibonacci (i—1) = fibonacci(i+l), což je přesně podle rekurentní definice z Algoritmu 11.9. □ Petr Hliněný, Fl MU Brno, 2020 10/24 Fl: IB000: Důkazy pro algoritmy 11.4 Techniky důkazu indukcí • Doposud zde byla matematická indukce obvykle představována ve své přímočaré formě, kdy dokazované tvrzení ihned nabízelo celočíselný parametr, podle nějž bylo potřebné indukci vést. • Indukční krok pak prostě zpracoval přechod „n = i ^ n = i + 1". • To však u dokazování správnosti algoritmů často neplatia našim cílem zde je ukázat různé možné techniky, jak správně indukci na dokazování algoritmů aplikovat. □ • Uvidíme, jak si z nabízejících se parametrů správně vybrat a jak je případně kombinovat. Petr Hliněný, Fl MU Brno, 2020 11/24 Fl: IB000: Důkazy pro algoritmy Technika fixace parametru Příklad 11.11. Mějme následující algoritmus. Co je jeho výsledkem výpočtu? Algoritmus . function soucin(x,y ) : if x < 0 then t <- 0; else t ^— soucin(x-l,y) + y; return t . Sledováním průběhu rekurze v algoritmu zjistíme, že hloubka zanoření volání funkce součin bude rovna nezáporné (horní celé) části x. Jelikož každé zanoření poté k výsledku přičte hodnotu y, odhadneme: Věta. Pro každé x,y £ N Algoritmus 11.11 vrátí hodnotu t = x • y. Jaký je vhodný postup k důkazu tohoto tvrzení indukcí? Je snadno vidět, že na hodnotě vstupu y vlastně nijak podstatně nezáleží (lze y fixovat) a důležité je sledovat x. Tato úvaha nás dovede k následujícímu: Petr Hliněný, Fl MU Brno, 2020 12/24 Fl: IB000: Důkazy pro algoritmy function soucin(x,y ) : if x < 0 then t <- 0; else t ^— soucin(x-l,y) + y; Důkaz: Budiž y G N libovolné ale pro další úvahy pevné. Dokazujeme tady, že pro každý vstup x:=iGN volání funkce soucin(x,y) navrátí hodnotu i • y. • V bázi pro x — i — 0 provedeme první větev podmínky, tj. t 0 = 0 • yx • Indukční krok. Nechť je tvrzení známo pro x = i G N a uvažujme další vstup x := i + 1 > 0. V tom případě se vykonává druhá větev podmínky, čili t ^— soucin(x — 1, y) + y. Všimněte si, že platí x — 1 — i. Podle indukčního předpokladu již víme, že návratovou hodnotu volání funkce soucin(i, y) je i • y. nZbývá jen uvedené poznatky správně zřetězit t <- soucin(x - 1, y) + y = soucin(i, y)+y = i-y + y= (i + l)y = x-y . Důkaz matematickou indukcí je tímto zdárně ukončen. i-| Petr Hliněný, Fl MU Brno, 2020 13/24 Fl: IB000: Důkazy pro algoritmy ■r Indukce k součtu parametrů Příklad 11.12. Co je výsledkem následujícího rekurzivního výpočtu? Algoritmus . function zkombinovat(m,n) : if m = 0 v n = 0 then res 1; else res ^— zkombinovat(m-1,n)+zkombinovat(m,n-l); fi return res . Výše uvedený vzorec (a ostatně i název funkce) naznačuje, že funkce má co společného s kombinačními čísly a Pascalovým trojúhelníkem je však třeba správně „nastavit" význam parametrů a, 6. . . t Věta. Pro každé parametry m,n £ N je výsledek výpočtu funkce zkombinovat(m,n) roven počtu všech m-prvkových podmnožin (m + n)-prvkové množiny, tedy kombinačnímu číslu res = (m+ny Petr Hliněný, Fl MU Brno, 2020 14/24 Fl: IB000: Důkazy pro algoritmy ■r if m = 0 v n = 0 then res 1; else res ^— zkombinovat(m-1,n)+zkombinovat(m,n-1); fi res 'L počet m-prvkových podmn. (m + n)-prvk. množ., tj. (mr^n) Důkaz indukcí vzhledem k součtu parametrů i = m + n: • Báze i = m + n = 0 pro m, n G N znamená, že m = n = 0. Zde však s výhodou využijeme tzv. „rozšírení báze" na všechny hraniční případy m = 0 nebo n = 0 zvlášť. V obou rozšírených případech daná podmínka algoritmu není splněna, a proto výsledek výpočtu bude počáteční res = 1. Je toto platná odpověď? * Kolik je prázdných podmnožin (m = 0) jakékoliv množiny? Jedna, 0. * Kolik je m-prvkových podmnožin (n = 0) m-prvkové množiny? Zase jedna, ta množina samotná. Tím je důkaz rozšírené báze indukce dokončen. Petr Hliněný, FI MU Brno, 2020 15/24 FI: IB000: Důkazy pro algoritmy if m = O v n = O then res 1; else res ^— zkombinovat (m-1 ,n) + zkombinovat (m,n-l); fi • Indukční krok přechází na součet i + 1 = m + n pro m, n > 0. Nyní je podmínka algoritmu splněna a vykonají se rekurentní volání zkombinovat(m-1,n) + zkombinovat(m,n-l) .c Rekurentní volání se vztahují k výběru podmnožin nosné množiny, která mám — 1 + n — m + n — 1 — i prvků, například M — {1,2,..., i}. Výsledkem tedy je, podle indukčního předpokladu pro součet i, počet všech (m — l)-prvkových plus m-prvkových podmnožin množiny M. Kolik je m-prvkových podmn. (i +l)-prvkové množiny M' — M U {i + 1}? Pokud ze všech těchto podmnožin odebereme prvek i + 1, dostaneme právě * m-prvkové podmnožiny (z těch neobsahujících prvek i + 1) plus * (m — l)-prvkové podmnožiny (z těch původně obsahujících i + 1). A to je v součtu rovno zkombinovat(m-1,n) + zkombinovat(m,n-l), jak jsme měli v indukčním kroku dokázat. □ Petr Hliněný, FI MU Brno, 2020 16/24 FI: IB000: Důkazy pro algoritmy Zesílení dokazovaného tvrzení Příklad 11.13. Zjistěte, jaká je návratová hodnota volání následující funkce tajemne(x, 1) v závislosti na celočíselné vstupní hodnotě x. Algoritmus 11.14. function tajemné(x,y ) : if x < 0 then t <- 0; else t ^— tajemné(x-l,2-y)+y; return t . Zkusíme-li si výpočet simulovat pro x = 0,1, 2, 3,4... , postupně získáme pro tajemne(x, 1) návratové hodnoty 0,1,3,7,15.... Na základě toho již není obtížné uhodnout, že návratová hodnota asi bude obecně určena vztahem 2X — 1. Toto je však třeba dokázat! Jak záhy zjistíme, matematická indukce na naše tvrzení přímo „nezabírá", ale mnohem lépe se nám povede s následujícím přirozeným zesílením dokazovaného tvrzení, které zobecňuje výsledek na proměnné hodnoty parametru y (a které také musíme uhodnout): Petr Hliněný, Fl MU Brno, 2020 17/24 Fl: IB000: Důkazy pro algoritmy Algoritmus . function tajemné(x,y ) : if x < 0 then t <- 0; else t ^— tajemné(x-l,2-y)+y; Věta. Pro každá přirozená x,y volání funkce tajemné (x, y) Algoritmu 11.14 vráti hodnotu (2X — 1) • y. Důkaz: Postupujeme indukcí podle x := i G N. • V bázi, pro vstup x = i = 0 je navrácena hodnota 0 = (2° — 1) • y.c • Indukční krok. Nechť je tvrzení známo pro x = i G N a uvažujme další vstup x := i + 1 > 0. V tom případě se vykonává druhá větev podmínky a výsledek bude roven hodnotě tajemne(x —1, 2y)+y = tajemne(i, 2y)+y.t Podle indukčního předpokladu již víme, že volání funkce tajemne(i, 2y) navrátí (2l — 1) • 2y, a celkem tak platí: tajemne(i, 2y) + y = (2i - 1) • 2y + y = 2i+1y - 2y + y = (2i+1 - 1) • y Poslední výraz je roven požadovanému (2X — 1) • y. □ Petr Hliněný, Fl MU Brno, 2020 18/24 Fl: IB000: Důkazy pro algoritmy 11.5 Dodatek: Zajímavé algoritmy aritmetiky Euklidův algoritmus Algoritmus 11.15. Euklidův pro největšího společného dělitele. input p, q ; while p>0 a q>0 do if p>q then p ^— p-q; else q ^— q-p; done output p+q. Věta. Pro každé p,g G N na vstupu algoritmus vrátí hodnotu největšího společného dělitele čísel p a q, nebo 0 pro p = q = O.c Důkaz povedeme indukcí podle součtu i— p + q vstupních hodnot. (Jak jsme psali, je to přirozená volba v situaci, kdy každý průchod cyklem algoritmu sníží jedno zp,q, avšak není jasné, které z nich.) • Báze indukce pro i = p + q = 0 je zřejmá; cyklus algoritmu neproběhne a výsledek ihned bude 0. Petr Hliněný, Fl MU Brno, 2020 19/24 Fl: IB000: Důkazy pro algoritmy while p>0 a q>0 do if p>q then p ^— p-q; else q ^— q-p; done • Ve skutečnosti je zase výhodné uvažovat rozšířenou bázi, která zahrnuje i případy, kdy jen jedno zp, q je nulové (což je ukončovací podmínka cyklu).c Pak výsledek p + q bude roven tomu nenulovému z obou sčítanců, což je v tomto případě zároveň jejich největší společný dělitel. • Indukční krok. Uvažme vstupy p := hp a q \— hq, přičemž hp + hq = i + 1 ahp>0ahq>0- tehdy dojde k prvnímu průchodu tělem cyklu. * Předp. hp > hq] poté po prvním průchodu tělem cyklu budou hodnoty p — hp — hq a q — hq, což znamená p + q — hp < hp + hq — 1 = i. * Podle indukčního předpokladu tudíž výsledkem algoritmu pro vstupy p = hp — hq a q = hq bude největší společný dělitel NSD(hp — hq, hq)x * Symetricky pro hp < hq algoritmus vrátí NSD(hp, hq — hp). Důkaz proto bude dokončen následujícím Lematem 11.16. □ Petr Hliněný, Fl MU Brno, 2020 20/24 Fl: IB000: Důkazy pro algoritmy Největší společný dělitel Lema 11.16. NSD(a, b) = NSD(a - 6, b) = NSD(a, b-a). Všimněte si, že dělitelnost je dobře definována i na záporných celých číslech. Důkaz: Ověříme, že c = NSD(a — 6, b) je také největší společný dělitel čísel a a b (druhá část je pak symetrická). • Jelikož číslo c dělí čísla a —b a b, dělí i jejich součet (a — b) + b — a. Potom c je společným dělitelem a a b. • Naopak nechť d nějaký společný dělitel čísel a a b. Pak d dělí také rozdíl a — b. Tedy d je společný dělitel čísel a — bab. Jelikož c je největší společný dělitel těchto dvou čísel, nutně d dělí c a závěr platí. Petr Hliněný, Fl MU Brno, 2020 21/24 Fl: IB000: Důkazy pro algoritmy Modulární umocňování Dále například umocňování na velmi vysoké exponenty je podkladem RSA šifry. Algoritmus 11.17. Binární postup umocňování. Pro daná čísla a, b vypočteme jejich celočíselnou mocninu (omezenou na zbytkové třídy modulo m pro prevenci přetečení rozsahu celých čísel v počítači), tj. hodnotu ab mod m, následujícím postupem. input a,b, m ; res ^— 1; while b > 0 do if b mod 2 > 0 then res ^— (res-a) mod m; b [k/2j ; a (a-a) mod m ; done output res . K důkazu správnosti použijeme indukci podle délky i binárního zápisu čísla b. Věta. Algoritmus 11.17 skončí a správně vypočte hodnotu ab mod m. Petr Hliněný, Fl MU Brno, 2020 22/24 Fl: IB000: Důkazy pro algoritmy res ^— 1; while b > O do if 6 mod 2 > 0 then res ^— (res-a) mod m; b [k/2j ; a (a-a) mod m; done output res. Důkaz: Báze indukce je pro í — 1, kdy 6 = 0 nebo 6=1. Přitom pro 6 = 0 se cyklus vůbec nevykoná a výsledek je res = 1. Pro 6 = 1 se vykoná jen jedna iterace cyklu a výsledek je res = a mod m. Nechť tvrzení platí pro všechny vstupy 6 délky i — i > 1 a uvažme vstup délky i \— i + 1. Pak zřejmě 6 > 2 a vykonají se alespoň dvě iterace cyklu. Po první iteraci budou hodnoty proměnných po řadě ax a2, 6i [6/2J a res = n = (ab mod 2) mod m .□ Tudíž délka binárního zápisu &i bude jen ^ — 1 = i a podle indukčního předpokladu zbylé iterace algoritmu skončí s výsledkem res — 7*1 • a^1 mod m — (ab mod 2 • a2^/2J) mod m — ab mod m. Petr Hliněný, Fl MU Brno, 2020 23/24 Fl: IB000: Důkazy pro algoritmy Dodatek II Relativně rychlé odmocnění Na závěr oddílu si ukážeme jeden netradiční krátký algoritmus a jeho analýzu a důkaz zde ponecháme otevřené. Dokážete popsat, na čem je algoritmus založen? Algoritmus 11.18. Celočíselná odmocnina. Pro dané přirozené číslo x vypočteme dolní celou část jeho odmocniny \_\rx\: input x; p ^— x; res ^— 0; while p > 0 do while (res + p)2 < x do res ^— res + p; p <- Lp/2J ; done output res. Petr Hliněný, Fl MU Brno, 2020 24/24 Fl: IB000: Důkazy pro algoritmy