9   Jednoduchý deklarativní jazyk
Pokračujeme v tématu předchozí lekce, tj. budeme se zabývat matematickým dokazován ím vlastnost í a spravnosti algoritmU. TřebaZe mnohým mohla prij ít uZ Lekce 8 více neZ dost formaln í, nen í tomu uplne tak; nýn í si ukaZeme (jeste) presnejs í přístup zaloZený na mýslenkach funkcionaln ího programovan í.
f (3)
3 * f (2)
3 * (2 * f (1))
3*(2*(1 *f (0)))
3 * (2 * 1)
if 3 then 3 * f (3 - 1) else 1 fi
3 * (if 2 then 2 * f (2 - 1) else 1 fi)
3 * (2 * (if 1 then 1 * f (1 - 1) else 1 fi))
3*(2 * (1 * (if 0 then 0 * f (0-1) else 1 fi)))
3*2
— 3 * f (3 - 1) —
— 3 * (2 * f (2 - 1)) —
— 3*(2*(1*f(1-1))) -
— 3 * (2 * (1 * 1)) —
— 6
StruCný přehled lekce
* Zaveden í jednoduchého deklarativn ího jazyka, jeho formaln í pr ínos.
* Formalizace pojmu „výpočet" z hlediska naSeho jazyka.
* Nekolik konkretních zapisU algoritmU a jejich vyhodnocení / dUkaz.
Petr Hline
FI MU Brno
FI: IB000: Deklarativní jazyk
O „správnosti" programů, podruhé
Vraťme se k otázce, jak se mame přesvědčit, že program funguje „správně"?c
• V nekťerých případech, jak už jsme zmínili, je treba mít naprostou jistotu, že program funguje tak jak ma, například v řídících sýstemech, na nichž zavisí lidske životý. c
V takovem případe je jedinou „dostatecne spolehlivou" možností podat formalní matematický dukaž chovaní algoritmu. c
• A co tedý dukažý vlastností symbolický žapsaných (proceduralních) algoritmu ž Lekce 8? Vsimli jste si, co v nich býlo problematickým bodem?c Nás procedurální žápis algoritmu totiž presne nedefinuje, co je to „elementární krok" vípoctu - to je sice vetsinou docela žrejme, nekdý vsak muže hlavní problem nastat príve žde. Sice bý býlo možne použít k definici nekterý ž presných teoretických modelu výpoctu jako je Turingův stroj (nebo třeba i nekterí vhodný ž reílních programovacích jažýku), avsak pak bý se formílní dukažý stalý velmi složitými. c
• Vhodnejsím resením (pro potrebý formílního dokažovíní) se jeví príklon k „funkcionalnímu" žapisu algoritmu pomocí matematický žcela přesných deklaraci.
Petr Hliněný,  FI MU Brno__FI: IB000: Deklarativní jazyk
r.
9.1   Popis jednoduchého deklarativního jazyka Definice 9.1. Deklarativní programovací jazyk (pro přednášky FI: IB000).
• Necht Var = {x, y, z,... } je spočetná množina proměnných.c
• Necht Num = {0,1,... 52,... 397,... } je množina všech dekadických žápisů přirozených císel. c
• Necht Fun = {/, g, h,... } je spocetná množina funkčních sýmbolU. Ke každemů / € Fun je přiraženo císlo a € N, ktere nažyváme arita /.
Dále předpokládáme, že pro každe a € N existuje nekonecne mnoho / € Fun s aritoů a. c
• Množina vyrazU Exp je (indůktivne) definována nýsledůjící abstraktní syntaktickou rovnici:
E   ::=   x | n
V ůvedene rovnici je x € Var, n € Num, / € Fun a a € N je arita /.
Ei + E2 | Ei — E2 | Ei * E2 | Ei -j- E2 | (Ei)
/ (Ei, ••• ,Ea)
if Ei then E2 else E3 fi
'etr Hliněný,  FI MU Brno
FI: IB000: Deklaratívni jaz;
Poznámka: Taková specifikace syntaxe je abstraktní v tom smyslu, že se nezabývá tím, jak výrazy jednoznaCne zapsat do řadku jako posloupnost symbolU. Je na nas, abychom napsali dostateCne mnoho zavorek a prípadne stanovili prioritu operatorU tak, aby bylo zcela jasne, jak dany vyraz podle uvedene rovnice vznikl.c
(Ve smyslu Lekce 6 tato induktivní definice není jednoznacna. To nam vsak nebude v Definici 9.2 vadit.)
Pro lepsí pochopení uvadíme několik příkladů vyrazu (Exp) z definice.
• 254
• 2 + 3 * 4c
• f (2) 4 g(5)
• f (2 + x,g(y, 3 * y))c
• if x — 1 then (2 + f (y)) else g(x, x) fi
(Vyhodnocenípodmínky v „if" testuje nenulovost argumentu.)
Definice: Deklarace (v jazyce Definice 9.1) je konečný systém rovnic tvaru
fi(xi, • • • ,xai)   = Ei
fra(xií        ,xa„)    = En
kde pro kaZde 1 < i < n platí, Ze f j G Fun je funkce arity aiľ Ze xi,..., xai € Var jsou promenne a Ej je výraz, v nemZ se mohou vyskytovat pouze promenne xi,... ,xai a funkční symboly fi,...,fn. c
Opet uvádíme pro osvetení nekolik příkladu deklarací z nasí def nice.
• f (x)   =   if x then x * f (x — 1) else 1 f c
,   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.)c
• g(x,y)   =   if x — y then x else y f c
^   f (x)   =   f (x) c
(Nezapisuje toto níhodou „nekonečnou smyčku"?)
Petr Hliněný,  FI MU Brno__FI: IB000: Deklaratívni jazyk
9.2   Formalizace pojmu „výpočet"
Za výpočet (nad A) budeme považovat posloupnost úprav výrazů, ktere jsou „postaveny" na naSí uvažovane deklaraci A. To je formálne podchyceno v následujících dvou definicích. Srovnejte si Definici 9.2 take s neformálním pojetím algoritmu jako konecných posloupností elementarních kroku v Oddíle 1.4.
Definice: Bud' A deklarace. Symbolem Exp(A) oznacíme množinu vsech výrazu E, ktere splňují zaroven tyto dve podmínky:
- E neobsahuje zadnou promennou.
- Jestlize E obsahuje funkcní symbol f, pak f byl v A deklarovín.c
Dívejte se na mnozinu Exp(A) jako na soubor „platnych vstupu" (jako u programu) pro deklaraci A, nad kterymi bude provaden vypocet.
Fakt: Mnozinu Exp (A) lze definovat take induktivne:
E   ::=   n | (E\) | E\ + E2 | E\ — E2 | E\ * E2 | E\ -ŕ- E2 |    f (Ei, • • • , Ea) | if Ei then E2 else E3 fi
V uvedene zapise je n € Num, f € Fun je funkcní symbol deklarovany v A a a € N je arita tohoto f.
Petr Hliněný,  FI MU Brno__FI: IB000: Deklarativní jazyk
Definice 9.2. Výpočet a krok výpočtu v našem deklarativním jazyce. Funkci „krok výpcčtu" — : Exp (A) — Exp (A) definujeme induktivně takto; míšto — (E) = F budeme pšít E — F.
• n — n pro kaZde n € Num. c
• Pro E = (-Bi) definujeme krok výpočtu takto:
* JeštliZe Ei — F € Num, pak (Ei) — F.
* JeštliZe E1 — F € Num, pak (E1) — (F).c
• Pro E = Ei -\- E2 definujeme krok výpočtu takto:
* JeštliZe E1,E2 € Num, pak E1 + E2 — z, kde z je dekadicky zýpiš číšla E1 + E2.
* JeštliZe E1 € Num, pak E1 + E2 — F + E2, kde E1 — F.
* JeštliZe E1 € Num a E2 € Num, pak E1 + E2 — E1 + F, kde E2 — F.
• Pro E = E\ — E2 definujeme krok výpočtu takto:
* Jestlize E1,E2 € Num, pak E1 — E2 — z, kde z je dekadicky zapis ňísla max{0,E1 — E2}. (Pozor na nezapornost vysledku odcítaní!)
* Jestlize E1 € Num, pak E1 — E2 — F — E2, kde E1 — F.
* Jestlize E1 € Num a E2 € Num, pak E1 — E2 — E1 — F, kde E2 — F .□
• Pro E = Ei * E2 definujeme krok výpočtu takto:
* Jestlize E1, E2 € Num, pak E1 * E2 — z, kde z je dekadicky zapis císla
E1 * E2.
* Jestliňze E1 € Num, pak E1 * E2 — F * E2, kde E1 — F.
* Jestlize E1 € Num a E2 € Num, pak E1 * E2 — E1 * F, kde E2 — F .□
• Pro E = Ei -ý- E2 definujeme krok výpočtu takto:
* Jestlize E1,E2 € Num, pak E1 4 E2 — z, kde z je dekadicky zapis (cele casti) císla [E1/E2J. Pokud E2 = 0, je z = 0 (delení nulou!).
* Jestliňze E1 € Num, pak E1 - E2 — F - E2, kde E1 — F.
* Jestlize E1 € Num a E2 € Num, pak E14E2 — E14F, kde E2 — F.
Petr Hliněný,  FI MU Brn_: IB000: Deklarativní jazyk
• Pro E = if E\ then E2 else Es fi definujeme krok výpočtu takto:
* Jestliže E\ e Num a Ei = 0, pak if Ei then E2 else E3 fi — (E3).
* Jestliže Ei e Num a Ei = 0, pak if Ei then E2 else E3 fi — (E2).
* Jestliže E1 e Num, pak
if E1 then E2 else E3 fi — if F then E2 else E3 fi, kde E1 — F
• Pro -B = f (Ei, • • • , íľfc) definujeme krok výpočtu takto:
* Jestliže Ei, • • • , Efc e Num, pak f (Ei, • • • ,Efc) — (Ef (xi ľEi, • • • ,xfc ľEfc))
* Jinak f (Ei, • • • , Efc) — f (Ei, • • • ,Ei_i,F,Ej+i, • • • , Efc), kde i je ne-jmensí index pro který plat í Ej e Num a Ei — F-□
V žapise jednotlivých bodů vždý platí, že Ei,E2, ••• e Exp (A). Znak = žde žnamena „textovou" rovnost na množine výražů Exp.
Při nejednožnaCnosti vždý aplikujeme první poůžitelne pravidlo nasí definice
žleva-
Reflexivní a tranžitivní ůžaver relace — žnaCíme —* („ výpočet").
Petr Hliněný,  FI MU Brno
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 povSimněte některých „aritmetických" aspektů výpoCtu.
- Výsledek odecítaní je vždý nezaporný, neboli vsechna zaporna císla jsou nahrazena nulou. c
- Výsledek delení je vzdý celocíselný, pocítame jeho dolní celou cast. c
- Delen í nulou je definovano (nen í chýbou), výsledkem je opet nula. c
• Dalsí pripom ínka se týka porad í výhodnocovan í ve výrazu — to je presne dano porad ím pravidel v Definici 9.2, neboli vzdý aplikujeme prvn í pravidlo, ktere aktualne lze pouz ít na výraz E, a to na prvn ím moznem m íste zleva.c Mimo jine je takto „definovana" nejvýssí priorita výhodnocen í uzavorkovaneho výrazu. c
• Uvedomte si dobre, ze defi nice výpocetn ího kroku — je (ponekud skrýte) rekurzivní. Treba krok (2 * 1) — 2 je ve skutecnosti jediným krokem, přestoze „vývola" pouzit í dvou pravidel v sobe - výhodnocen í souánu i odstranen í zavorek. c
• Jeste si uved'me, ze nase definice pripoust í jistý nedeterminismus: Je mozne m ít v deklaraci A zadaných více rovnic pro tutez funkci f (), pak se vsak z
- stava pouha relace. Mý se touto moznost í nebudeme zabývat.
Petr Hliněný,  FI MU Brno_10_FI: IB000: 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. Uvažme deklaraci f (x) = if x then x * f (x — 1) else 1 fi. Pak treba f (3) —* 6, nebot
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*(1*f (0))) — 3*(2*(1*(if 0 then 0 * f (0-1) else 1 fi))) — 3 * (2 * (1 * 1)) —
3 * (2 * 1) — 3 * 2 — 6 .□
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) .□ Uvažme deklaraci f (x) = f (x). Pak pro každe n G Num platí
f (n) — f (n)
a podobne f (f (n)) — f (f (n)). Ale f (f (2 + 3)) — f (f (5)) — f (f (5)). □ □
Poznámka: Vsimnete si, že pri nasich upravach výražu si dovolujeme výnechavat žbýtecne „vnejsí" žavorký kolem celeho výražu.
s----Petr Hliněný,  FI MU Brno_11_FI: IB000: Deklarativní jazyk ^
Příklad 9.4. Jak bude přesně vyhodnocen následující vyraz?
1 + 2 — 3 + 4 — 5c
Řešení: Kl ícem křesen í tohoto je spravne pochopen í Definice 9.2. Prvn ím pouzitelnym
pravidlem naseho deklarativn ího jazyka je to pro E = E\ + E2. Je pouzito na prvn ím m íste zleva, tj. pro Ei = 1 a E2 = 2 — 3 + 4 — 5. Podle definice je tedy nutno upravit Ei G Num i E2 G Num, neboli definici aplikovat (rekurzivne) na vyraz E2. c
Pri vyhodnocovan i E2 = E' = 2 — 3 + 4 — 5 je prvn ím pouzitelnym pravidlem opet to pro E' = Ei + E2, pricemz Ei = 2 — 3 a E2 = 4 — 5. Podle definice je nutno v tomto m íste vyhodnotit vyraz E i — 0. Celkem v prvn ím kroce
1 + 2 — 3 + 4 — 5 — 1+0+4 — 5.c
Nakonec stejnym postupem z ískame:
1+0 + 4 — 5 — 1+0 + 0 — 1 + 0 — 1
□
Petr Hliněný,  FI MU Brno
FI: IB000: Deklarativní jazyk
DUkaz 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) elše 1 fi .
Veta. Pro kaZde n € N platí f (n) —* m, kde m = n!.c DUkaz povedeme indukcí podle n:
• BýZe n = 0. Platí f (0) — if 0 then 0 * f (0 — 1) elše 1 fi — 1 a take
0! = 1.n
• IndukCní krok. Necht n + 1 = k. Pak
f (k) — if k then k * f (k — 1) elše 1 fi — k * f (k — 1) — k * f (w),
kde w = k — 1 = n. nPodle I.P. platí f (w) —* u, kde u = n!. Proto
k * f (w) —* k * u — v, kde v = (n + 1) • n! = (n + 1)!. c
Vidíte, jak „hutný" a formalne Zcela přešný Zapiš dukaZu naše formaliZace umoZnuje?
Petr Hliněný,  FI MU Brno_13_FI: IB000: Deklarativní jazyk
r.
Důkazy „neukončenosti" výpočtů Veta 9.6. Bud A deklarace. Pro každé i € N definujeme relaci — 1 C
klademe — 0 = {(E, E) | E € Exp (A)}. Pak platí —*  = U*=0 — ^
Podle predchoz í vetý plat í, ze E —* F prave kdýz E — 1 F pro nejake i € N. Navíc musí existovat nejmensí i s touto vlastnost í. Toto pozorovan í býva velmi uzitecne v dukazech „neukoncenosti" výpoctu. c
Příklad 9.7. Uvažme deklaraci f (x) = f (x).
Veta. Pro kazde n € Num platí, ze neexistuje zadne m € Num takove, ze f (n) —* m.c
Důkaz sporem: Předpokladejme, ze existuj í n, m € Num takove, ze f (n) —* m. Pak existuje nejmensí i € N takove, ze f (n) — * m. Jelikoz výrazý f (n) a m jsou ruzne, plat í i > 0. Jelikoz — * = — i-1 o — a f (n) — f (n), plat í f (n) — i-1 m, coz je spor s minimalitou i. □
Petr Hliněný,  FI MU Brno_14_FI: IB000: Deklarativní jazyk
Exp (A) x Exp (A) předpisem — 1
vt—» o ■ •• o        Dále definitoricky