Halting problem

Jednou z věcí, které dnes velmi trápí snad všechny producenty softwaru, je kvalita jejich produktů - neboli otázka, zda skutečně dělají to, co dělat mají. Softwarový průmysl se s tímto problémem vyrovnává nejčastěji cestou testování (různých alfa- a beta-verzí), což ovšem ne vždy přináší kýžené výsledky - jak dokazují četné chyby, které se objevují i ve finálních verzích komerčních produktů. Jak by se asi všem ulevilo, kdyby existovala nějaká možnost formálního ověření správnosti programů, schopná podat pádný a nezvratný důkaz o tom, že určitý program je v pořádku, neobsahuje žádné chyby a skutečně "dělá to, co dělat má".

Je asi přirozené, že stejná otázka napadla i lidi, kteří se počítači zabývají po teoretické stránce. Ti ale bohužel zjistili, že nic takového neexistuje a v principu ani existovat nemůže. Tedy že nikdy nebude existovat prostředek, který by o libovolném programu dokázal s určitostí zjistit, zda je správný či nikoli. Jak ale k tomuto závěru došli?

Na pomoc si vzali jeden z možných abstraktních modelů počítače, Turingův stroj, o kterém je známo, že je "stejně tak silný jako kterýkoli počítač" (viz minulý díl této rubriky). Na něm začali nejprve hledat odpověd na poněkud jednodušší otázku: je možné vždy rozhodnout o tom, zda se kterýkoli Turingův stroj zastaví? Neboli, převedeno zpět do světa reálných počítačů: je možné rozhodnout o tom, zda výpočet kteréhokoli programu skončí v konečném čase, nebo nikoli?

Tento zajímavý problém dostal i své vlastní jméno: halting problem neboli problém zastavení (míněno: zastavení Turingova stroje). Bohužel se však ukázalo, že nemá řešení. Přesněji že není algoritmicky rozhodnutelné, zda se libovolný Turingův stroj (alias počítač s libovolným programem) v konečném čase zastaví, či nikoli.

Tomuto výsledku je ovšem třeba správně rozumět. Říká totiž, že nikdy nebude existovat algoritmus, který by problém zastavení Turingova stroje řešil pro libovolný program (resp. pro libovolný Turingův stroj). Tím ovšem není vyloučeno, aby takovýto algoritmus existoval pro určitou podmnožinu všech možných programů (Turingových strojů) - neexistuje pouze takový, který by byl jeden a fungoval spolehlivě pro jakýkoli program.

Jestliže ale nebude nikdy z principu možné rozhodnout o tom, zda libovolný program vůbec někdy dopočítá a skončí, pak zcela jistě nebude možné rozhodnout ani o tom, že to, co vypočítá bude správné. No a právě to je ona záporná odpověď všem, kteří volají po možnosti formálního dokazování správnosti programů. Znovu je ale třeba této odpovědi správně rozumět: nikdy nebude existovat prostředek, který by dokázal rozhodnout o správnosti libovolného programu. To samozřejmě neznamená, že by nebylo možné formálně dokázat správnost některých speciálních programů - dnes dokonce existuje celá vědní disciplína, která se dokazováním správnosti (neboli tzv. verifikací) programů zabývá. Zatím jde ale spíše o akademickou záležitost, která nemá větší vliv na tvrdou realitu softwarového trhu.