Program, algoritmus, funkce
Program je form/Elní popis chov/Eníějiak0ho syst0mu (aplikání program, reaktivní syst0m, operační syst0m...). Skl/Ed/E se z popisu algoritmů.
Algoritmus lze ch/Epat jako parci/Elní funkci z množiny všechnožných vstupů do množiny všech možných výstupů.
funkce : Vstupy —■> Výstupy
Pozor, není to definice: sice každ0mu algoritmu odpovíd/E pani/Elní funkce ze vstupů do výstupů, ale naopak ne každou takovou funkci lze vyj/Eit algoritmem.
3
Algoritmus je parci/Elní funkce z množiny vstupů do množinyvýstupů, k níž existuje konečný popis v určit0m formalismu.
Tímto formalismem je typicky programovací jazyk, ale existují i další matematick0 formalismy: Turingův stroj, RAM, lambda kalkul, kombin/Bbrový kalkul, vyčísliteln0 funkce, Markovův algoritmus...
Slovo algoritmus je odvozeno ze jm0na starovšk0ho persk0ho matematika a astronoma al-Chwarezmího (Abú 'Abd Alláh Muhammad ibn MGsä al-Khwärizmľ).
4
Funkce z množiny vstupů do množiny výstupů, kter0 lze vyj/Eřit algoritmem, se nazývají rekursivně spočetnQ
Reaktivní syst0m je program, jehož prov/Eění norm/Elě nemusí končit (např. operační syst0my apod.), v obecnějším smyslu jsou to interaktivní programy.
Program, který je implementovaným algoritmem, při výpočtu přečte vstup, zpracuje ho (vstupní data transformuje na výstupní), vypíše výstup a skončí.
Většina současných programů je interaktivních, ale souč/Estí všech jsou algoritmy.
Korektnost algoritmu
In množina vstupních dat
Out množina výstupních dat
A : In —■> Out algoritmus (na vstupu z In vypisující výstup z Out)
cp : In —> £00/ vstupní podmínka
ijj : In x Out —> £00/ výstupní podmínka
Vstupní podmínka cp určuje, zda daný vstupní oedaj je pro algoritmuspř/pusfr?/, vymezuje tedy jistou podmnožinu množiny vstupních dat In.
Výstupní podmínka tp řík/E, zda daný výstupní cedaj jěi není výsledkem výpočtu algoritmu na dan0m vstupním cedaji.
Vstupní podmínka je un/Erní predik/Et na množěnvstupních dat, výstupní podmínka je bin/Erní predik/Et na množin/Ech vstupních a výstupních dat.
Výstupní podmínka V> řík/E, zda daný výstupní oedaj jěi není (pro nedeterministicko algoritmy zda může či nemůže být) výsledkem výpočtu algoritmu na dan0m vstupním oedaji.
Příklad:   Algoritmus A přečte tři čísla a vypíše je v neklesajícím pořadí; funguje korektně pro „mal/E" pirozen/Bčísla.
In = Out = Z x Z x Z,
<pA(x, y,z) = 0 < x < 231 A 0 < y < 231 A 0 < z < 231 iPa(%,   z, u, v, w) = (u,v,w) £ Permut(x, y, z) A u < v < w
Pozn/Emka: Připustíme i algoritmy, kter0 nenačítají ž/Edný vstup. Pro ě položíme /n = {0}.
Def: Řekneme, že A je konvergentní vzhledem k cp, když množina {x G In \ (p(x)} je podmnožinou definičního oboru funkce A, tj. když pro každou vstupní hodnotu x, pro niž platí (p(x), je výsledek výpočtu podle algoritmu A definov/En (výpéet se zastaví).
Def:   Řekneme, že A je parci/Elě korektní vzhledem k cp a tp, když pro každou vstupní hodnotu x z definičního oboru funkce A splňující vstupní podmínku ip (tj. pro každ0£, pro něž je A(x) definov/Eno ap(x)) platí ip(x, A(x)).
Def:   Řekneme, že A je tot/Elě korektní vzhledem k cp a tp, když je konvergentní vzhledem k cp a parci/Elě korektní vzhledem k cp a tp.
Důsledek:   Algoritmus A je tot/Elě korektní vzhledem k cp a ijj, pr/Eé když pro každou vstupní hodnotu x splňující vstupní podmínku výpočet podle algorimu A skončí a jeho výsledek splňuje i výstupní podmínku.
Vstupní a výstupní podmínce se \ak0ť\k/Especifikace algoritmu. O tot/Elě korektním algoritmu pak řík/Eme, ževyhovuje specifikaci.
7
Výpočetní paradigmata
Paradigma (vzor, přístup, pojetí) ud/Ev/E způsob, jakým je algoritmus vyjyflědi.
Výpočetní paradigmata:   - imperativní
-funkcion/Elní
- Iogick0
- procedur/Elní
- objektov0
- sekvenční
- paralelní
Imperativní paradigma
Neform/Elní definice:
Výpočet je posloupností tzv. výpočetních kroků. Výpočetní krok je realizací instrukce (jednoduch0ho riíkazu) programu. Přenos informace mezi jednotlivými kroky výpočtu zprostředkov/Ev/šfáK.
Jinak řečeno, příkazy programu jsou stavov0 transform/Etory— (parci/Elní) funkce z množiny stavů do množiny stavů.
Pro form/Elní definici je nutno zav0st abstraktní poítač. V sekvenčním imperativním paradigmatu jím nejčastěji býv/E Turingův stroj nebo RAM (Random-Access Machine).
Může jím být tak0 „vyšší" imperativní jazyk, který krorrě element/Erních stavových transform/Etorů (typicky {zvpřiřazovacího příkazu) obsahuje složen0 stavov0 transform/Etory realizující sekvenci (begin-end), bin/Erní étvení výpočtu (if-then-else), n/Esobn0štvení (case), opakov/Ení (while-do, for-do), apod.
Výpočetním krokem je pak přechod mezi dvěma konfiguracemi Turingova stroje, resp. provedení jedn0 instrukce RAMu, resp. provedení jed noho element/ErníhcpnWazu.
Abstraktní počítače pro imperativní programy
• Tu ringů v stroj
• RAM
• (abstraktní) programovací jazyk
Tu ringů v stroj
• Konečn/E nepr/Ezdn/E množiSasymbolů — tzv. abeceda
• Nekonečn/^o/£s/ca— spočetn/E posloupnost poliek. Každ0 polčko p/Esky obsahuje jeden symbol abecedy, přičemž skoro všechna políčka obsahují zvl/Eštní symboU.
• Čtecí hlava, jejíž pozice na p/Esce je d/Enařpozeným číslem.
• Konečn/E množina!? vnitřních stavů s vyznačeným poč/Etěním stavem <7n a koncovými stavy F C S.
• Přechodov/E funkce :SxE^SxSx{L,R}
11
RAM
• Spočetn/E posloupnostM registrů (paměťových míst) — tzv. paměť. Každý registr obsahuje cel0číslo, vždy však skoro všechny obsahují nulu.
• Stav a e S = N x Z*
• Konečn/E množina inštrukcií. Každ/E instrukca G X m/E danou s0mantiku — funkci l : S —■> S.
• Konečn/E posloupnostP G X* instrukcí, tzv. program
J
12
Příklad:   Výpočet faktori/Elu (funkcion/Elní verze - Pascal)
Faktori/Ehez/Epom0ho cel0hóísla n je číslo n! = 1 • 2 • 3.....(n — 1) • n.
Speci/Elě 0! = 1 (součin nulov0ho pcčtu činitelů).
function fact (n:Integer): Integer; begin
if n==0 then fact:= 1 {return 1}
else fact:= n*fact(n-l)   {return n*fact(n-l)}
end
Věta:   Funkce fact konverguje vzhledem ke vstupní podmínce (p(ri) = n E N.
Věta:   Funkce fact je parci/Elě korektní vzhledem k^ak výstupní podmínce
^(n, k) = k — n\.
Důsledek:   fact je tot/Elě korektní vzhledem k cp, ip.
Věta:   Funkce f act konverguje vzhledem ke vstupní podmínce (f(n) = n G N.
Důkaz indukcí podle n. Pro n = 0 se výpočet zastaví; zastaví-li se výpočet pro n, zastaví se i pro n + 1.
Věta:   Funkce f act je parci/Elě korektní vzhledem k <p a k výstupní podmínce
i/j(n, k) = k = n!.
Důkaz opět indukcí podle n. f act(O) = 1 = 0!. Nechť n > 0 a tvrzení platí pro n — 1. Pak
f act (n) = n • f act (n — 1) = n • (n — 1)! = n!, tedy tvrzení platí i pro n.
Výpočet faktori/Elu (imperativní verze - Pascal)
function factorial (n:Integer): Integer;
var i, k: Integer;
begin
i : = 0;
k := 1;
while   i < n do begin i :=
k := k*i
end;
factorial := k      {return k} end
Věta:   Funkce konverguje vzhledem ke vstupní podmínce (p(ri) = n G N.
Funkce je parci/Elě korektní vzhledem kcp ak výstupní podmínce tp(n, k) = k = n\.
Věta:   Funkce f actorial konverguje vzhledem ke vstupní podmínce <p(n) = n G N.
Důkaz spočív/E v nalezenčíseln0 hodnoty (z/Evisl0 na obsahu programových proěinných), kter/E v ž/Edn0m okamžiku výptw nemůže být z/Eporn/E ařjlom při každ0m průchodu ělem cyklu klesne nejm0ně o jedničku. V tomto příkladě je touto hodnotou číslo n — i a důkaz nez/Epornosti i kles/Ení je snadný.
Věta:   Funkce f actorial je parci/Elé korektní vzhledem k (f a k výstupní podmínce
ip(n, k) = k = n\.
Důkaz spočív/E v nalezení mezilehlých podmínek, zejm0na invariantuycklu while. Invariant cyklu v místě testov/Ení podmínky \ek = i\ A 0 < i < n.
Invariant cyklu
je mezilehl/E podmínka, kter/E je spima v dan0m boce výpočtu podle algoritmu Invariant cykluv každ0m průchodu cyklem.
V našem příkladě bude invariantem cyklu while podmínka fc = üA0<i<na bude se vztahovat k místu testov/Ení podmínky cyklu. Důkaz paroíElní korektnosti funkce f actorial se rozloží do kroků:
1. Platí-li na zač/Etku^(n), pak po provedení oevodních pjiřazení bude splněn invariant cyklu.
2. Je-li v nějak0m okamžiku splněn invariant cyklu a provede se tělo cyklu, pak po jeho provedení bude opět splněn invariant.
3. Je-li splněn invariant cyklu a není splněna podmínka cyklu, pak je splněna mezilehl/E podmínka za cyklem, tedy ip(n, k).
_)
Pro místa v algoritmu ležící mezi příkazy stanovíme tzv. mezilehlOpodmínky Podmínka na zač/Etku buóep(n), podmínka na konci bude z ostatních bodů v algoritmu pro
důkaz parci/Elní korektnosti obvykle stáí vybrat jen význačn/E místa, v nichž se stav výpótu významně mění. Takovými místy jsou body uvnitř cyklů, například na jejich zač/Etku. Mezilehl/E podmínka pro místo uvnřt cyklu se nazýv/Einvariant cyklu.
Příklad: Algoritmus umocňov/Encísla na přirozený exponent (funkcion/Elní verze -Pascal)
function pow (z:Real; n:Integer): Real;
{ Predpokladá se z>0, n>0 }
begin
if n==0 then pow := 1
else pow := z * pow(z,n-l)
end
Věta:   Funkce pow konverguje vzhledem ke vstupní podmínce
(p(z, n) = z e M, n G N, z > 0.
Důkaz: Klesající hodnotou je zde exponent.
Věta: Funkce pow je parci/Elě korektní vzhledem ke vstupní podmínce ip a k výstupní podmínce ip(z, n, r) = r — zn.
16
Důkaz věty: Indukcí podle exponentu.
Příklad:   Algoritmus umocňov/Enčísla půlením exponentu (imperativní verze - Pascal)
function power (z:Real; n:Integer): Real; { Předpokládá se z>09 n>0 } var y,r:Real; k:Integer; begin
k	:= n;
y	:= z;
r	:= 1;
while k > 0 do begin
if odd(k) then r := r * y; k := k div 2; y := sqr(y) end; power := r end
Věta:   Funkce power konverguje vzhledem ke vstupní podmínce
(p(z, n) = z e M, n G N, z > 0.
Důkaz: Klesající hodnotou je zde exponent. Kles/Ení je tencbkr/Et rychlejší než v předch/Ezejícím píkladě, ale pro k > 0 je vždy ostr0.
Věta: Funkce power je parci/Elé korektní vzhledem ke vstupní podmínce (p k výstupní podmínce ip(z, n, r) = r = zn.
Invariant:   r • yk = zn A k > 0
Věta:   Funkce power konverguje vzhledem ke vstupní podmínce
<p(z, n) = z e R, n <E N, z > 0.
Důkaz: Klesající hodnotou je zde exponent. Kles/Ení je tercbkr/Et rychlejší než v předch/Ezejícím píkladě, ale pro k > 0 je vždy ostr0.
Věta: Funkce power je parci/Elě korektní vzhledem ke vstupní podmínce (pak výstupn podmínce ^(z, n, r) = r = zn.
Důkaz: Invariant cyklu while, který platí vždy v okamžiku testov/Ení podmínky cykluj > 0),
r • yk = zn A k > 0
Po poslední iteraci platí tento invariant v konjunkci spolu s negací podmínky cyklu (-i(k > 0)). Z t0to konjunkce vyplýv/5: = zn, přičemž r je výsledn/E hodnota funkce power. Platí tedy i výstupní podmínka power (z, n)).
Příklad:   Algoritmus řazení vkl/Ed/Ením (imperativní verze - Pascal)
1 const MAX = 999;
2 type Elem = Integer;
3 Posl = array [1..MAX] of Elem;
4 procedure ilnsSort (n:Integer; var A:Posl);
5 var i, j  : Integer;    x : Elem;
6 begin
7 for i := 2 to n do
8 begin
9 x := A[i] ;    j  : = i-1;
10 while (j>0) && (A[j]>x) do
11 begin
12 A[j+1]   := A[j] ;
13 j  := j-1
14 end;
15 A[j+1]   := x
16 end
17 end
Věta:   Algoritmus ilnsSort je tot/Elě korektní vzhledem k podmínk/Em
(p(n, A)        =   posloupnost A je nepr/Ezdn/E n > 1 je její d0lka ip(n,A,Af)   =   posloupnost Af je permutací posloupnosti A a je neklesající
20
Věta:   Nechť Z* označuje množinu všech konečných celočíselných posloupností, In = N x Z*,Out= Z*. Nechť <p(n,A) = n > 1 A \A\ = n, V>(n, A, A') = A' e Permut{A) A Vij, l<i<j< n.A^ < A^ Pak ilnsSort je tot/Elě korektní vzhledem k podmínk/Emý9, i/j.
Důkaz rozložíme na důkaz konvergence a parci/Elní korektosti.
Lemma:   Algoritmus ilnsSort je konvergentní vzhledem k (p.
Důkaz: Vnější cyklus for vždy skončí, protože je vždy předem d/En pevný poet jeho opakov/Ení^i — 1). Vnitřní cyklus while se prov/Edí jen kdyžj > 0. Ale při každ0m průchodu tělem tohoto cyklu hodnota proměnn0 j klesne. To znamen/E, že cyklus while se provede konečněkr/Et (nejvýše(i — l)-kr/Et).
Lemma:   Algoritmus ilnsSort je parci/Elě korektní vzhledem k podmínk/Em^, ip.
Důkaz: Vstupní posloupnost označme (ai,..., an), obsah pole A (v dan0m stavu výpočtu) označme (Ai,..., An).
Invariantem vnějšího cyklu for (splněným vždy na zač/Etku tohoto cyklu) je podmínka
A\ < A2 < - - - < Ai-i A (Ai,..., Aí-i) e Permut(ai,..., a;_i) A A{ =
cii,..., An = an, takže po posledním průchodu cyklem for platí A\ < A2 < ... < An.
Invariantem vnitřního cyklu while (opět splněným vždy na zač/Etku cyklu) je podmínka
Ai < • • • < Aj-! < Aj = Aý+i < Aj+2 <-" <
Ai A (Ai,..., Aj, a^, Aj+2, • • •, Ai) G Permut(ai,..., a^)
(Důkaz, že jde skutečně o invarianty, je snadný.)
Funkcion/Elní paradigma
Neform/Elní definice:
Výpočet je posloupností tzv. redukčních kroků, z nichž každý je element/Erní oepravou programu (výrazu). Výsledkem výpočtu je hodnota, kterou už nelze d/Ele zjednodušit.
D0lka výpočtu je pak d0lkou t0to posloupnosti, tj. poet redukčních kroků vedoucích k výsledku.
Pro form/Elní definici je nutno zav0st form/Elní kalkul. Ve fkiciion/Elním paradigmatu jím nejčastěji býv/E jazyk vych/Ezející z lambda kalkulu -funkcion/Elníjazyk
21
Příklad: Funkce maxim najde největší číslo z konečn0ho nepr/Ezdn0ho seznamaísel maxim [x] = x
maxim (x:y:s)    =   if x>y then maxim (x:s)
else maxim (y:s)
maxim [4,3,5,1] ~» if 4>3   then maxim [4,5,1] else maxim [3,5,1] -w if True then maxim [4,5,1] else maxim [3,5,1]
maxim [4,5,1] ^ if 4>5     then maxim [4,1] else maxim [5,1] if False then maxim [4,1] else maxim [5,1]
maxim [5,1]
if 5>1 then maxim [5] else maxim [1] ^ if True then maxim [5] else maxim [1]
maxim [5]
5
Příklad:   Algoritmus řazení vkl/Ed/Ením (funkcion/Elní verze - Haskell)
flnsSort []       = [] flnsSort (x:s) =   ins x (flnsSort s) where ins x []       = [x]
ins x (y:t) = if x<=y then x:(y:t)
else y:(ins x t)
Nechť In = Out\e množina všech seznamů (posloupností) celých čísel, (p(s) = s je konečný,
ip(s, ť) = „t je permutací seznamu s a t je neklesající".
Věta:   AlgoritmusPak flnsSort je tot/Elě korektní vzhledem k cp, ip.
Pozn/Emka: V Haskellu lze definici zapsat i kratčeji: flnsSort =   foldr ins [] .
Věta:   AlgoritmusPak f InsSort je tot/Elě korektní vzhledem k (p,
Důkaz: Nechť s je konečný seznam d0lkyn. Konvergence obou funkcí se uk/Eže indukcí pes d0lku seznamu.
Při důkazu parci/Elní korektnosti vyjdeme z vlastnosti funfee ins: Je-li seznam u neklesající, pak ins y u je neklesající permutace seznamu y: u. Zbytek indukcí přes d0lku seznamus.