9   Jednoduchý deklarativní jazyk
Nyní se vracíme a pokračujeme dále 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; v následujícím si ukážeme (ještě) přesnější přístup založený na myšlenkách funkcionálního programování. Zároveň si tak i procvičíme správné chápání a používání matematických definic.
/(3) i-t-
3»/(2) h-).
3»(2»/(l)) h+
3.(2.(1./(O))) h+
3 * (2 * 1) i->
if 3 then 3 . /(3 - 1) else 1 fi
3 . (if 2 then 2 . /(2 - 1) else 1 fi)
3 . (2 . (if 1 then 1 . /(I - 1) else 1 fi))
3* (2 * (1 * (if O then O * /(O-l) else 1 fi)))
3*2
i-t- 3*/(3-l) i->
i-t- 3*(2*/(2-l)) !->
i-t- 3.(2.(1./(l-l))) i->
i-t- 3 * (2 * (1 * 1)) i->
i-t- 6
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, 2011
1/16
FI: IB000: Deklarativní'jazyk
O „správnosti" programů, podruhé
Vraťme se zpět - jak se máme přesvědčit, že program funguje „správně"?c
• V případech, kdy je třeba mít naprostou jistotu správné funkce, je jedinou „dostatečně spolehlivou" možností podat formální matematický důkaz chování algoritmu, c
Úplné matematické důkazy pro svou složitost dokáží obsáhnout pouze „malé" algoritmy, c
* Přesto je jejich přesné dokazování důležité, neboť právě malé algoritmy obvykle tvoří stavební kameny rozsáhlejších systémů (kde již pak nastupují jiné metody verifikace).
Petr Hliněný, Fl MU Brno, 2011
2/16
Fl: IB000: Deklarativní'jazyk
• 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?c
* 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. c
* 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.
c
• 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ý, Fl MU Brno, 2011
3/16
Fl: IB000: Deklarativní'jazyk
9.1   Popis jednoduchého deklarativního jazyka
Definice 9.1. Deklarativní programovací jazyk (pro přednášky Fl: IB000).
• Nechť Var = {x, y, z,... } je spočetná množina proměnných.c
• Nechť Num = {0,1,... 52,... 397,... } je množina všech dekadických zápisů přirozených čísel, c
• Nechť Fun = {f,g,h,...} je spočetná množina funkčních symbolů. Ke každému / G Fun je přiřazeno číslo a G N, které nazýváme arita f.
Dále předpokládáme, že pro každé a G N existuje nekonečně mnoho / G Fun s aritou a.
• Množina výrazů Exp je (induktivně) definována následující abstraktní syntaktickou rovnicí:
E   ::=   x | n
Ei + e2 I Ei — e2 I Ei * e2 I Ei -ť- e2 j (Ei)
f(Ei,--- ,Ea)
if Ei then £2 else Es fi
V uvedené rovnici je x G Var, n G Mim, / G Fun a a G N je arita /.
Petr Hliněný, Fl MU Brno, 2011
4/16
Fl: IB000: Deklarativní'jazyk
Poznámka: Dobře si povšimněte, že ve smyslu Lekce 6 tato induktivní Definice 9.1 není jednoznačná. Neboli jeden výraz, jako třeba a + 1 — 2 * 3 lze odvodit několika různými způsoby. Praktickým důsledkem pak je, že není zřejmá „priorita operací", což lze na druhou stranu ale vždy snadno napravit přidáním dostatečného počtu závorek.c
Tuto volnost syntaxe ponecháváme z čistě pragmatického důvodu snadnějšího méně formálního zápisu výrazů. Nakonec bude priorita operací přesně určena Definicí 9.2.
Pro lepší pochopení uvádíme několik příkladů výrazů (Exp) z definice.
• 254
• 2 + 3 * 4c
• /(2)-5(5)
• f{2 + x,g(y,3*y))\z
• if x — 1 then (2 + f(y)) else g(x, x) fi    (čtěme „if x — 1 ^ 0 ... ")
Petr Hliněný, FI MU Brno, 2011
5/16
FI: IB000: Deklarativní'jazyk
Co je deklarace
Definice: Deklarace (v jazyce Definice 9.1) je konečný systém rovnic tvaru
• • • ,xai)   = Efl
fn(x1,--- ,XaJ    = Efn
kde pro každé 1 < i < n platí, že fi £ Fun je funkce arity a^, že x±,... ,xai G Var jsou proměnné a Ei je výraz, v němž se mohou vyskytovat pouze proměnné X\,..., xai a funkční symboly /i,..., fn- c
Opět uvádíme pro osvětení několik příkladů deklarací z naší definice.
• f{x)   =   if x then x * /(x — 1) else 1 fi
• /0*0    = 5(^-1,^)
g(x,y)   =   if x then /(y) else 3 fi
Později uvidíme, proč a jak je konvencí našich výpočtů tvrdit 0 — 1 "=" O.c
• g(x, y)   =   if x — y then x else y fi c
• f (x)   =   f (x) c    (Nezapisuje toto náhodou „nekonečnou smyčku"?)
Petr Hliněný, FI MU Brno, 2011
6/16
FI: IB000: Deklarativní'jazyk
9.2   Formalizace pojmu „výpočet"
Za výpočet budeme považovat posloupnost úprav výrazů, které jsou „postaveny" na naší uvažované deklaraci A. To je formálně podchyceno v následujících dvou definicích, které si porovnejte také s neformálním pojetím algoritmů jako konečných posloupností elementárních kroků v Oddíle 1.4.
• Pro připomenutí... Deklarace je konečný systém rovnic tvaru
fi{xi,--- ,xai)   = Efl
/„(Xl,-"   ,Xon)      = Efn
Definice: Nechť A je deklarace. Symbolem Exp(A) označíme množinu všech výrazů E, které splňují zároveň tyto dvě podmínky:
- E neobsahuje žádnou proměnnou.c
- Jestliže E obsahuje funkční symbol /, pak / byl v A deklarován.
Petr Hliněný, Fl MU Brno, 2011
7/16
Fl: IB000: Deklarativní'jazyk
Výrazy nad deklarací
Definice: Nechť A je deklarace. Symbolem Exp(A) označíme množinu všech výrazů E, které splňují zároveň tyto dvě podmínky:
- E neobsahuje žádnou proměnnou.c
- Jestliže E obsahuje funkční symbol /, pak / byl v A deklarován.
□
Dívejte se na množinu Exp(A) jako na soubor „platných vstupů" (jako u programu) pro deklaraci A, nad kterými bude prováděn výpočet, c
Fakt: Množinu Exp(A) lze podle Definice 9.1 zadat také induktivně:
E   y.=   n | (•E'i) I Ei + e2 I Ei — e2 I Ei * e2 I Ei -ŕ- e2 f(Ei,--- ,Ea) j if Ei then E2 else E3 f i
V uvedené zápise je n G Num, f G Fun je funkční symbol deklarovaný v A a a G N je arita tohoto /.
Petr Hliněný, Fl MU Brno, 2011
8/16
Fl: IB000: Deklarativní'jazyk
Jednotlivý krok výpočtu
Definice 9.2. Výpočet a krok výpočtu v našem deklarativním jazyce. Relaci „krok výpočtu" i—> C Exp(A) x Exp(A) definujeme induktivně; místo (E,F) G        budeme psát E\-*F, neboť se pro naše potřeby bude zhusta jednat o funkci.
i) n i—> n pro každé n £ Num. c
ii) Pro E = (Ei) definujeme krok výpočtu takto:
• Jestliže £ir->Fe Num, pak (Ei) F.
• Jestliže Ei \-+ F 0 Num, pak (Ei) \-+ (F).c
iii) Pro E = E\ -\- E2 definujeme krok výpočtu takto:
• Jestliže Ei,ľ2 £ Num, pak E\ + e2 1—>■ z, kde z je dekadický zápis čísla Ei + E2.
• Jestliže Ei 0 Num a i?i i-y F, pak £1 + £2 >->• i7 + E2.
• Jestliže Ei G Num a E2 g. Num a E2^ F, pak Ei+E2*-^ Ei + F.
Petr Hliněný, Fl MU Brno, 2011
9/16
Fl: IB000: Deklarativní'jazyk
iv) Pro E = E\ — E2 definujeme krok výpočtu takto:
• Jestliže Fi,F2 £ Mm, pak E\ — e2 1—> z, kde z je dekadický zápis čísla max{0,Fi — F2}. (Pozor na nezápornost výsledku odčítání!)
• Jestliže Ei 0 Num a Ex \-+ F, pak Ex - E2     F - E2.
• Jestliže Ex G Num a E2 0 Mm a£2^F, pak E1-E2i-^ Eľ- Fx
v) Pro E = E\ * E2 definujeme krok výpočtu takto:
• Jestliže Fi, F2 £ Mim, pak Fi *F2 \-t z, kde z je dekadický zápis čísla Ei * F2.
• Jestliže Ei 0 Mm a i?i i-y F, pak £1 * F2 1—y F * F2.
• Jestliže Ei G Mm a F2 0 Num a F2 1—> F, pak £1 * F2 1—>■ Fi * Fx
vi) Pro E = E\    E2 definujeme krok výpočtu takto:
• Jestliže Fi,F2 £ Mm, pak E\ 4 F2 1—► z, kde z je dekadický zápis (celé části) čísla [E1/E2\. Pokud E2 = 0, je z = 0 (dělení nulou!).
• Jestliže £1 0 Mm a kde £1 i->- F, pak Ex 4 F2 i->- F 4 F2.
• Jestliže Fx G Mm a F2 0 Mm a F2 i->- F, pak £1 4 F2 \-t Fx 4 F.
Petr Hliněný,  FI MU Brno, 2011
10/16
FhIBOOO: Deklarativní'jazyk
vii) Pro E = if E\ then E2 else Es fi definujeme krok výpočtu takto:
• Jestliže Ei G Num a Ex = 0, pak if Ex then E2 else E3 fi (E3).
• Jestliže Ei G Mim a Ex ^ 0, pak if Ex then E2 else E3 fi (E2).
• Jestliže Ei 0 iVum a Ei 1—> F, pak
if Ei then £2 else Eg fi 1—> if E then E2 else E3 fi.c
viii) Pro E = f (Ei, • • • , Eh) definujeme krok výpočtu takto:
• Jestliže Ei, • • • , Efc £ Mim, pak /(#!,■■ ■ ,£fc) ^ (Ef(Xl \Elr-- ,xk \Ek)
• Jinak f (Ei, ■■ ■ ,Ek) h+ f(Elr-- , E{-U F, Ei+1, ■ ■ ■ ,Ek), kde i je ne-jmenší index pro který platí E« 0 Num a E« 1—► E.c
V zápise jednotlivých bodů vždy platí, že Ei,E2,-- - G Exp(A). Znak = zde znamená „textovou" rovnost na množině výrazů Exp.
Při nejednoznačnosti vždy aplikujeme první použitelné pravidlo naší definice na prvním použitelném místě zleva, c
Definice: Reflexivní a tranzitivní uzávěr relace 1—> značíme 1—>* („výpočet").
Petr Hliněný,  Fl MU Brno, 2011
11/16
FhIBOOO: Deklarativní'jazyk
Poznámky ke kroku výpočtu
• 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ý - záporná jsou nahrazena nulou.c
- Výsledek dělení je vždy celočíselný, počítáme jeho dolní celou část.
- Dělení nulou je definováno (není chybou), výsledkem je opět nula.
• 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.c Mimo jiné je takto „definována" nejvyšší priorita vyhodnocení uzávorkovaného výrazu, c
• Uvědomte si dobře, že definice výpočetního kroku i—> je (poněkud skrytě) rekurzivní. Třeba krok (2 * 1) i—> 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, c
• Ještě si uveďme, že naše definice připouští jistý nedeterminismus: Je možné mít v deklaraci A zadaných více rovnic pro tutéž funkci /(), pak však i—> přestává být funkcí. My se touto možností nebudeme zabývat.
Petr Hliněný,  Fl MU Brno, 2011
12/16
FhIBOOO: Deklarativní'jazyk
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. Všimněte si, že při úpravách výrazů si dovolujeme (oproti formální definici) pro zpřehlednění vynechávat zdvojené a vnější závorky.
• Uvažme deklaraci f(x) — if x then x * f (x — 1) else 1 fi.   Pak /(3) i—y* 6, neboť
/(3) H- if 3 then 3 * /(3 - 1) else 1 fi H- 3 * /(3 - 1) H-
3*/(2) 3 * (if 2 then 2 */(2 - 1) else 1 fi) H-3 * (2 */(2 - 1)) H-
3*(2*/(l)) H- 3 * (2 * (if 1 then 1 * /(l - 1) else 1 fi)) H- 3*(2*(1* /(l-l)))
3*(2*(l*/(0))) H-3*(2*(l*(if 0 then 0*/(0-l) else 1 fi))) H-3 * (2 * (1 * 1)) n-
3 * (2*1) 3 * 2 i->- 6 .□
• Uvažme deklaraci f(x) — g(x — l,x) a g(x,y) — if x then /(y) else 3 fi. Pak
/(3)     ff(3 - 1, 3)     ff(2, 3) i—^ if 2 then /(3) else 3 fi i—^ /(3).
• Uvažme deklaraci f(x) — f(x). Pak pro každé n e Num platí
/(n) ^ /(n)
a podobně /(/(n)) ^ /(/(n)). Ale /(/(2 + 3)) ^ /(/(5)) ^ /(/(5)). r
Petr Hliněný,  FI MU Brno, 2011
13/16
FhIBOOO: Deklarativní'jazyk
O pořadí provádění operací ve výrazu
Příklad 9.4. Jak bude přesně vyhodnocen následující výraz?
1 + 2- 3 + 4- 5c
Řešení: Klíčem k řešení tohoto je správné pochopení Definice 9.2. Prvním použitelným pravidlem našeho deklarativního jazyka je to pro E = E\ + E2. Je použito na prvním místě zleva, tj. pro £i e 1 a £2 s 2 - 3 + 4 — 5. Podle definice je tedy nutno upravit Ei e Num i E2 ^ Num, neboli definici aplikovat (rekurzivně) na výraz E2. c
Při vyhodnocování E2 — E' = 2 — 3 + 4 — 5 je prvním použitelným pravidlem opět to pro E' = E[ + E'2, přičemž E[ = 2 — 3 a E'2 = 4 — 5. Podle definice je nutno v tomto místě vyhodnotit výraz E[ 1—y 0. Celkem v prvním kroce
1 + 2-3 + 4-5 !->• 1+0+4- 5. c
Nakonec stejným postupem získáme:
l+0 + 4-5r-^l+0 + 0r-^l + 0r-^l
Z
Petr Hliněný,  Fl MU Brno, 2011
14/16
FhIBOOO: Deklarativní'jazyk
Důkaz správnosti programu
Příklad 9.5. Pro ukázku uvažme deklaraci A obsahující pouze rovnici f(x) = if x then x * f (x — 1) else 1 fi.
Věta. Pro každé n G N platí /(n) i—>* m, kde m = nl.c Důkaz povedeme indukcí podle n:
• Báze n = 0. Platí /(O) i—^ if 0 then 0 * /(O - 1) else 1 fi i—^ 1 a také 0! = l.n
• Indukční krok. Nechť n + 1 = k. Pak
/(k) i-)- if k then k * f (k - 1) else 1 fi ■->• k * /(k - 1) ■->• k * /(w).
kde w = — 1 = n. nPodle I.P. platí /(w) i—>* u, kde u = n!. Proto k * /(w) !-»•* k*ui-yv, kde v = (n + 1) • n! = (n + 1)!. c
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, 2011
15/16
FhIBOOO: Deklarativní'jazyk
Důkazy „neukončenosti" výpočtů
Fakt: Nechť A je deklarace. Pro každé i G N definujeme relaci i—y 1 C Exp(A) x Exp(A) předpisem   \-}t   = j-t o • • • o i—y y Dále definitoricky
i
klademe ■->■ 0 = {(E,E) \ E G i£z;p(A)}. Pak platí  ■->■*   = U=o ^
Podle předchozího faktu platí, že E i—y* F právě když E i—>■ * F pro nějaké i G N. 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ů, c
Příklad 9.6. Uvažme deklaraci f(x) = f(x).
Pak pro každé n G Num platí, že neexistuje žádné m G Num takové, že /(n) i—y* m.r
Důkaz sporem: Předpokládejme, že existují n, m G Num takové, že /(n) !—»•* m. Pak existuje nejmenší i G N takové, že /(n) i—y 1 m. Jelikož výrazy /(n) a m jsou různé, platí i > 0. Jelikož i—► 1 = i—>■4-1 o i—y a /(n) i—y /(n), platí /(n) i—y %~x m, což je spor s minimalitou i. a
Petr Hliněný,  Fl MU Brno, 2011
16/16
FhIBOOO: Deklarativní'jazyk