Problema deciziei

În matematică și informatică, problema deciziei, denumită și Entscheidungsproblem (Pronunție în germană: /ɛntˈʃaɪ̯dʊŋspʁoˌbleːm/, din germană) este o provocare lansată de David Hilbert în 1928. Problema cere un algoritm care are ca intrare o afirmație într-o logică de ordinul întâi^⁠(d) (eventual cu un număr finit de axiome în afara axiomelor obișnuite din logica de ordinul întâi) și răspunde cu "Da" sau "Nu" după cum afirmația este universal valabilă, adică valabile în orice structură care satisface axiomele. Conform teoremei de integralitate a logicilor de ordinul întâi^⁠(d), o afirmație este universal valabilă dacă și numai dacă ea poate fi dedusă din axiome, deci problema deciziei poate fi văzută și ca cerând unui algoritm să decidă dacă o anumită afirmație este demonstrată din axiome cu ajutorul regulilor logicii^⁠(d).

În 1936, Alonzo Church și Alan Turing au publicat independent lucrări în care arătau că o soluție generală a problemei deciziei este imposibilă, presupunând că noțiunea intuitivă de „efectiv calculabilă^⁠(d)” este capturată de funcțiile calculabile de către o mașină Turing (sau, echivalent, de cele exprimate în calculul lambda^⁠(d)). Această ipoteză este acum cunoscut sub numele de teza Church–Turing.

Istoria problemei

Originea problemei deciziei datează de la Gottfried Leibniz, care, în secolul al XVII-lea, după ce a construit o mașină de calcul^⁠(d) mecanică, visa să construiască o mașină care ar putea manipula simboluri pentru a determina valoarea de adevăr a unei afirmații matematice. El și-a dat seama că primul pas ar trebui să fie un limbaj formal curat, și o mare parte din lucrările sale ulterioare s-au îndreptat în direcția acestui obiectiv. În 1928, David Hilbert și Wilhelm Ackermann au pus problema în forma prezentată mai sus.

În continuarea „programului” său, Hilbert a pus trei întrebări la o conferință internațională în 1928, dintre care a treia a devenit cunoscută sub numele de „Entscheidungsproblem a lui Hilbert”. În 1929, Moses Schönfinkel^⁠(d) a publicat un articol cu privire la cazurile particulare ale problemei deciziei, care au fost pregătite de Paul Bernays.

Chiar și în 1930, Hilbert credea că nu există probleme de nerezolvat.

Răspunsul negativ

Înainte ca întrebarea să poate primi răspuns, trebuia definită formal noțiunea de „algoritm”. Acest lucru a fost făcut de către Alonzo Church în 1936 cu conceptul de „calculabilitate efectivă”, bazat pe calcul λ^⁠(d), precum și de către Alan Turing în același an, cu conceptul său de mașină Turing. Turing a recunoscut imediat că acestea sunt modele de calcul^⁠(d) echivalente.

Răspunsul negativ la problema deciziei apoi a fost dat de către Alonzo Church în 1935-36 și în mod independent^⁠(d) la scurt timp după aceea de către Alan Turing în 1936. Church a demonstrat că nu există nicio funcție calculabilă^⁠(d) care decide, pentru două λ-expresii date, dacă acestea sunt echivalente sau nu. El s-a bazat în mare măsură pe lucrările anterioare ale lui Stephen Kleene. Turing a redus întrebarea la existența unui „algoritm” sau a unei „metode generale” capabilă să rezolve problema deciziei la întrebarea dacă există sau nu o metodă generală care decide dacă o anumită mașină Turing se oprește sau nu (problema opririi^⁠(d)). Dacă cuvântul „algoritm” este înțeles ca fiind echivalent cu o mașină Turing, și în condițiile în care întrebarea din urmă are răspuns negativ (în general), întrebarea despre existența unui algoritm pentru problema opririi are răspuns tot negativ (în general). În articolul său din 1936, Turing spunea: „Corespunzător fiecărei mașini de calcul «it» vom construi o formulă «Un(it)» și vom arăta că, dacă există o metodă generală pentru a determina dacă «Un(it)» este demonstrabilă, atunci există o metodă generală pentru a determina dacă «it» tipărește vreodată 0".

Munca lui Church și Turing a fost puternic influențată de lucrările anterioare ale lui Kurt Gödel la teorema incompletitudinii^⁠(d), mai ales prin metoda de atribuire de numere (o numerotare Gödel^⁠(d)) formulelor logice, în scopul de a reduce logica la aritmetică.

