Problém zastavenia (Haltingov problém): definícia a Turingov dôkaz

Haltingov problém: jasné vysvetlenie definície a Turingovho dôkazu, prečo neexistuje univerzálny rozhodovač programov. Príklady a dôkaz krok za krokom.

Problém zastavenia je základný problém v informatike a teorii výpočtovosti. Spočíva v tom, že máme na vstupe popis programu (alebo Turingovho stroja) a jeho vstup a chceme rozhodnúť, či tento program na danom vstupe niekedy skončí (zastaví sa), alebo bude bežať večne. Hovoríme, že program „rieši problém zastavenia“, ak pre ľubovoľný pár (program, vstup) dokáže v konečnom čase povedať „zastaví sa“ alebo „nebude sa zastavovať“.

Napríklad nasledujúce dve ukážky jasne rozlišujú prípady:

while True: pokračovať;

tento program sa bude opakovať donekonečna, zatiaľ čo

while False: pokračovať;

sa okamžite zastaví. Otázka však znie, či existuje všeobecný algoritmus, ktorý by pre akýkoľvek program a akýkoľvek vstup spoľahlivo povedal, či sa program zastaví.

Formálna idea dôkazu (Turingov dôkaz)

Ukážeme (metódou sporu), že takýto všeobecný program neexistuje. Predstavme si, že existuje program P, ktorý pre ľubovoľný program F a vstup I odpovie true práve vtedy, keď F spustené na vstupe I beží večne (inak odpovie false). Formálne:

def P(F, I):     if F(I) runs forever:         return True     else:         return False

P je teda hypotetický „rozhodovač“ problému zastavenia (v texte sa zameriavame na verziu, ktorá vracia True pre nekončiace behy; rovnaká logika funguje pri opačnej definícii).

S využitím P si zostrojíme ďalší program Q, ktorý jednoducho vyhodnotí P na páre (F, F) — teda pýta sa, či program F na vlastnom popise ako vstupe beží večne:

def Q(F):     return P(F, F)

Teraz definujeme program R, ktorý pre ľubovoľný program F urobí presný opak toho, čo predpovie Q(F):

def R(F):     if Q(F):         return   # okamžite sa zastaví     else:         while True:             continue   # beží večne

R teda končí práve vtedy, keď Q(F) odpovedá, že F na sebe beží večne; a naopak, R beží večne práve vtedy, keď Q(F) tvrdí, že F na sebe bežať večne nebude.

Samokontradikcia (klasická diagonálna argumentácia)

Teraz uvažujme, čo sa stane, ak spustíme R s vlastným popisom ako vstup, teda R(R).

• Predpokladajme, že R(R) sa zastaví. Podľa definície R to znamená, že vtedy Q(R) vrátilo True (t. j. P(R,R) tvrdí, že R(R) beží večne). Ale ak Q(R) tvrdí, že R(R) beží večne, potom podľa definície R by R(R) nemal končiť — spor.
• Predpokladajme naopak, že R(R) beží večne. Potom podľa definície R musí byť Q(R) False (t. j. P(R,R) tvrdí, že R(R) sa nezastaví). Ale ak Q(R) tvrdí, že R(R) sa nezastaví, potom podľa definície R by sa R(R) mal zastaviť — opäť spor.

V oboch prípadoch dostaneme rozpor. Jediný predpoklad, ktorý sme pri dôkaze urobili a ktorý môže byť chybný, je existencia programu P, teda že existuje algoritmus, ktorý rozhodne, či ľubovoľný program na ľubovoľnom vstupe beží večne alebo sa zastaví. Preto takýto algoritmus neexistuje.

Záver: Neexistuje všeobecný program, ktorý by rozhodoval problém zastavenia. Tento výsledok prvý dokázal Alan Turing v roku 1936; dôkaz využíva diagonálnu Konštrukciu a metódu sporu.

Dôsledky a rozšírenia

• Neurčiteľnosť vs. rozpoznateľnosť: Hoci problém zastavenia nie je rozhodnuteľný (nie je možné vždy povedať áno/nie v konečnom čase), existuje čiastočné riešenie: simulátor, ktorý spustí testovaný program na danom vstupe a ak simulácia skončí, vráti „zastavil sa“. Ak simulácia nikdy neskončí, náš simulátor tiež nikdy nevráti odpoveď. Preto množina párov (program, vstup), kde program skutočne zastaví, je rekurzívne spočítateľná (semi-decidable), ale jej doplnok nie je.
• Dôsledky v praxi: Z teoretického hľadiska to znamená, že neexistuje univerzálny statický analyzátor, ktorý by dokázal pre všetky programy spoľahlivo rozhodnúť, či sa niekde v budúcnosti zastavia. V praxi sa preto používajú heuristiky, obmedzenia jazyka alebo overovacie techniky, ktoré fungujú iba pre konkrétne triedy programov.
• Generalizácie: Riceova veta hovorí, že akákoľvek neverejná (netriviálna) vlastnosť správania programu je neurčiteľná — to je silnejší, všeobecnejší výsledok než jednotlivý halting proof. Turingov prístup je tiež spojený s Cantorovou diagonálnou myšlienkou a súvisí s Gödelovými vetami o neúplnosti.

Krátke zhrnutie

• Problém zastavenia: rozhodnúť, či program na danom vstupe skončí alebo bude bežať večne.
• Turing dokázal, že neexistuje algoritmus, ktorý by tento problém vyriešil pre všetky programy a vstupy.
• Problém je však čiastočne rozpoznateľný: simulácia „objaví“ ukončenia, ale nikdy nedokáže dôkaz, že daný program beží večne.

Otázky a odpovede

Otázka: V čom spočíva problém Halting?

Otázka: Ako zistíme, či program rieši problém zastavenia?

Otázka: Dá sa nejako dokázať, že takýto program neexistuje?

Otázka: Čo robí program P?

Otázka: Čo robí Q?

Otázka: Čo robí R?

Otázka: Čo sa stane, keď prinútime R pozrieť sa na seba?

Hľadajte podľa písmena