Problém zastavení

Z Wikipedie, otevřené encyklopedie

Problém zastavení (halting problem) je úloha teorie vyčíslitelnosti, která může být neformálně zadána takto:

Znáte-li zdrojový kód programu a jeho vstup, rozhodněte, zda program zastaví, nebo zda poběží navždy bez zastavení.

V roce 1936 Alan Turing dokázal, že obecný algoritmus, který by řešil problém zastavení pro všechny vstupy všech programů, neexistuje. Problém zastavení se proto označuje jako algoritmicky nerozhodnutelný problém.

[editovat] Náčrt důkazu

Nerozhodnutelnost problému zastavení lze dokázat sporem.

Počáteční předpoklad: Předpokládejme, že problém zastavení lze rozhodnout. To znamená, že existuje nějaký program Zastaví(program, vstup), který je univerzálním řešením problému zastavení.
Ten funguje tak, že pokud volání program(vstup) po konečném počtu kroků skončí, pak Zastaví(program, vstup) vrátí hodnotu ANO, v opačném případě (pokud by se volání program(vstup) zacyklilo) vrátí hodnotu NE.
Zkonstruujme program Paradox(x), který se záměrně zacyklí, pokud volání programu Zastaví(x, x) vrátí ANO, a zastaví se, pokud volání programu Zastaví(x, x) vrátí NE.
Nyní se ptejme, co je výsledkem volání Paradox(Paradox).
Předpokládejme na chvíli, že Zastaví(Paradox, Paradox) vrací ANO. Z definice programu Paradox pak víme, že se Paradox(Paradox) zacyklí. Podle definice programu Zastaví ale platí, že pokud Paradox(Paradox) zacyklí, pak musí Zastaví(Paradox, Paradox) vracet NE. Došli jsme ke sporu.
Předpokládejme na druhou stranu na chvíli, že Zastaví(Paradox, Paradox) vrací NE. Z definice programu Paradox pak víme, že se Paradox(Paradox) zastaví. Podle definice programu Zastaví ale platí, že pokud Paradox(Paradox) zastaví, pak musí Zastaví(Paradox, Paradox) vracet ANO. Opět jsme došli ke sporu.
Protože jsme vyčerpali všechny možnosti a vždy došli ke sporu, musí být nepravdivý počáteční předpoklad. Z toho vyplývá, že program Zastaví(program, vstup), tak jak byl definován, neexistuje.