În teoria calculabilității, problema opririi este problema de a determina, din descrierea unui program de calculator arbitrar, și din intrarea lui, dacă programul va termina de rulat, sau va rula la nesfârșit. Problema opririi este , adică nu există niciun algoritm general care să o rezolve pentru orice pereche posibilă program–intrare. Problema apare adesea în discuțiile pe tema întrucât demonstrează că unele funcții sunt matematic dar nu sunt calculabile.
O parte esențială a formulării formale a problemei este definiția matematică a calculatorului și a programului, care de obicei se face prin intermediul formalismului denumit mașină Turing. Demonstrația arată apoi că, pentru orice program care ar putea determina dacă programele se opresc, atunci există un program „patologic” pentru care face o determinare incorectă. Anume, este programul care, atunci când este apelat cu o oarecare intrare, își dă mai departe propria sursă, împreună cu intrarea, lui f și face exact opusul a ceea ce va prevedea că face . Comportamentul lui asupra lui demonstrează indecidabilitatea, deoarece el înseamnă că niciun program nu va rezolva problema opririi în orice caz posibil.
Context Problema opririi este problema de decizie despre proprietățile unui program de calculator ce rulează pe un model de calcul fix Turing-complet, adică orice program care poate fi scris într-un limbaj de programare dat, care are caracter suficient de general încât să fie echivalent cu o mașină Turing. Problema este să se determine, dat fiind un program și datele lui de intrare, dacă respectivul program se va opri din rulare la un moment dat când este pornit cu intrarea respectivă. În acest cadru abstract, nu există limitări de resurse privind cantitatea de memorie sau durata de timp a execuției programului; rularea lui poate avea o durată arbitrară, și poate ocupa orice volum de spațiu înainte de a se opri. Întrebarea care se pune este dacă el se oprește sau rulează la infinit.
De exemplu, în pseudocod, programul
while (true) continue
nu se oprește; el este alcătuit exclusiv dintr-o . Pe de altă parte, programul
print "Hello, world!"
se oprește.
În aceste exemple, decizia dacă se opresc sau nu este simplă, dar programele mai complexe se dovedesc a fi problematice. O abordare a problemei ar putea fi rularea programului pentru un anumit număr de pași și verificarea dacă mai este sau nu de rulat. Dar, dacă mai are de rula, nu se știe încă dacă el se va opri sau va rula la nesfârșit. Turing a demonstrat că nu există niciun algoritm care să decidă întotdeauna corect dacă un program arbitrar cu o intrare arbitrară, se oprește. Esența demonstrației lui Turing este că orice astfel de algoritm poate fi făcut să producă o ieșire contradictorie, și deci nu poate fi corect.
Consecințele în domeniul programării calculatoarelor Unele pot fi utile. De exemplu, serverele rulează adesea în și sunt codate explicit pentru a nu se opri. Cele mai multe subrutine sunt, însă, făcute să se oprească. În particular, în , programatorii încearcă să scrie subrutine care garantează că se termină, și nu doar atât: că se termină într-un termen dat.
Uneori, acești programatori folosesc un limbaj de programare de uz general (Turing-complet), încearcă să scrie într-un stil restricționat, cum ar fi sau , ceea ce facilitează demonstrarea faptului că respectivele subrutine se opresc în termenul specificat.
Alteori, programatorii de timp real aplică ; ei folosesc intenționat un limbaj de programare care nu este cu totul Turing-complet. Adesea, acestea sunt limbaje care garantează că toate subrutinele se termină, cum ar fi .
Probleme comune Dificultatea problemei opririi constă în cerința ca procedura de decizie să funcționeze pentru orice program și orice intrare. Când primește o anume intrare, un anume program fie se oprește, fie nu. Dacă un algoritm răspunde întotdeauna cu DA și unul întotdeauna cu NU, atunci unul dintre ele a răspuns oricând corect, dar nu se știe care. Nu există însă un unic algoritm care să rezolve problema opririi la modul general.
Există interpretoare care simulează execuția unui cod sursă pe care îl primesc. Astfel de programe pot demonstra că un program se oprește: când simularea se termină, interpretorul știe că programul se oprește. Dacă însă simularea nu se oprește, atunci nici simultorul nu se oprește, astfel că el nu se poate opri și spune că programul rulat nu se oprește.
Problema opririi este teoretic decidabilă doar pentru (, LBA) sau pentru mașinile deterministe cu memorie finită. O mașină cu memorie finită are un număr finit de configurații și deci, orice program determinist de pe ea trebuie să se oprească sau să repete o configurație anterioară:. italics in originalMinsky însă remarcă:Un calculator cu un milion de piese mici, fiecare cu două stări, va avea însă, în practică, cel puțin 2 de stări posibile:
Se poate decide automat și dacă o mașină nedeterministă cu memorie finită se oprește pe unele, pe toate, sau pe niciuna din șirurile posibile de acțiuni nedeterministe, prin enumerarea stărilor de după fiecare decizie posibilă.
Istorie În aprilie 1936, Alonzo Church a publicat demonstrația indecidabilității unei probleme în . a fost și ea publicată ulterior, în ianuarie 1937. De atunci, au fost descrise multe alte probleme indecidabile, inclusiv problema opririi care a apărut în anii 1950.
Originea problemei opririi Multe articole și manuale pun definiția și demonstrația indecidabilității problemei opririi pe seama lucrării lui Turing din 1936. În ea, și nici în alte lucrări publicate, Turing nu a folosit însă termenul „oprire”. În literatura academică dintre 1936 și 1958, prima apariție a termenului „problema opririi” este în Rogers (1957). Rogers spune însă că a avut la dispoziție o ciornă a articolului Davis (1958), iar Martin Davis spune în introducere: „expertul va găsi, poate, ceva nou în aranjamentul și tratamentul subiectelor”, astfel că terminologia îi aparține lui Davis. Într-o scrisoare, el povestea că vorbea despre problema opririi din 1952.letter from Davis to Copeland, 12 December 2001, Footnote 61 in Utilizarea în cartea lui Davis este după cum urmează:
Un posibil precursor al formulării lui Davis este afirmația lui Kleene din 1952, care diferă doar prin formulare:
Problema opririi este atât cu problema tipăririi a lui Davis („o mașină Turing pornind dintr-o stare dată ajunge să tipărească vreodată un simbol dat?”) cât și cu cu problema tipăririi enunțată în articolul lui Turing din 1936 („o mașină Turing care pornește cu banda goală tipărește vreodată un simbol dat?”). Echivalența Turing este însă relativ laxă și nu înseamnă că cele două probleme sunt aceeași. Există mașini care tipăresc dar nu se opresc, și unele care se opresc dar nu tipăresc. Problemele tipăririi și opririi adresează chestiuni diferite și prezintă diferențe conceptuale și tehnice importante. Astfel, Davis era doar modest când spunea:
Formalizare În demonstrația sa, Turing a formalizat conceptul de algoritm introducând mașina Turing. Rezultatul nu este însă specific acesteia; se aplică în egală măsură oricărui model de calcul echivalent ca putere computațională cu mașina Turing, cum ar fi , , , , sau .
Important este că formalizarea permite realizarea de corespondențe directe între algoritmi și unele tipuri de date pe care poate opera un algoritm. De exemplu, dacă permite algoritmilor să definească funcții pe șiruri (cum face mașina Turing) atunci ar trebui să există o corespondență între acești algoritmi și șiruri, și dacă formalismul permite algoritmilor să definească funcții pe numere naturale (cum ar fi funcțiile calculabile) atunci trebuie să existe o corespondență între algoritmi și numerele naturale. Corespondența la șiruri este de regulă cea mai evidentă, dar șirurile peste un alfabet cu n caractere pot fi puse în corespondență cu numerele, interpretându-le ca numere într-un sistem de numerație n-ar.
Reprezentarea ca mulțime Reprezentarea convențională a problemelor de decizie este mulțimea obiectelor ce posedă proprietatea în chestiune. Mulțimea opririi
K = {(i, x) | program i se oprește când rulează pe intrarea x}
reprezintă problema opririi.
Această mulțime este , ceea ce înseamnă că există o funcție calculabilă care listează toate perechile (i, x) pe care le conține mulțimea; dar complementul acestei mulțimi nu este recursiv enumerabil.
Există mai multe formulări echivalente cu problema opririi; orice mulțime al cărei este egal cu cel al problemei opririi este o astfel de formulare. Printre exemplele de astfel de mulțimi se numără:
{i | programul i se oprește când rulează pe intrarea 0} {i | există o intrare x astfel încât programul i se oprește când rulează pe intrarea x}.
Schiță de demonstrație Christopher Strachey a enunțat o demonstrație prin reducere la absurd a propoziției „problema opririi nu este rezolvabilă”.Demonstrația este: Să presupunem că există o funcție calculabilă halts(f) care returnează dacă subrutina f se oprește (când rulează fără intrări) și altfel. Acum fie următoarea subrutină:def g() -> None: if halts(g): loop_forever()halts(g) trebuie să returneze sau , deoarece halts este presupusă a fi totală. Dacă halts(g) returnează , atunci g apelează loop_forever și nu se oprește, ceea ce este o contradicție. Dacă halts(g) returnează , atunci g se oprește, pentru că nu mai apelează loop_forever; și aceasta este o contradicție. Per ansamblu, g face opusul a ceea ce spune halts că va face g, deci halts(g) nu poate returna o valoare de adevăr consistentă cu faptul că g se oprește sau nu. Ca urmare, presupunerea inițială că halts este funcție calculabilă totală trebuie să fie falsă.
Schița unei demonstrații riguroase Conceptul de mai sus prezintă metoda generală de demonstrație, dar funcția calculabilă halts nu ia direct o subrutină ca argument; în schimb, ea primește codul sursă al unui. Mai mult, definiția lui este autoreferențială. O demonstrație rigoroasă abordează și aceste neajunsuri. Obiectivul de ansamblu este de a arăta că nu există nicio funcție calculabilă care să decidă dacă un program arbitrar i se oprește pe o intrare arbitrară x; adică următoarea funcție h (de la ) nu este calculabilă:
Aici, programul i înseamnă al i-lea program într-o a tuturor programelor unui model de calcul Turing-complet fixat.f(i,j)i123456j11 0 0 1 0 12 00 0 1 0 03 0 10 1 0 14 1 0 01 0 05 0 0 0 11 16 1 1 0 0 10 f(i,i)100110g(i)U00UU0 Valori posibile ale unei funcții calculabile totale f aranjate într-un tablou 2D. Celulele portocalii sunt diagonala. Valorile lui f(i,i) și g(i) sunt arătate jos; U indică dacă funcția g este nedefinită pentru a nume valoare de intrare.Demonstrația continuă stabilind direct că nicio funcție calculabilă totală cu două argumente nu poate fi funcția h cerută. Ca și în schița de concept, dată fiind orice funcție binară calculabilă f, următoarea funcție parțială g este și ea calculabilă de un program e:
Confirmarea că g este calculabilă se bazează pe următoarele construcții (sau echivalentele lor):
subprogramele calculabile (programul care calculează f este un subprogram din programul e), duplicarea de valori (programul e calculează intrărirle i,i de la f din intrarea i pentru g), ramificarea condiționată (programul e alege între două rezultate în funcție de valoarea pe care o calculează pentru f(i,i)), neproducerea unui rezultat definit (de exemplu, prin ciclarea la infinit), returnarea unei valori 0.
Următorul pseudocod pentru e ilustrează o modalitate simplă de a calcula g:procedure e(i): if f(i, i) == 0 then return 0 else loop foreverDeoarece g este parțial calculabilă, trebuie să existe un program e care calculează g, prin presupunerea că modelul de calcul este Turing-complet. Acest program este unul din toate programele pe care este definită funcția de oprire h. Următorul pas al demonstrației arată că h(e,e) nu va avea aceeași valoare ca f(e,e).