Problema deciziei este legată de a zecea problemă a lui Hilbert^⁠(d), care cere un algoritm pentru a decide dacă ecuațiile diofantice^⁠(d) au o soluție. Inexistența unui astfel de algoritm, stabilită de către Iuri Matiasevici^⁠(d) în 1970, implică, de asemenea, un răspuns negativ la problema deciziei.

Unele teorii de ordinul întâi sunt algoritmic decidabile; exemple în acest sens includ aritmetica Presburger^⁠(d), corpurile reale închise^⁠(d) și sistemele de tipare statică^⁠(d) ale multor limbaje de programare. Teoria generală de ordinul întâi a numerelor naturale exprimată prin axiomele lui Peano^⁠(d) nu poate fi decisă însă cu un algoritm.

Proceduri practice de decizie

Existența unor proceduri practice de decizie pentru unele clase formule logice este însă de interes considerabil pentru verificarea programelor^⁠(d) și a circuitelor. Formulele pur booleene sunt, de obicei, decise folosind tehnici de rezolvare SAT^⁠(d) bazate pe algoritmul DPLL^⁠(d). Formulele conjunctive peste aritmetici liniare reale sau raționale pot fi decis cu ajutorul algoritmului simplex, formulele în aritmetica liniară a întregilor (aritmetica Presburger^⁠(d)) pot fi decise cu ajutorul algoritmului lui Cooper sau cu testul Omega al lui William Pugh^⁠(d). Formulele cu negații, conjuncții și disjuncții combină dificultățile testării satisfiabilității cu cele ale deciziei conjuncțiilor; ele sunt, în general, decise astăzi folosind tehnici de rezolvare SMT^⁠(d), care combina rezolvările SAT cu procedurile de decizie pentru conjuncții și tehnici de propagare. Aritmetica polinomială reală cunoscută și ca „teoria corpurilor reale închise^⁠(d)”, este decidabilă; aceasta este teorema Tarski–Seidenberg^⁠(d), care a fost pusă în aplicare în computere cu ajutorul descompunerii algebrice cilindrice^⁠(d).

Bibliografie

• David Hilbert și Wilhelm Ackermann (1928). Grundzüge der theoretischen Logik (Principii de Logică Matematică). Springer-Verlag, ISBN: 0-8218-2024-9.
• Alonzo Church, "O problemă de nerezolvat de elementar de teoria numerelor", American Journal of Mathematics, 58 (1936), pp 345-363
• Alonzo Church, "O notă privind Entscheidungsproblem", Revista de Logica Simbolică, 1 (1936), pp. 40-41.
• Martin Davis, 2000, Motoare de Logica, W. W. Norton & Company, Londra, ISBN: 0-393-32229-7 pbk.
• Alan Turing, "On computable numbers, cu o cerere la Entscheidungsproblem", Proceedings of the London Mathematical Society, Seria 2, 42 (1936-7), pp 230-265. Versiunile Online: de la site-ul revistei, de la Turing Arhivă Digitală^{[nefuncțională]}, de la abelard.org. Erata a apărut în Seria 2, 43 (1937), pp 544-546.
• Martin Davis, "Nehotărât, Bază Documente privind Nehotărât Propuneri, Probleme de Nerezolvat Și Calculabil Funcții", Raven Press, New York, 1965. Turing hârtie este #3 în acest volum. Documentele includ pe cele de Gödel, Church, Rosser, Kleene, și Post.
• Andrew Hodges, Alan Turing: The Enigma, Simon and Schuster, New York, 1983. Alan M. Turing biografia lui. Cf Capitolul "Duhul Adevărului" pentru o istorie care să conducă la, și o discuție a lui dovada.
• Robert Soare, "Computability și recursivitate", Bull. Logica simbolică 2 (1996), nr. 3, 284-321.
• Stephen Toulmin, "Căderea unui Geniu", o recenzie de carte "Alan Turing: The Enigma de Andrew Hodges", în The New York Review of Books, 19 ianuarie 1984, p. 3ff.
• Alfred North Whitehead și Bertrand Russell, Principia Mathematica a *56, la Cambridge University Press, 1962. Re: problema de paradoxuri, autorii discuta problema dintr-un set nu fi un obiect în orice "determinarea funcții", în special "Introducere, Cap. 1 p. 24 "...dificultățile care apar în logica formală", și Chap. 2.I. "Vicios-Cerc Principiul" p. 37ff, și Chap. 2.VIII. "Contradicțiile" p. 60 ff.