Petr Hliněný, FI MU Brno 1 FI: IB000: Deklarativní jazyk 9 Jednoduchý deklarativní jazyk9 Jednoduchý deklarativní jazyk Pokračujeme v tématu předchozí lekce, tj. budeme se zabývat matematickým dokazováním vlastností a správnosti algoritmů. Třebaže mnohým mohla přijít už Lekce 8 více než dost formální, není tomu úplně tak; nyní si ukážeme (ještě) přesnější přístup založený na myšlenkách funkcionálního programování. f(3) if 3 then 3 f(3 - 1) else 1 fi 3 f(3 - 1) 3 f(2) 3 (if 2 then 2 f(2 - 1) else 1 fi) 3 (2 f(2 - 1)) 3 (2 f(1)) 3 (2 (if 1 then 1 f(1 - 1) else 1 fi)) 3(2(1 f(1-1))) 3(2(1f(0))) 3(2(1(if 0 then 0 f(0-1) else 1 fi))) 3 (2 (1 1)) 3 (2 1) 3 2 6 2 Stručný přehled lekce * Zavedení jednoduchého deklarativního jazyka, jeho formální přínos. * Formalizace pojmu ,,výpočet z hlediska našeho jazyka. * Několik konkrétních zápisů algoritmů a jejich vyhodnocení / důkaz. Petr Hliněný, FI MU Brno 2 FI: IB000: Deklarativní jazyk O ,,správnosti programů, podruhé Vraťme se k otázce, jak se máme přesvědčit, že program funguje ,,správně ?2 * V některých případech, jak už jsme zmínili, je třeba mít naprostou jistotu, že program funguje tak jak má, například v řídících systémech, na nichž závisí lidské životy. 2 V takovém případě je jedinou ,,dostatečně spolehlivou možností podat formální matematický důkaz chování algoritmu. 2 * A co tedy důkazy vlastností symbolicky zapsaných (procedurálních) algoritmů z Lekce 8? Všimli jste si, co v nich bylo problematickým bodem?2 Náš procedurální zápis algoritmu totiž přesně nedefinuje, co je to ,,elementární krok výpočtu ­ to je sice většinou docela zřejmé, někdy však může hlavní problém nastat právě zde. Sice by bylo možné použít k definici některý z přesných teoretických modelů výpočtu jako je Turingův stroj (nebo třeba i některý vhodný z reálných programovacích jazyků), avšak pak by se formální důkazy staly velmi složitými. 2 * Vhodnějším řešením (pro potřeby formálního dokazování) se jeví příklon k ,,funkcionálnímu zápisu algoritmů pomocí matematicky zcela přesných deklarací. Petr Hliněný, FI MU Brno 3 FI: IB000: Deklarativní jazyk 9.1 Popis jednoduchého deklarativního jazyka9.1 Popis jednoduchého deklarativního jazyka Definice 9.1. Deklarativní programovací jazyk (pro přednášky FI: IB000). * Nechť Var = {x, y, z, . . .} je spočetná množina proměnných.2 * Nechť Num = {0, 1, . . . 52, . . . 397, . . .} je množina všech dekadických zápisů přirozených čísel. 2 * Nechť Fun = {f, g, h, . . .} je spočetná množina funkčních symbolů. Ke každému f Fun je přiřazeno číslo a , které nazýváme arita f. Dále předpokládáme, že pro každé a existuje nekonečně mnoho f Fun s aritou a. 2 * Množina výrazů Exp je (induktivně) definována následující abstraktní syntaktickou rovnicí: E ::= x | n | E1 + E2 | E1 - E2 | E1 E2 | E1 ÷ E2 | ( E1 ) | f(E1, , Ea) | if E1 then E2 else E3 fi V uvedené rovnici je x Var, n Num, f Fun a a je arita f. Petr Hliněný, FI MU Brno 4 FI: IB000: Deklarativní jazyk Pozn´amka: Taková specifikace syntaxe je abstraktní v tom smyslu, že se nezabývá tím, jak výrazy jednoznačně zapsat do řádku jako posloupnost symbolů. Je na nás, abychom napsali dostatečně mnoho závorek a případně stanovili prioritu operátorů tak, aby bylo zcela jasné, jak daný výraz podle uvedené rovnice vznikl.2 (Ve smyslu Lekce 6 tato induktivní definice není jednoznačná. To nám však nebude v Definici 9.2 vadit.) Pro lepší pochopení uvádíme několik příkladů výrazů (Exp) z definice. * 254 * 2 + 3 42 * f(2) ÷ g(5) * f(2 + x, g(y, 3 y))2 * if x - 1 then (2 + f(y)) else g(x, x) fi (Vyhodnocení podmínky v ,,if testuje nenulovost argumentu.) Petr Hliněný, FI MU Brno 5 FI: IB000: Deklarativní jazyk Definice: Deklarace (v jazyce Definice 9.1) je konečný systém rovnic tvaru f1(x1, , xa1 ) = E1 ... ... fn(x1, , xan ) = En , kde pro každé 1 i n platí, že fi Fun je funkce arity ai, že x1, . . . , xai Var jsou proměnné a Ei je výraz, v němž se mohou vyskytovat pouze proměnné x1, . . . , xai a funkční symboly f1, . . . , fn. 2 Opět uvádíme pro osvětení několik příkladů deklarací z naší definice. * f(x) = if x then x f(x - 1) else 1 fi 2 ˇ f(x) = g(x - 1, x) g(x, y) = if x then f(y) else 3 fi (Jak uvidíme formálně později, konvencí našich výpočtů je neužívat záporná čísla, místo toho 0 - 1 ,,= 0.)2 * g(x, y) = if x - y then x else y fi 2 * f(x) = f(x) 2 (Nezapisuje toto náhodou ,,nekonečnou smyčku ?) Petr Hliněný, FI MU Brno 6 FI: IB000: Deklarativní jazyk 9.2 Formalizace pojmu ,,výpočet9.2 Formalizace pojmu ,,výpočet Za výpočet (nad ) budeme považovat posloupnost úprav výrazů, které jsou ,,postaveny na naší uvažované deklaraci . To je formálně podchyceno v následujících dvou definicích. Srovnejte si Definici 9.2 také s neformálním pojetím algoritmů jako konečných posloupností elementárních kroků v Oddíle 1.3. Definice: Buď deklarace. Symbolem Exp() označíme množinu všech výrazů E, které splňují zároveň tyto dvě podmínky: ­ E neobsahuje žádnou proměnnou. ­ Jestliže E obsahuje funkční symbol f, pak f byl v deklarován.2 Dívejte se na množinu Exp() jako na soubor ,,platných vstupů (jako u programu) pro deklaraci , nad kterými bude prováděn výpočet. Fakt: Množinu Exp() lze definovat také induktivně: E ::= n | (E1) | E1 + E2 | E1 - E2 | E1 E2 | E1 ÷ E2 | f(E1, , Ea) | if E1 then E2 else E3 fi V uvedené zápise je n Num, f Fun je funkční symbol deklarovaný v a a je arita tohoto f. Petr Hliněný, FI MU Brno 7 FI: IB000: Deklarativní jazyk Definice 9.2. Výpočet a krok výpočtu v našem deklarativním jazyce. Funkci ,,krok výpočtu : Exp() Exp() definujeme induktivně takto; místo (E) = F budeme psát E F . * n n pro každé n Num. 2 * Pro E (E1) definujeme krok výpočtu takto: Jestliže E1 F Num, pak (E1) F. Jestliže E1 F Num, pak (E1) (F).2 * Pro E E1 + E2 definujeme krok výpočtu takto: Jestliže E1, E2 Num, pak E1 + E2 z, kde z je dekadický zápis čísla E1 + E2. Jestliže E1 Num, pak E1 + E2 F + E2, kde E1 F. Jestliže E1 Num a E2 Num, pak E1 +E2 E1 +F, kde E2 F. Petr Hliněný, FI MU Brno 8 FI: IB000: Deklarativní jazyk * Pro E E1 - E2 definujeme krok výpočtu takto: Jestliže E1, E2 Num, pak E1 - E2 z, kde z je dekadický zápis čísla max{0, E1 - E2}. (Pozor na nezápornost výsledku odčítání!) Jestliže E1 Num, pak E1 - E2 F - E2, kde E1 F. Jestliže E1 Num a E2 Num, pak E1 - E2 E1 - F, kde E2 F.2 * Pro E E1 E2 definujeme krok výpočtu takto: Jestliže E1, E2 Num, pak E1 E2 z, kde z je dekadický zápis čísla E1 E2. Jestliže E1 Num, pak E1 E2 F E2, kde E1 F. Jestliže E1 Num a E2 Num, pak E1 E2 E1 F, kde E2 F.2 * Pro E E1 ÷ E2 definujeme krok výpočtu takto: Jestliže E1, E2 Num, pak E1 ÷ E2 z, kde z je dekadický zápis (celé části) čísla E1/E2. Pokud E2 0, je z 0 (dělení nulou!). Jestliže E1 Num, pak E1 ÷ E2 F ÷ E2, kde E1 F. Jestliže E1 Num a E2 Num, pak E1 ÷E2 E1 ÷F, kde E2 F. Petr Hliněný, FI MU Brno 9 FI: IB000: Deklarativní jazyk * Pro E if E1 then E2 else E3 fi definujeme krok výpočtu takto: Jestliže E1 Num a E1 0, pak if E1 then E2 else E3 fi (E3). Jestliže E1 Num a E1 0, pak if E1 then E2 else E3 fi (E2). Jestliže E1 Num, pak if E1 then E2 else E3 fi if F then E2 else E3 fi, kde E1 F.2 * Pro E f(E1, , Ek) definujeme krok výpočtu takto: Jestliže E1, , Ek Num, pak f(E1, , Ek) (Ef (x1 E1, , xk Ek)). Jinak f(E1, , Ek) f(E1, , Ei-1, F, Ei+1, , Ek), kde i je nejmenší index pro který platí Ei Num a Ei F.2 V zápise jednotlivých bodů vždy platí, že E1, E2, . . . Exp(). Znak zde znamená ,,textovou rovnost na množině výrazů Exp. Při nejednoznačnosti vždy aplikujeme první použitelné pravidlo naší definice zleva. Reflexivní a tranzitivní uzávěr relace značíme (,,výpočet ). Petr Hliněný, FI MU Brno 10 FI: IB000: Deklarativní jazyk Tato rozsáhlá a důležitá definice si zaslouží několik podstatných připomínek. * Za prvé si dobře povšimněte některých ,,aritmetických aspektů výpočtu. ­ Výsledek odečítání je vždy nezáporný, neboli všechna záporná čísla jsou nahrazena nulou. 2 ­ Výsledek dělení je vždy celočíselný, počítáme jeho dolní celou část. 2 ­ Dělení nulou je definováno (není chybou), výsledkem je opět nula. 2 * Další připomínka se týká pořadí vyhodnocování ve výrazu -- to je přesně dáno pořadím pravidel v Definici 9.2, neboli vždy aplikujeme první pravidlo, které aktuálně lze použít na výraz E, a to na prvním možném místě zleva.2 Mimo jiné je takto ,,definována nejvyšší priorita vyhodnocení uzávorkovaného výrazu. 2 * Uvědomte si dobře, že definice výpočetního kroku je (poněkud skrytě) rekurzivní. Třeba krok (2 1) 2 je ve skutečnosti jediným krokem, přestože ,,vyvolá použití dvou pravidel v sobě ­ vyhodnocení součinu i odstranění závorek. 2 * Ještě si uveďme, že naše definice připouští jistý nedeterminismus: Je možné mít v deklaraci zadaných více rovnic pro tutéž funkci f(), pak se však z stává pouhá relace. My se touto možností nebudeme zabývat. Petr Hliněný, FI MU Brno 11 FI: IB000: Deklarativní jazyk 9.3 Příklady výpočtů a důkazů9.3 Příklady výpočtů a důkazů Příklad 9.3. Ukážeme si několik ilustrativních ,,výpočtů nad různými deklaracemi. Uvažme deklaraci f(x) = if x then x f(x - 1) else 1 fi. Pak třeba f(3) 6, neboť f(3) if 3 then 3 f(3 - 1) else 1 fi 3 f(3 - 1) 3 f(2) 3 (if 2 then 2 f(2 - 1) else 1 fi) 3 (2 f(2 - 1)) 3 (2 f(1)) 3 (2 (if 1 then 1 f(1 - 1) else 1 fi)) 3(2(1 f(1-1))) 3(2(1f(0))) 3(2(1(if 0 then 0 f(0-1) else 1 fi))) 3 (2 (1 1)) 3 (2 1) 3 2 6 .2 Uvažme deklaraci f(x) = g(x-1, x) a g(x, y) = if x then f(y) else 3 fi. Pak například f(3) g(3 - 1, 3) g(2, 3) if 2 then f(3) else 3 fi f(3) .2 Uvažme deklaraci f(x) = f(x). Pak pro každé n Num platí f(n) f(n) a podobně f(f(n)) f(f(n)). Ale f(f(2 + 3)) f(f(5)) f(f(5)). 2 2 Pozn´amka: Všimněte si, že při našich úpravách výrazů si dovolujeme vynechávat zbytečné ,,vnější závorky kolem celého výrazu. Petr Hliněný, FI MU Brno 12 FI: IB000: Deklarativní jazyk Důkaz správnosti programu Příklad 9.4. Pro ukázku uvažme deklaraci obsahující pouze rovnici f(x) = if x then x f(x - 1) else 1 fi . Věta. Pro každé n platí f(n) m, kde m n!.2 Důkaz povedeme indukcí podle n: * Báze n = 0. Platí f(0) if 0 then 0 f(0 - 1) else 1 fi 1 a také 0! = 1.2 * Indukční krok. Nechť n + 1 k. Pak f(k) if k then k f(k - 1) else 1 fi k f(k - 1) k f(w) , kde w k - 1 = n. 2Podle I.P. platí f(w) u, kde u n!. Proto k f(w) k u v, kde v (n + 1) n! = (n + 1)!. 2 2 Vidíte, jak ,,hutný a formálně zcela přesný zápis důkazu naše formalizace umožňuje? Petr Hliněný, FI MU Brno 13 FI: IB000: Deklarativní jazyk Důkazy ,,neukončenosti výpočtů Vˇeta 9.5. Buď deklarace. Pro každé i definujeme relaci i Exp() × Exp() předpisem i = i . Dále definitoricky klademe 0 = {(E, E) | E Exp()}. Pak platí = i=0 i.2 Podle předchozí věty platí, že E F právě když E i F pro nějaké i . Navíc musí existovat nejmenší i s touto vlastností. Toto pozorování bývá velmi užitečné v důkazech ,,neukončenosti výpočtů. 2 Příklad 9.6. Uvažme deklaraci f(x) = f(x). Věta. Pro každé n Num platí, že neexistuje žádné m Num takové, že f(n) m.2 Důkaz sporem: Předpokládejme, že existují n, m Num takové, že f(n) m. Pak existuje nejmenší i takové, že f(n) i m. Jelikož výrazy f(n) a m jsou různé, platí i > 0. Jelikož i = i-1 a f(n) f(n), platí f(n) i-1 m, což je spor s minimalitou i. 2