' $'
&
$
%Petr Hliněný, FI MU Brno 1 IB000 "Úv. Inf.": Deklarativní jazyk
9 Jednoduchý deklarativní jazyk9 Jednoduchý deklarativní jazyk
Pokračujeme v tématu předchozí lekce, tj. budeme se zabývat matematickým doka-
zová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  3  f(3 - 1) 
3  f(2)  3  (if 2 then 2  f(2 - 1) else 1)  3  (2  f(2 - 1)) 
3  (2  f(1))  3  (2  (if 1 then 1  f(1 - 1) else 1))  3(2(1 f(1-1))) 
3(2(1f(0)))  3(2(1(if 0 then 0  f(0-1) else 1)))  3  (2  (1  1)) 
3  (2  1)  3  2  6
' $'
&
$
%Petr Hliněný, FI MU Brno 1 IB000 "Úv. Inf.": Deklarativní jazyk
9 Jednoduchý deklarativní jazyk9 Jednoduchý deklarativní jazyk
Pokračujeme v tématu předchozí lekce, tj. budeme se zabývat matematickým doka-
zová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  3  f(3 - 1) 
3  f(2)  3  (if 2 then 2  f(2 - 1) else 1)  3  (2  f(2 - 1)) 
3  (2  f(1))  3  (2  (if 1 then 1  f(1 - 1) else 1))  3(2(1 f(1-1))) 
3(2(1f(0)))  3(2(1(if 0 then 0  f(0-1) else 1)))  3  (2  (1  1)) 
3  (2  1)  3  2  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 2 IB000 "Úv. Inf.": 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ě ?
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": 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ě ?
ˇ 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": 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ě ?
ˇ 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.
V takovém případě je jedinou ,,dostatečně spolehlivou možností podat
formální matematický důkaz chování algoritmu.
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": 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ě ?
ˇ 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.
V takovém případě je jedinou ,,dostatečně spolehlivou možností podat
formální matematický důkaz chování algoritmu.
ˇ A co tedy důkazy vlastností symbolicky zapsaných (procedurálních) algo-
ritmů z Lekce 8? Všimli jste si, co v nich bylo problematickým bodem?
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": 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ě ?
ˇ 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.
V takovém případě je jedinou ,,dostatečně spolehlivou možností podat
formální matematický důkaz chování algoritmu.
ˇ A co tedy důkazy vlastností symbolicky zapsaných (procedurálních) algo-
ritmů z Lekce 8? Všimli jste si, co v nich bylo problematickým bodem?
Náš procedurální zápis algoritmu totiž přesně nedefinuje, co je to ,,elemen-
tá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.
' $'
&
$
%Petr Hliněný, FI MU Brno 2 IB000 "Úv. Inf.": 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ě ?
ˇ 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.
V takovém případě je jedinou ,,dostatečně spolehlivou možností podat
formální matematický důkaz chování algoritmu.
ˇ A co tedy důkazy vlastností symbolicky zapsaných (procedurálních) algo-
ritmů z Lekce 8? Všimli jste si, co v nich bylo problematickým bodem?
Náš procedurální zápis algoritmu totiž přesně nedefinuje, co je to ,,elemen-
tá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.
ˇ 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 IB000 "Úv. Inf.": 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 IB000).
ˇ Nechť Var = {x, y, z, . . .} je spočetná množina proměnných.
' $'
&
$
%Petr Hliněný, FI MU Brno 3 IB000 "Úv. Inf.": 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 IB000).
ˇ Nechť Var = {x, y, z, . . .} je spočetná množina proměnných.
ˇ Nechť Num = {0, 1, . . . 52, . . . 397, . . .} je množina všech dekadických
zápisů přirozených čísel.
' $'
&
$
%Petr Hliněný, FI MU Brno 3 IB000 "Úv. Inf.": 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 IB000).
ˇ Nechť Var = {x, y, z, . . .} je spočetná množina proměnných.
ˇ Nechť Num = {0, 1, . . . 52, . . . 397, . . .} je množina všech dekadických
zápisů přirozených čísel.
ˇ 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  N, které nazýváme arita f.
Dále předpokládáme, že pro každé a  N existuje nekonečně mnoho f 
Fun s aritou a.
' $'
&
$
%Petr Hliněný, FI MU Brno 3 IB000 "Úv. Inf.": 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 IB000).
ˇ Nechť Var = {x, y, z, . . .} je spočetná množina proměnných.
ˇ Nechť Num = {0, 1, . . . 52, . . . 397, . . .} je množina všech dekadických
zápisů přirozených čísel.
ˇ 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  N, které nazýváme arita f.
Dále předpokládáme, že pro každé a  N existuje nekonečně mnoho f 
Fun s aritou a.
ˇ Množina výrazů Exp je (induktivně) definována následující abstraktní syn-
taktickou rovnicí:
E ::= x | n
| E1 + E2 | E1 - E2 | E1  E2 | E1 ÷ E2 | ( E1 )
| f(E1,    , Ea)
| if E1 then E2 else E3
V uvedené rovnici je x  Var, n  Num, f  Fun a a  N je arita f.
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Deklarativní jazyk
Poznámka: Takováto 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Deklarativní jazyk
Poznámka: Takováto 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.
(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  4
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Deklarativní jazyk
Poznámka: Takováto 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.
(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  4
ˇ f(2) ÷ g(5)
ˇ f(2 + x, g(y, 3  y))
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Deklarativní jazyk
Poznámka: Takováto 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.
(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  4
ˇ f(2) ÷ g(5)
ˇ f(2 + x, g(y, 3  y))
ˇ if x - 1 then (2 + f(y)) else g(x, x)
(Vyhodnocení podmínky v ,,if testuje nenulovost argumentu.)
' $'
&
$
%Petr Hliněný, FI MU Brno 4 IB000 "Úv. Inf.": Deklarativní jazyk
Poznámka: Takováto 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.
(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  4
ˇ f(2) ÷ g(5)
ˇ f(2 + x, g(y, 3  y))
ˇ if x - 1 then (2 + f(y)) else g(x, x)
(Vyhodnocení podmínky v ,,if testuje nenulovost argumentu.)
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": 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, x1, . . . , xai 
Var proměnné a Ei je výraz, v němž se mohou vyskytovat pouze proměnné
x1, . . . , xai a funkční symboly f1, . . . , fn.
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": 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, x1, . . . , xai 
Var proměnné a Ei je výraz, v němž se mohou vyskytovat pouze proměnné
x1, . . . , xai a funkční symboly f1, . . . , fn.
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
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": 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, x1, . . . , xai 
Var proměnné a Ei je výraz, v němž se mohou vyskytovat pouze proměnné
x1, . . . , xai a funkční symboly f1, . . . , fn.
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
ˇ
f(x) = g(x - 1, x)
g(x, y) = if x then f(y) else 3
(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.)
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": 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, x1, . . . , xai 
Var proměnné a Ei je výraz, v němž se mohou vyskytovat pouze proměnné
x1, . . . , xai a funkční symboly f1, . . . , fn.
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
ˇ
f(x) = g(x - 1, x)
g(x, y) = if x then f(y) else 3
(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.)
ˇ g(x, y) = if x - y then x else y
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": 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, x1, . . . , xai 
Var proměnné a Ei je výraz, v němž se mohou vyskytovat pouze proměnné
x1, . . . , xai a funkční symboly f1, . . . , fn.
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
ˇ
f(x) = g(x - 1, x)
g(x, y) = if x then f(y) else 3
(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.)
ˇ g(x, y) = if x - y then x else y
ˇ f(x) = f(x)
' $'
&
$
%Petr Hliněný, FI MU Brno 5 IB000 "Úv. Inf.": 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, x1, . . . , xai 
Var proměnné a Ei je výraz, v němž se mohou vyskytovat pouze proměnné
x1, . . . , xai a funkční symboly f1, . . . , fn.
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
ˇ
f(x) = g(x - 1, x)
g(x, y) = if x then f(y) else 3
(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.)
ˇ g(x, y) = if x - y then x else y
ˇ f(x) = f(x)
(Nezapisuje toto náhodou ,,nekonečnou smyčku ?)
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": 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 násle-
dujícíma dvěma definicema.
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.
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": 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 násle-
dujícíma dvěma definicema.
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.
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
V uvedené zápise je n  Num, f  Fun je funkční symbol deklarovaný v  a
a  N je arita tohoto f.
' $'
&
$
%Petr Hliněný, FI MU Brno 6 IB000 "Úv. Inf.": 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 násle-
dujícíma dvěma definicema.
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.
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
V uvedené zápise je n  Num, f  Fun je funkční symbol deklarovaný v  a
a  N je arita tohoto f.
' $'
&
$
%Petr Hliněný, FI MU Brno 7 IB000 "Úv. Inf.": 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 7 IB000 "Úv. Inf.": 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.
ˇ 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).
' $'
&
$
%Petr Hliněný, FI MU Brno 7 IB000 "Úv. Inf.": 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.
ˇ 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).
ˇ 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 IB000 "Úv. Inf.": 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 8 IB000 "Úv. Inf.": 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.
ˇ 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 IB000 "Úv. Inf.": 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.
ˇ 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.
ˇ 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 IB000 "Úv. Inf.": Deklarativní jazyk
ˇ Pro E  if E1 then E2 else E3 definujeme krok výpočtu takto:
 Jestliže E1  Num a E1  0, pak if E1 then E2 else E3  E3.
 Jestliže E1  Num a E1  0, pak if E1 then E2 else E3  E2.
 Jestliže E1  Num, pak
if E1 then E2 else E3  if F then E2 else E3, kde E1  F.
' $'
&
$
%Petr Hliněný, FI MU Brno 9 IB000 "Úv. Inf.": Deklarativní jazyk
ˇ Pro E  if E1 then E2 else E3 definujeme krok výpočtu takto:
 Jestliže E1  Num a E1  0, pak if E1 then E2 else E3  E3.
 Jestliže E1  Num a E1  0, pak if E1 then E2 else E3  E2.
 Jestliže E1  Num, pak
if E1 then E2 else E3  if F then E2 else E3, kde E1  F.
ˇ 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 9 IB000 "Úv. Inf.": Deklarativní jazyk
ˇ Pro E  if E1 then E2 else E3 definujeme krok výpočtu takto:
 Jestliže E1  Num a E1  0, pak if E1 then E2 else E3  E3.
 Jestliže E1  Num a E1  0, pak if E1 then E2 else E3  E2.
 Jestliže E1  Num, pak
if E1 then E2 else E3  if F then E2 else E3, kde E1  F.
ˇ 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.
Reflexivní a tranzitivní uzávěr relace  značíme  (,,výpočet ).
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": 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.
­ Výsledek dělení je vždy celočíselný, počítáme jeho dolní celou část.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": 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.
­ 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": 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.
­ 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": 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.
­ 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.
Mimo jiné je takto ,,definována nejvyšší priorita vyhodnocení uzávorkova-
ného výrazu.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": 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.
­ 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.
Mimo jiné je takto ,,definována nejvyšší priorita vyhodnocení uzávorkova-
ného výrazu.
ˇ 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.
' $'
&
$
%Petr Hliněný, FI MU Brno 10 IB000 "Úv. Inf.": 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.
­ 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.
Mimo jiné je takto ,,definována nejvyšší priorita vyhodnocení uzávorkova-
ného výrazu.
ˇ 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.
ˇ 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 IB000 "Úv. Inf.": Deklarativní jazyk
9.3 Příklady výpočtů9.3 Příklady výpočtů
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. Pak třeba f(3) 
6, neboť
f(3)  if 3 then 3  f(3 - 1) else 1  3  f(3 - 1) 
3  f(2)  3  (if 2 then 2  f(2 - 1) else 1)  3  (2  f(2 - 1)) 
3  (2  f(1))  3  (2  (if 1 then 1  f(1 - 1) else 1))  3(2(1 f(1-1))) 
3(2(1f(0)))  3(2(1(if 0 then 0  f(0-1) else 1)))  3  (2  (1  1)) 
3  (2  1)  3  2  6 .
' $'
&
$
%Petr Hliněný, FI MU Brno 11 IB000 "Úv. Inf.": Deklarativní jazyk
9.3 Příklady výpočtů9.3 Příklady výpočtů
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. Pak třeba f(3) 
6, neboť
f(3)  if 3 then 3  f(3 - 1) else 1  3  f(3 - 1) 
3  f(2)  3  (if 2 then 2  f(2 - 1) else 1)  3  (2  f(2 - 1)) 
3  (2  f(1))  3  (2  (if 1 then 1  f(1 - 1) else 1))  3(2(1 f(1-1))) 
3(2(1f(0)))  3(2(1(if 0 then 0  f(0-1) else 1)))  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. Pak například
f(3) 
f(3), neboť
f(3)  g(3 - 1, 3)  g(2, 3)  if 2 then f(3) else 3  f(3) .
' $'
&
$
%Petr Hliněný, FI MU Brno 11 IB000 "Úv. Inf.": Deklarativní jazyk
9.3 Příklady výpočtů9.3 Příklady výpočtů
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. Pak třeba f(3) 
6, neboť
f(3)  if 3 then 3  f(3 - 1) else 1  3  f(3 - 1) 
3  f(2)  3  (if 2 then 2  f(2 - 1) else 1)  3  (2  f(2 - 1)) 
3  (2  f(1))  3  (2  (if 1 then 1  f(1 - 1) else 1))  3(2(1 f(1-1))) 
3(2(1f(0)))  3(2(1(if 0 then 0  f(0-1) else 1)))  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. Pak například
f(3) 
f(3), neboť
f(3)  g(3 - 1, 3)  g(2, 3)  if 2 then f(3) else 3  f(3) .
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
' $'
&
$
%Petr Hliněný, FI MU Brno 12 IB000 "Úv. Inf.": 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 .
Věta. Pro každé n  N0 platí f(n)  m, kde m  n!.
' $'
&
$
%Petr Hliněný, FI MU Brno 12 IB000 "Úv. Inf.": 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 .
Věta. Pro každé n  N0 platí f(n)  m, kde m  n!.
Důkaz povedeme indukcí podle n:
ˇ Báze n = 0. Platí f(0)  if 0 then 0  f(0 - 1) else 1  1 a platí
0! = 1.
' $'
&
$
%Petr Hliněný, FI MU Brno 12 IB000 "Úv. Inf.": 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 .
Věta. Pro každé n  N0 platí f(n)  m, kde m  n!.
Důkaz povedeme indukcí podle n:
ˇ Báze n = 0. Platí f(0)  if 0 then 0  f(0 - 1) else 1  1 a platí
0! = 1.
ˇ Indukční krok. Nechť n + 1  k. Pak
f(k)  if k then k  f(k - 1) else 1  k  f(k - 1)  k  f(w) ,
kde w  k - 1 = n.
' $'
&
$
%Petr Hliněný, FI MU Brno 12 IB000 "Úv. Inf.": 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 .
Věta. Pro každé n  N0 platí f(n)  m, kde m  n!.
Důkaz povedeme indukcí podle n:
ˇ Báze n = 0. Platí f(0)  if 0 then 0  f(0 - 1) else 1  1 a platí
0! = 1.
ˇ Indukční krok. Nechť n + 1  k. Pak
f(k)  if k then k  f(k - 1) else 1  k  f(k - 1)  k  f(w) ,
kde w  k - 1 = n. Podle I.P. platí f(w)  u, kde u  n!. Proto
k  f(w)  k  u  v, kde v  (n + 1)  n! = (n + 1)!.
' $'
&
$
%Petr Hliněný, FI MU Brno 12 IB000 "Úv. Inf.": 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 .
Věta. Pro každé n  N0 platí f(n)  m, kde m  n!.
Důkaz povedeme indukcí podle n:
ˇ Báze n = 0. Platí f(0)  if 0 then 0  f(0 - 1) else 1  1 a platí
0! = 1.
ˇ Indukční krok. Nechť n + 1  k. Pak
f(k)  if k then k  f(k - 1) else 1  k  f(k - 1)  k  f(w) ,
kde w  k - 1 = n. Podle I.P. platí f(w)  u, kde u  n!. Proto
k  f(w)  k  u  v, kde v  (n + 1)  n! = (n + 1)!.
2
Vidíte, jak ,,hutný a přitom formálně zcela přesný zápis důkazu naše formalizace umož-
ňuje?
' $'
&
$
%Petr Hliněný, FI MU Brno 13 IB000 "Úv. Inf.": Deklarativní jazyk
Důkazy ,,neukončenosti výpočtů
Věta 9.5. Buď  deklarace. Pro každé i  N definujeme relaci i 
Exp() × Exp() předpisem i =       
i
. Dále definitoricky klademe
0 = {(E, E) | E  Exp()}. Pak platí  = 
i=0 i.
' $'
&
$
%Petr Hliněný, FI MU Brno 13 IB000 "Úv. Inf.": Deklarativní jazyk
Důkazy ,,neukončenosti výpočtů
Věta 9.5. Buď  deklarace. Pro každé i  N definujeme relaci i 
Exp() × Exp() předpisem i =       
i
. Dále definitoricky klademe
0 = {(E, E) | E  Exp()}. Pak platí  = 
i=0 i.
Podle předchozí věty platí, že E  F právě když E i F pro nějaké i  N0.
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ů.
' $'
&
$
%Petr Hliněný, FI MU Brno 13 IB000 "Úv. Inf.": Deklarativní jazyk
Důkazy ,,neukončenosti výpočtů
Věta 9.5. Buď  deklarace. Pro každé i  N definujeme relaci i 
Exp() × Exp() předpisem i =       
i
. Dále definitoricky klademe
0 = {(E, E) | E  Exp()}. Pak platí  = 
i=0 i.
Podle předchozí věty platí, že E  F právě když E i F pro nějaké i  N0.
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ů.
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.
' $'
&
$
%Petr Hliněný, FI MU Brno 13 IB000 "Úv. Inf.": Deklarativní jazyk
Důkazy ,,neukončenosti výpočtů
Věta 9.5. Buď  deklarace. Pro každé i  N definujeme relaci i 
Exp() × Exp() předpisem i =       
i
. Dále definitoricky klademe
0 = {(E, E) | E  Exp()}. Pak platí  = 
i=0 i.
Podle předchozí věty platí, že E  F právě když E i F pro nějaké i  N0.
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ů.
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.
Důkaz sporem: Předpokládejme, že existují n, m  Num takové, že f(n) 
m. Pak existuje nejmenší i  N0 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