Haltingo (sustabdymo) problema – tai klausimas, ar egzistuoja bendra procedūra (programa), kuri bet kuriai duotai programai ir jos įėjimui galėtų tiksliai nusakyti, ar ta programa galiausiai sustos (sustos vykdymą), ar veiks amžinai. Kitaip tariant, ar galima parašyti programą P, kuri gauna programos F ir įėjimo I aprašymą ir grąžina true, jei F su I sustoja, ir false, jei F su I niekada nesustoja.

Papildomi pavyzdžiai

Aiškiai pamatyti skirtumą tarp amžinai veikiančios ir greitai sustojančios programos padeda paprasti pavyzdžiai:

while True:     continue  # ciklas tęsis amžinai  while False:     continue  # šis ciklas iš karto praleidžiamas ir programa greitai sustoja

Formalus teiginys

Formaliai: haltingo problema klausia, ar egzistuoja algoritmo P(F, I), kuris išvestų teisingą atsakymą "sustoja" arba "nesustoja" visiems poroms (F, I). 1936 m. Alanas Tiuringas. parodė, kad toks universalus algoritmas neegzistuoja — problema yra neapsprendžiama (undecidable).

Įrodymo idėja (įrodymas pagal prieštaravimą)

Įrodymas remiasi prieštaravimo konstrukcija ir savireferencijos idėja. Tarkime, kad egzistuoja P, kuris teisingai nusprendžia sustojimą:

def P(F, I):     # grąžina True, jeigu F( I ) sustoja; False priešingu atveju     ...

Naudodami tokį P, sukuriame naują programą D (diagonalizuojančią programą), kuri elgiasi taip:

def D(F):     if P(F, F):         # jei F, paleista su savo pačiu aprašymu, sustos         while True:             continue    # tada D įeina į begalinį ciklą (nesustoja)     else:         return          # kitaip D sustoja

Dabar pažiūrėkime, kas nutiks, kai paleisime D su pačia savimi kaip įėjimu, t. y. apsvarstykime D(D).

  • Jeigu P(D, D) teigia, kad D(D) sustos, pagal D aprašymą D(D) turėtų pradėti begalinį ciklą ir nesustoti. Tai prieštarauja P prognozei.
  • Jeigu P(D, D) teigia, kad D(D) nesustos, pagal D aprašymą D(D) turėtų sustoti. Irgi prieštaravimas.

Taigi abu variantai sukelia prieštaravimą. Vienintelis šios paradoksalios situacijos paaiškinimas yra tas, kad pradinis prielaidavimas — esanti visapusiškai teisinga programa P, nusakanti sustojimą visiems įėjimams — yra klaidingas. Iš to seka: universalaus sprendimo haltingo problemai nėra.

Svarbūs pastebėjimai

  • Haltingo problema yra neapsprendžiama (undecidable): nėra algoritmo, kuris visiems įmanomiems programų aprašymams ir įėjimams pateiktų galutinį teisingą atsakymą „sustoja“ arba „nesustoja“.
  • Tačiau problema yra iš dalies pažįstama (semi-decidable / Turing-recognizable): galime sukurti programą, kuri imituoja (simuliuoja) F su I; jei F sustoja, simuliatorius kada nors aptiks sustojimą ir praneš; jeigu F niekada nesustos, simuliatorius taip pat niekada nebaigs — tad galime patikimai atpažinti tik sustojimo atvejus, bet negalime patikimai atpažinti „niekada nesustos“ atvejų.
  • Ši neapsprendžiamumo savybė pasireiškia daugelyje kitų uždavinių: pagal Rice'o teoremą, bet kuri neminimomo pobūdžio (non-trivial) savybė apie programų funkcionalumą yra neapsprendžiama. Tai reiškia, kad daugelio programų savybių (pvz., „ar programa išskaičiuoja konkrečią funkciją?“, „ar programa turi tam tikrą semantikos savybę?“) negalima patikrinti universalia procedūra.

Praktinės pasekmės

Nors haltingo problema rodo, kad neegzistuoja absoliutus automatinis būdas patikrinti bet kurios programos sustojimą, tai netrukdo turėti daug naudingų įrankių praktikoje:

  • Statinė analizė, tipų sistemos ir formalių metodų įrankiai veikia apribotose programų kalbose arba pateikia konservatyvius (galbūt klaidingus) įspėjimus — jie neapsprendžiami visiškai, bet praktiškai naudingi.
  • Yra specialūs terminacijų įrodymai ir įrankiai (termination provers), kurie gali įrodyti sustojimą tam tikroms programų klasėms (pvz., rekurencinėms funkcijoms su tam tikromis sąlygomis), tačiau jie negali apimti visų galimų programų.
  • Haltingo problemos neapsprendžiamumas taip pat riboja automatinį programų korektiškumo įrodymų apimtį — tam tikrus klausimus apie elgesį ir savybes reikia spręsti per apribojimus ar žmogaus įsikišimą.

Istorinis kontekstas

Šį įrodymą 1936 m. pateikė Alanas Tiuringas. Jis parodė, kad tam tikros skaičiavimo problemos yra esminiu būdu neapsprendžiamos, o tai turėjo gilų poveikį teorinei kompiuterių mokslo krypčiai — formaliems modeliams (Turingo mašina), algoritmų riboms ir skaičiavimo teorijai.

Apibendrinant: haltingo problema rodo, kad egzistuoja fundamentiniai apribojimai automatinėms metodikoms nustatyti programų elgesį: nėra bendro algoritmo, galinčio teisingai nuspręsti, ar bet kuri programa su bet kokiu įėjimu kada nors sustos.