Problém zastavení: neřešitelnost, důkaz a důsledky

Co přesně znamená problém zastavení

Formálně se jedná o rozhodovací problém: vezmeme kód programu P a konkrétní vstup I; chceme rozhodnout pravdivost výroku "P spuštěné s I se nakonec zastaví". Kdyby existoval algoritmus H, který by na každé dvojici (P,I) vždy v konečném čase odpověděl "ano" (zastaví se) nebo "ne" (neběží nikdy), říkáme, že problém zastavení je řešitelný. Turing ukázal, že takový univerzální rozhodovač H neexistuje.

Stručný náčrt důkazu neřešitelnosti

Důkaz je založený na technice diagonální samoodkaznosti a argumentu sporem (redukcí). Předpokládejme pro účely sporu, že existuje program H, který rozhoduje zastavení: H(P,I) vrací pravdu, když P spuštěné s I běží věčně, nebo nepravdu v opačném případě (formulace může být přizpůsobena, důležitá je představa rozhodovače). Z tohoto předpokladu se dá sestrojit nový program S, který interpretuje chování H proti sobě samému a chová se opačně než H předpovídá. S přijímá jako vstup kód programu X a provede následující: zavolá H(X,X) a pokud H tvrdí, že X spuštěné s X poběží věčně, S se zastaví; pokud H tvrdí, že X spuštěné s X se zastaví, S vstoupí do nekonečné smyčky.

Co se stane, pokud S dostane svůj vlastní kód jako vstup? Vyvolá se paradox: pokud S(S) poběží věčně, pak podle definice S chce udělat opak toho, co H předpovídá, a tedy by se zastavil; pokud se S(S) zastaví, pak podle definice by měl běžet věčně. Obě možnosti vedou ke sporu, takže počáteční předpoklad (existence H) je nesprávný. Tento typ konstrukce ukazuje, že žádný algoritmus nemůže univerzálně rozhodnout zastavení pro všechny programy a všechny vstupy.

Historie a souvislosti

Tento výsledek formálně odvodil Alan Turing ve své práci z roku 1936, která také položila základ pro pojem Turingova stroje jako matematického modelu výpočtu. Pokud potřebujete základní orientaci v literatuře nebo dalších zdrojích, viz obecné přehledy teorie výpočtů a historické studie o Turínově práci či učebnice teorie algoritmů a rekurzivity zaměřené na počítačovou vědu.

Důsledky a související výsledky

• Neřešitelnost dalších vlastností: Z neexistence rozhodovače pro zastavení plyne, že mnohé jiné otázky o obecném chování programů jsou rovněž nerozhodnutelné. Například nelze obecně rozhodnout, zda program nikdy nepoužije určitou proměnnou nebo zda vždy vypočítá určitou funkci — neexistuje univerzální metoda pro netriviální sémantické vlastnosti programů.
• Částečné (semi-)rozhodování: Halting problem je rekurzivně vyčíslitelný (enumerable) v jednom směru: existuje simulační postup, který, pokud program skutečně skončí, dokáže to potvrdit (simulací do konce), ale pokud program neběží nikdy, takový postup může běžet věčně a nedá odpověď. To znamená, že "zastavení" je částečně rozhodnutelné, zatímco jeho negace ne.
• Praktické nástroje: V praxi existují automatizované metody, které umějí odhalit mnoho případů neukončení nebo naopak dokázat ukončení — terminace se řeší pomocí speciálních důkazních technik, metrik, abstrakcí a heuristik. Žádný z těchto nástrojů ale nemůže pokrýt všechny možné programy.

Příklady, které ilustrují problém

Jednoduché programy ukazují, jak snadno lze napsat verifikovatelně ukončující i zjevně neukončující kód: program s cyklem "while True: continue" se nikdy nezastaví, zatímco "while False: continue" se zastaví okamžitě. Komplikace nastávají u programů, které závisí na hodnotách výpočtů, rekurzi, nebo na chování jiných programů — právě to dělá obecné rozhodnutí nemožným. Konstrukce použitá v důkaze využívá schopnosti programu analyzovat a spouštět jiné programy (nebo sebe sama), což vede ke samoopakovacím paradoxům.

Závěr a význam pro informatiku

Problém zastavení představuje jeden z nejdůležitějších a nejznámějších příkladů limitů formálních systémů v informatice. Ukazuje, že existují přesně definovatelné otázky o výpočtech, na které nelze najít algoritmické odpovědi. Tento poznatek ovlivnil vývoj teorie programovacího jazyka, verifikačních metod, bezpečnosti a porozumění tomu, co lze a co nelze automatizovat. I přesto, že nelze sestavit univerzální rozhodovač, praktické techniky stále umožňují řešit řadu důležitých konkrétních případů a odhalit hranice automatické analýzy programů.