Haltavimo (sustabdymo) problema: apibrėžimas, įrodymas ir pasekmės
Haltavimo (sustabdymo) problema: kas tai, kodėl neįmanoma ją išspręsti, įrodymas ir pasekmės kompiuterių moksle — aiškus paaiškinimas ir pavyzdžiai
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.
Klausimai ir atsakymai
K: Kas yra Haltingo problema?
A: Haltingo problema yra informatikos problema, nagrinėjanti kompiuterio programą ir nustatanti, ar programa veiks amžinai, ar ne.
K: Kaip sužinoti, ar programa išsprendžia Haltingo problemą?
Atsakymas: Sakome, kad programa "sprendžia sustabdymo problemą", jei ji gali pažvelgti į bet kurią kitą programą ir pasakyti, ar ta kita programa veiks amžinai, ar ne.
K: Ar yra būdas įrodyti, kad tokios programos nėra?
A: Taip, parodant, kad jei tokia programa egzistuotų, įvyktų kažkas neįmanomo. Šį įrodymą 1936 m. rado Alanas Tiuringas (Alan Turing).
K: Ką daro P?
A: P yra funkcija, kuri įvertina kitą funkciją F (iškviestą su argumentu I) ir grąžina true, jei ji veikia amžinai, ir false priešingu atveju.
K: Ką daro Q?
A: Q nagrinėja kitą programą ir atsako į klausimą, ar paleidus tą pačią programą ant jos pačios, susidarys begalinė kilpa. Ji tai daro naudodama P, kad įvertintų duotąją funkciją F.
K: Ką daro R?
Atsakymas: R žiūri į kitą programą ir prašo Q atsakyti į klausimą apie tą konkrečią programą. Jei Q atsako "taip, jei paleisime šią programą ir priversime ją žiūrėti į savo kopiją, ji veiks amžinai", R sustoja; tačiau jei Q atsako "ne, jei paleisime šią programą ir priversime ją žiūrėti į savo kopiją, ji neveiks amžinai", R įeina į begalinį ciklą ir veikia amžinai.
Klausimas: Kas atsitinka, kai priverčiame R pažvelgti į save?
Atsakymas: Gali atsitikti du dalykai - arba R sustoja, arba veikia amžinai, tačiau abu rezultatai yra neįmanomi pagal tai, kas buvo įrodyta, kad tokios programos kaip P neegzistuoja, taigi kažkas kažkur pakeliui, kol privertėme R pažvelgti į save, turėjo būti negerai.
Ieškoti