Seznámíme se ještě s jedním nenumerickým algoritmem, s hledáním cesty v bludišti. Ukážeme si na něm celou řadu důležitých vlastností algoritmů i některé postupy, kterými lze ověřovat jejich správnost.
Pro motivaci a terminologii se vypravíme až do antického Řecka. Připomeňme si příběh athénského hrdiny Thésea a krétské princezny Ariadny.
Všechno začalo na Krétě za vlády krále Mínóa. Králova manželka Pásifaé byla svému manželovi nevěrná, dokonce s býkem (je s podivem, co všechno se tenkrát smělo o vládcích, a pokud víme beztrestně, říkat). Z nepřirozeného vztahu se královně narodil syn Mínótauros s býčí hlavou. Rozzlobený král nechal Mínótaura uvěznit v Labyrinthu, právě dokončené stavbě s mnoha chodbami a komnatami, jejíž jméno vešlo později do všech jazyků jako název pro bludiště. Po vítězství nad Athénami uložil Mínós poraženým povinnost posílat každoročně sedm panen a sedm jinochů jako potravu pro Minótaura. Athénský princ Théseus se k nim dobrovolně připojil a Mínótaura v Labyrinthu zabil. Pomohla mu v tom Ariadna, dcera krále Mínóa, která dala Théseovi klubko nití, aby v Labyrinthu nezabloudil a vrátil se k ní zpět. Tak začal příběh jejich lásky, o němž se můžete dočíst např. u Ovidia.
My se z
celého jímavého příběhu soustředíme pouze na rekonstrukci algoritmu, který
mohla Ariadna Théseovi poradit. Nepůjde nám při tom ' pochopitelně o
historicky důvěryhodnou verzi algoritmu. Báje nám k tomu ostatně dává pouze
jediné vodítko, zmínku o klubku nití.
Abychom
mohli sestavit vhodný algoritmus, musíme si úlohu zadat přesněji. Zjednodušíme
ji předpokladem, že Mínótauros se v bludišti nepohybuje a setrvává stále v
jedné komnatě. Vždyť přece šlo o geneticky méněcennou bytost, kterou nepochybně
dlouhý pobyt v Labyrinthu bez reálné naděje na to, že se někdy dostane ven,
musel unavit. Na druhé straně Ariadně situaci zkomplikujeme tím, že přivedeme
na scénu Théseovu matku (v Ariadniných plánech její budoucí tchýni). Jmenovala
se Aithra a měla, jak už to bývá, o svého syna velký strach a vrozenou nedůvěru
k potenciálním snachám obecně, a k Ariadně obzvlášť. Vždyť šlo přece o dceru
nepřátelského krále! Proto Aithra vyžadovala přesvědčivé argumenty, že
Ariadniny návody nepřivedou Thésea do záhuby.
Ariadna musí tedy hledat takový algoritmus, který by splňoval tři požadavky:
1. Musí být pro Thésea snadno zapamatovatelný a proveditelný. Uvědomme si, že úlohou Thésea nebylo "provádět jakýsi algoritmus", ale najít a zabít netvora. Rek duševně zdeptaný prováděním složitého algoritmu by se mohl stát snadnou kořistí Mínótaura, čímž by neúnosně utrpěl "výchovný dopad" báje.
2. Musí být také snadno obhajitelný jak před Théseem, tak i před jeho matkou. Théseus požaduje jistotu, že komnatu s Mínótaurem v bludišti nemine (chce se přece vyznamenat před dějinami), Aithra zase požaduje záruku, že její syn v Labyrinthu nezabloudí, a to ani v případě, že by v něm žádný Mínótauros nebyl. Jako žena životem zkušená si totiž dovede představit daleko pravděpodobnější důvody pro Mínóův požadavek sedmi panen a mladíků, než je jakýsi poločlověk polobýk v bludišti.
3. Měl by zaručit, že Théseus, po tom, co
Mínótaura najde a jak Ariadna pevně věří zabije ho, se nebude muset unaven
bojem se stvůrou vracet k Ariadně oklikami, ale bude moci jít přímou cestou
"bez smyček".
Víme, že Ariadna dala Théseovi onu bájnou nit. My ho pro jednoduchost popisu algoritmu vybavíme ještě zcela nehistorickou rekvizitou - červeným fixem.
Algoritmus bude navržen tak, aby Théseus neprošel žádnou chodbou více než dvakrát. Proto bude Théseus označovat chodby, kterými již prošel, pomocí fixu a niti.
Při prvním průchodu chodbou Théseus rozvíjí nit. Pokud se některou chodbou vrací zpět, pak při tom jednak označí oba její konce červeným fixem, jednak nit opět svine. Jak uvidíme, bude algoritmus navržen tak, že Théseus nikdy nevstoupí do chodby, která je označena fixem, a chodbou, kterou je právě natažena nit, se může pouze vrátit zpět.
Abychom se o tomto označení chodeb mohli pohodlněji vyjadřovat, zavedeme pro ně pojmenování, která vám připomenou barvy na semaforu. V každém okamžiku práce algoritmu si můžeme představovat chodby v bludišti "obarvené" na jednu ze tří barev: červenou, žlutou nebo zelenou.
Červenými budeme nazývat ty chodby, jejichž oba konce jsou označeny červeným fixem (a kterými tedy Théseus již dvakrát prošel). V červených chodbách nemůže být natažena nit, protože ji Théseus při návratu svinuje. Chodby, kterými je právě natažena nit, budeme nazývat žlutými (těmito chodbami prošel Théseus jen jednou). A konečně o chodbách, které nejsou ani červené ani žluté (a kterými tedy Théseus neprošel dosud ani jednou) budeme mluvit jako o chodbách zelených.
Na počátku jsou všechny chodby v bludišti zelené. Théseus může vcházet jen do zelených chodeb a vracet se žlutými. Při průchodu zelenou chodbou rozvíjí Théseus nit a tím "obarvuje tuto chodbu nažluto". Při návratu žlutou chodbou označí Théseus oba její konce červeným fixem a smotává nit; tak "obarvuje chodbu načerveno". Protože do červených chodeb nesmí Théseus vstoupit, nedochází při provádění algoritmu k jiným změnám barev chodeb.
Fixem
jsme tedy vybavili Thésea proto, aby mohl odlišit červenou chodbu od zelené.
Jste-li pedanti nebo máte-li dost nití, jistě vás napadlo, že by se Théseus
mohl obejít i bez fixu, kdyby při cestě zpět žlutou chodbou nit nesmotával, ale
pokládal ji tam podruhé. To by však bylo v praxi, jak jistě sami uznáte, velmi
nepohodlné a nespolehlivé (zašmodrchávání nití, jejich vytahování z chodeb,
zakopávání o ně apod.).
Nyní jsme už schopni podat návod, který mohla Ariadna Théseovi dát. Mohl znít třeba takto:
Bludiště
začneš prohledávat ve vstupní komnatě, kde na tebe budu čekat, dokud se
nevrátíš. Když přijdeš do komnaty, vždy zjisti podle následující tabulky, ve
které z pěti možných situací se nacházíš, a pak proveď akci pro tuto situaci
předepsanou. Při zjišťování situace postupuj vždy od začátku tabulky. Tedy
např. ve třetí situaci - "Zelená cesta" - se nacházíš, jestliže nejsou
splněny podmínky předchozích dvou situací - "Mínótauros" a
"Smyčka" - a je-li splněna podmínka této situace.
Situace Akce
1. Mínótauros STOP
v komnatě je Mínótauros
2. Smyčka ZPĚT, namotej nit
z komnaty vychází více než jedna žlutá chodba
3. Zelená cesta VPŘED, rozmotej nit
z komnaty vychází alespoň jedna zelená chodba
4. Ariadna STOP
v komnatě je Ariadna
5. Slepá cesta ZPĚT, namotej nit
z komnaty vede jediná žlutá chodba
Při akci ZPĚT se Théseus vrací žlutou chodbou, kterou právě přišel (a tím ji přebarvuje na červenou).
Při akci VPŘED si vybere jednu ze zelených chodeb, vycházejících z komnaty, a vydá se do ní (tím ji přebarvuje na žlutou). Aby to byla skutečně algoritmická akce, musíme ještě doplnit její popis o předpis, jak vybrat z (případně) více zelených chodeb, které z komnaty vycházejí, tu, jíž se má vydat. Abychom tedy zajistili mechanické provádění algoritmu a ušetřili Théseovi "zbytečné" rozhodování, přede píšeme mu, že v situaci "Zelená cesta" se má vydat vždy do první zelené chodby zleva.
Jak však
uvidíte, nebude správnost našeho algoritmu na volbě zelené chodby nijak
záviset. Mohli bychom Théseovi předepsat i jiný způsob jejího výběru. Mohl by
si třeba hodit kostkou (snad byly tehdy již známy), jít ve směru řevu bestie
nebo si vybrat jakkoli jinak. Takovému výběru, který nemůže ohrozit úspěch
algoritmu, ale může v některých případech jeho práci urychlit, se někdy říká heuristický
výběr.
V animaci můžete vyzkoušet cestu Théseua v jednom konkrétním bludišti. Při trasování se ukazuje i stav, ve kterém se Théseus právě nalézá.
Povšimněte si na této cestě Labyrinthem několika skutečností:
1. V komnatě D se podle našeho algoritmu Théseus vydal první zelenou chodbou vlevo. Kdyby se řídil nějakou jinou heuristikou (např. naslouchal řevu býka), našel by Mínótaura dříve. Vždyť už byl v těsném sousedství jeho komnaty M.
2. Při první návštěvě v komnatách J a K a třetí návštěvě v komnatě I se Théseus ocitá v situaci "Slepá cesta".
3. Při návratu do Ariadniny komnaty A se Théseus nemohl zastavit, protože podle definice algoritmu nebyl v situaci "Ariadna", ale v situaci "Smyčka" (z komnaty vedou dvě žluté chodby).
4. Při svých druhých návštěvách komnat B a D je
Théseus v situaci "Smyčka", protože z komnat vycházejí tři žluté
chodby.
Naučili
jsme se tedy spolu s Théseem hledat v bludišti. Dokázali bychom však pomoci
Ariadně přesvědčit Aithru a Thésea o správnosti algoritmu, který vymyslela? To
je úkol podstatně těžší. Zkuste to však, ještě než si vyslechneme Ariadniny
argumenty.
Aithra: "Ó veliký Die, nedovol, by se můj syn Théseus, pýcha Athén a naděje celé Helady, nechal vlákat do léčky schystané dcerou zlořečeného krále Mínóa!"
Ariadna: "Sama poznáš, ó královno, že nejde o léčku. Théseus si může být jistý, že ho můj návod nezklame. Nikdy se nemůže dostat v Labyrinthu do situace, na kterou bych nepamatovala."
Aithra: To by mohl říci každý, ale přesvědč nás o tom!"
Ariadna: "Pokud v některé komnatě na Théseově cestě není splněna podmínka ani jedné z prvních tří situací, pak nemůže jít o komnatu Mínótaurovu. Navíc z této komnaty může vycházet nejvýše jedna žlutá chodba, jinak by přece šlo o situaci 'Smyčka', a nemůže z ní také vycházet žádná chodba zelená, jinak by šlo o situaci 'Zelená cesta'. Nejde-li o komnatu, ve které budu na Thésea čekat já, a nenastává-li tedy ani situace 'Ariadna', pak je splněna podmínka páté situace 'Slepá cesta'. Vskutku pak do této komnaty vede jediná žlutá chodba, kterou do ní Théseus přišel."
Aithra: "Musím přiznat, že to, co říkáš, zní přesvědčivě. Nemůže to však rozptýlit mé obavy. Co když bude podle tvého návodu Théseus bloudit v Labyrinthu věčně?"
Ariadna: "To se stát nemůže. Théseus totiž může každou chodbou projít nejvýše dvakrát. A to znamená, že se musí podle mého návodu zastavit nejpozději po počtu kroků rovném dvojnásobku počtu chodeb v bludišti."
Aithru
ani nenapadlo uvažovat o nekonečných bludištích, jak to dělají matematici
(pokud to nenapadlo ani vás, vůbec vám to nebude v tomto kurzu vadit),
proto se nezmohla na repliku.
Ariadna: "Navíc se může Théseus v každém okamžiku cítit zcela bezpečný, nit mu totiž bude vždy ukazovat přímou cestu zpět ke mně."
Aithra: "Snad k nám, ne? A co míníš tím, že ta cesta bude přímá, princezno?"
Ariadna: "Takovou cestu, která se nekříží sama se sebou."
Připomeňme
si, že v naší terminologii se chodby, kterými prochází nit, nazývají žluté. Ariadna
tedy tvrdí, že během celé práce jejího algoritmu tvoří žluté chodby v bludišti
cestu, která se sama se sebou nekříží a vede od Ariadny k Théseovi. Ale
přestaňme již zajímavě se rozvíjející dialog Ariadny s Aithrou rušit.
Aithra: "Hm, ale jak to můžeš s takovou jistotou vědět? Já vás Kréťany moc dobře znám a vím, že vám nelze věřit ani slovo!"
Ariadna: "Promiňte královno, že vás přerušuji, ale dovolte mi, abych vás o tom přesvědčila. Na počátku své pouti bude Théseus ve výchozí komnatě Labyrinthu s námi a celou nit bude mít ještě smotanou v ruce. Nit tedy bude doopravdy označovat Théseovi cestu k nám. V tomto případě bude tato cesta prázdná. Tak teď na Krétě říkáme podle nové koncepce ve školách cestám, které neobsahují ani jednu chodbu. A taková prázdná cesta se přece nemůže křížit!"
Aithra: "Hromovládný Die, ty to slyšíš a nezasáhneš? Prázdná cesta..., to bych v našich školách nikdy nedovolila! Ale dobře vám tak, Kréťané! Pokračuj, Ariadno!"
Ariadna: "Na začátku tedy nit označuje přímou cestu zpět. Za chvíli se přesvědčíme o tom, že když v nějakém okamžiku označuje nit přímou cestu zpět, pak můj návod dává záruku, že tomu tak bude i v okamžiku příštím, po provedení jednoho kroku tohoto postupu. Bude tedy nit vyznačovat přímou cestu zpět v každém okamžiku Théseovy pouti Labyrinthem, i v okamžiku, kdy nalezne Mínótaura."
Aithra: "To je jasné. Proč však tvůj postup zachovává existenci přímé cesty z výchozí komnaty k Théseovi, označené nití?"
Ariadna: "To je jednoduché. Pokud se Théseus v situaci 'Smyčka’ nebo 'Slepá cesta' vrací zpět, pak se tato cesta jenom zkrátí, smyčky na ní tedy přibýt nemohou. Dopředu může Théseus postupovat jen v situaci 'Zelená cesta', která však může nastat, jen nejsou-li splněny podmínky situace 'Smyčka’ . To ale znamená, že ani v situaci 'Zelená cesta' nemůže podle mého návodu k překřížení niti dojít. Zbývají pouze situace 'Mínótauros’ a ’"Ariadna’, promiňte královno, chtěla jsem říci ’Aithra a Ariadna', ale v těch se Théseus zastavuje a cesta se tedy nemění."
Aithra: "Myslíš, že mě ošálíš falešnými lichotkami, ale to se mýlíš. I když jsem ti, ó bohové, uvěřila všechno, cos dosud říkala! Jak však můžeš zaručit, že Théseus Mínótaura v bludišti podle tvého návodu skutečně najde? Co když se zastaví u nás, v situaci ’Ariadna ’, jak jsi ji domýšlivě nazvala?"
Ariadna: "Théseus by se mohl zastavit v situaci 'Ariadna' jen v případě, že by v Labyrinthu neexistovala žádná cesta vedoucí z výchozí komnaty, kde na něj budeme čekat, k Mínótaurovi."
Aithra: "Jako bych Théseovi neříkala, že ta zrůda nemusí vůbec existovat! I když tvé matce Pásifaé je to tak podobné ..."
Ariadna: "Prosím vás, nyní mne nepřerušujte, královno. Naše další úvahy budou složitější, proto vás prosím o zvýšenou pozornost."
Aithra: "Vždyť již poslouchám."
Ariadna: "Nenajde-li Théseus Mínótaura, musí se nakonec zastavit v situaci 'Ariadna'. V okamžiku zastavení nemohou být v bludišti žádné žluté chodby. Kdyby v Labyrinthu zůstaly některé chodby žluté, pak by se Théseus nenalézal v situaci ’Ariadna ’, ale v situaci ’Smyčka’, a nemohl by se tedy ještě zastavit."
Ariadna: "Jestliže ale Mínótauros v Labyrinthu opravdu je, existuje cesta z naší výchozí komnaty k němu. Při svém hledání navštívil Théseus z této cesty jistě alespoň jednu komnatu - tu naši výchozí. Protože teď předpokládáme, že Théseus Mínótaura nenašel, nemohl navštívit všechny komnaty na této cestě. Nazvěme nejvzdálenější komnatu na této cestě, kterou Théseus navštívil, osudovou. V ní musel sejít ze správné cesty. Stačíte mne sledovat, královno?"
Aithra: "O mne se, princezno, neboj. A pokračuj!"
Ariadna: "Protože osudová komnata je poslední komnatou, kterou Théseus na dané cestě navštívil, zůstala alespoň jedna z chodeb z ní vedoucích ještě v době Théseova zastavení u nás zelená. Položme si otázku, v jaké situaci se Théseus nalézal, když byl v této komnatě naposledy. Tento okamžik můžeme také nazvat osudovým. Jistě v té chvíli nebyl v situaci ’Mínótauros', nemohl však být ani v situaci ’Smyčka', protože pak by se musel do této komnaty ještě jednou vrátit. V osudovém okamžiku byly tedy splněny podmínky situace ’Zelená cesta' a Théseus naposledy odešel z osudové komnaty zelenou chodbou a tak změnil její barvu na žlutou. My však již víme, že v okamžiku zastavení Thésea v situaci ’Ariadna’ nezbyly v Labyrinthu již žádné žluté chodby. Musel se tedy Théseus touto chodbou vrátit do osudové komnaty po osudovém okamžiku ještě jednou. A to není možné!"
Aithra (k Théseovi): "Tak vidíš, sama se přiznává, že mluví nesmysly!"
Ariadna:
"Nemluvím nesmysly. Jen jsem vám
ukázala, že není možné, aby se v případě, že v Labyrinthu existuje cesta k
Mínótaurovi, Théseus zastavil v situaci ’Ariadna ’. A to dokazuje, že můj návod je správný!"
Opustíme vzrušený dialog obou žen v okamžiku, kdy je, alespoň nám, už zcela jasné, že Ariadna musí vyhrát.
Možná se vám zdála motivace potřeby důkazu správnosti Ariadnina algoritmu přítomností Aithry poněkud nepřirozená. Nevedly nás k tomu vůbec důvody "literární", ale především metodické. Při programování se vám bude velmi hodit schopnost "zahrát si na vlastního nepřítele". Nepříteli se totiž hledají chyby v našich programech vždy snadněji, protože z nich má radost.
Ariadnin
algoritmus pro hledání v bludišti je jedním ze speciálních případů velmi
důležité obecné metody algoritmického vyhledávání, kterou můžeme nazvat třeba "prohledávání
s návratem". Protože všeobecně přijímaný český název pro ni není k
dispozici, uvádíme anglický název, pod nímž ji najdete i v české odborné
literatuře - backtracking.
Hlavní myšlenku této metody můžeme bez nároku na přesnost shrnout do jednoduchého návodu:
"Na kaŽdÉm rozcestÍ, na kterÉ pŘijdeŠ, zjisti
vŠechny moŽnÉ cesty, jimiŽ lze pokraČovat, vyber si jednu z nich a ostatní si
zapamatuj. tÍmto způsobem postupuj kupŘedu tak dlouho, dokud to jde nebo dokud
se nedostaneŠ do situace, ve kterÉ jsi jiŽ byl. nemůŽeŠ-li uŽ dÁl, vraŤ se na
poslednÍ rozcestÍ, kde ses rozhodoval, a vyber si jinou cestu (kterou jsi dosud
neŠel)."
V Ariadnině algoritmu se výběr cesty provádí ve stavu ’Zelená cesta’, návrat zpět ve stavech ’Smyčka’ a ’Slepá cesta’. Ve stavech ’Mínótauros’ a ’Ariadna ’ činnost algoritmu končí, protože jsme v obou těchto případech dosáhli cíle.
V
Théseově úloze jsme použili metody prohledávání s návratem pro hledání jedné
cesty. Kdybychom se však v případech, kdy jsme již nějakou cestu do cíle
nalezli, nezastavili, ale vraceli se, mohli bychom pomocí této metody najít
všechny cesty.
Využitím metody prohledávání s návratem lze poměrně snadno navrhnout algoritmy pro řešení široké třídy úloh. Velikou společnou nevýhodou těchto algoritmů však je velká časová náročnost výpočtů, ke kterým vedou. Proto se těchto algoritmů užívá především v případech, kdy o prostoru, v němž hledáme, skoro nic nevíme, a nemůžeme tedy použít svých znalostí o něm k urychlení hledání.
Abychom si myšlenku metody lépe zapamatovali, stačí si uvědomit, že nejde vlastně o nic jiného než o starou a osvědčenou metodu namlouvání z Moravského Slovácka, kterou nám naši předkové odkázali prostřednictvím sloganu:
"Hr na nĚ, a kdyŽ to nepojde, toŽ cÓfnem!"
Ať se nám
to líbí nebo ne, počítače pronikají do stále širších sfér života společnosti.
Tak se postupně stává stále více věcí v životě každého z nás i v životě lidstva
jako celku závislých na správné funkci mnoha algoritmů, podle nichž počítají.
Proto je dnes problematika ověřování správnosti algoritmů (a programů, které
jsou jejich vyjádřením v programovacím jazyce) tak důležitá, někdy doslova
životně.
Vzpomeňte si jen, kolikrát jste se v novinách či v televizi setkali se zprávou o poruše dopravní, kosmické či vojenské techniky vinou chyby v řídícím programu.
Ani my
jsme se proto nemohli těmto otázkám vyhnout.
Základní metody důkazů správnosti
Pro dokazování správnosti algoritmu neexistuje - a asi ani nemůže existovat - žádná univerzální metoda zaručující úspěch. Teoreticky byla rozpracována celá řada metod. Většinu z nich však nemá smysl detailně vykládat v knize, jako je naše. Proto se soustředíme na některé hlavní myšlenky z této problematiky. Můžeme při tom vyjít z postupu, kterým v části 1.6 dokazovala Ariadna správnost svého algoritmu v rozhovoru s Aithrou.
Abychom se dobrali obecněji platných metod, opustíme beletristickou formu výkladu a budeme se snažit o přesnější vyjadřování. Mějte však
na paměti, že pojmy, které si zavedeme, jsou jen nástroje. I když je použití vhodných nástrojů velmi důležité, jak může dosvědčit každý, kdo se pokoušel jíst polévku vidličkou a nožem, nesmíme pro nástroje samé nikdy zapomenout na podstatu věci, která je na nich do značné míry nezávislá.
Nejprve Ariadna přesvědčila Aithru o tom, že její algoritmus je korektní. To znamená, že při jeho návrhu neopomenula žádnou z možností, které mohou během výpočtu nastat. Taková opomenutí totiž patří mezi nejčastější chyby, jichž se při návrhu algoritmu dopouštějí začátečníci.
Na vlastním důkazu správnosti algoritmu bylo zajímavé především to, jak šikovně ho Ariadna rozčlenila na nezávislé důkazy několika jednodušších tvrzení. Taková schopnost rozdělit obtížný úkol na postupné provedení úkolů jednodušších je základem úspěchu v programování (a zdaleka nejen v něm).
První takové rozdělení vzniklo z následující jednoduché úvahy: Algoritmus je nesprávný, pokud jeho výpočet na některých přípustných datech buď vůbec neskončí ("zacyklí se"), nebo sice skončí, ale s nesprávným výsledkem. K důkazu správnosti tedy stačí ukázat, že nemůže nastat ani jeden z těchto případů. To nás vede k zavedení dvou pojmů.
Budeme říkat, že algoritmus má vlastnost konečnosti, jestliže jeho výpočet pro každá přípustná vstupní data skončí.
Budeme říkat, že algoritmus je částečně správný, jestliže se nemůže stát, že by jeho výpočet na některých přípustných vstupních datech skončil se špatným výsledkem. Jinak řečeno, jestliže výpočet skončí, pak skončí se správným výsledkem.
Povšimněte si, že v definici částečné správnosti se neříká nic o tom, zda výpočet algoritmu skončí, nebo ne. Částečně správný je tedy i takový algoritmus, jehož výpočet neskončí na žádných vstupních datech.
Rozmyslete si, že algoritmus, který má současně obě tyto vlastnosti, skutečně musí být správný.
Metoda, které Ariadna užila pro důkaz konečnosti svého algoritmu, je natolik důležitá a široce použitelná, že ji zformulujeme jako obecný návod.
K DŮKAZU KONEČNOSTI ALGORITMU STAČÍ NAJÍT ZPŮSOB, KTERÝ OHODNOCUJE
KAŽDÝ STAV VÝPOČTU PŘIROZENÝM ČÍSLEM,
A UKÁZAT, ŽE VŽDY PO PROVEDENÍ JEDNOHO
KROKU ALGORITMU (NEBO NĚKOLIKA JEHO KROKŮ) SE HODNOTA TOHOTO OHODNOCENÍ ZMENŠÍ.
Pak skutečně musí každý výpočet algoritmu skončit, protože jinak by ohodnocení stavů tvořila nekonečnou klesající posloupnost přirozených čísel.
Ariadnin způsob důkazu konečnosti jejího algoritmu lze vyjádřit v této formě.
"Stav výpočtu" je v tomto případě reprezentován obarvením chodeb v Labyrinthu. Ohodnoťme každou z chodeb přirozeným číslem podle její barvy: zelené chodby číslem 2, žluté číslem 1 a červené nulou (toto ohodnocení vlastně říká, kolikrát ještě Théseus může danou chodbou projít). Celkové ohodnocení bludiště pak definujeme jako součet ohodnocení všech jeho chodeb. V každém kroku Ariadnina algoritmu se pak změní barva jedné z chodeb tak, že se její ohodnocení zmenší o jedničku, zmenší se tedy o jedničku i ohodnocení bludiště.
Dalším důležitým pojmem, který se můžeme z Ariadnina postupu důkazu naučit, je pojem invariantu.
Ariadna dokázala najít podmínku, která je splněna během celé cesty Thésea Labyrithem. Bylo to tvrzení, že
(1) "ŽlutÉ chodby v bludiŠti tvoŘÍ cestu od Ariadny k ThÉseovi, NavÍc na tÉto cestĚ nejsou ŽÁdnÁ kŘÍŽenÍ."
Taková tvrzení, která platí "během celého výpočtu algoritmu" (později uvidíme, proč jsme to napsali v uvozovkách), patří k nejcennějším informacím, které můžeme o algoritmu získat. Proto se vám vyplatí, zvyknete-li si zaznamenávat si všechny netriviální invarianty svých algoritmů, na které jste přišli. Sami uvidíte, kolika nepříjemnostem se tím při tvorbě programů můžete vyhnout.
Na závěr zformulujme logickou stavbu Ariadnina důkazu částečné správnosti jejího algoritmu v terminologii, které jsme se právě naučili:
1. Nalezení a důkaz invariantu (1).
2. Důkaz toho, že zastaví-li se Théseus u Ariadny, nemůže v Labyrinthu existovat cesta k Mínótaurovi.
3. Tím je důkaz dokončen, protože podle definice algoritmu se Théseus může zastavit buď u Mínótaura (a pak se podle dokázaného invariantu může vrátit zpět k Ariadně po "žluté cestě" bez křížení) nebo u Ariadny (pak ovšem nemůže být Mínótauros v Labyrinthu).
Nejdůležitější ponaučení, které byste si z celého povídání o důkazu správnosti Ariadnina algoritmu měli odnést, jsme si úmyslně nechali až na konec. Možná ale, že jste na něj už přišli sami.
PotŘebu ovĚŘenÍ sprÁvnosti algoritmu je nutnÉ mÍt na zŘeteli od samÉho poČÁtku pracÍ na jeho nÁvrhu.
Zkušenost učí, že práce, kterou při takovém návrhu algoritmu vynaložíme "navíc", se vůbec neztratí. Naopak, většinou si tak práci dokonce ušetříme. A to i v případech, kdy formální důkaz správnosti nebudeme provádět.
Snahy o
ověření správnosti algoritmu navrženého bez tohoto zřetele jsou většinou
odsouzeny k neúspěchu a pokud "náhodou" vedou k cíli, pak je za to
třeba zaplatit vynaložením neúměrného úsilí.