У матэматыцы і інфарматыцы, Праблема вырашальнасці ( — нямецкая для «праблемы вырашэння») — задача з вобласці падстаў матэматыкі, сфармуляваная Давідам Гільбертам і Вільгельмам Акерманам у 1928 годзе: знайсці алгарытм, які б прымаў у якасці ўваходных дадзеных апісанне любой фармальнай мовы і матэматычнага сцвярджэння «S» на гэтай мове — і, пасля канчатковага ліку крокаў, спыняўся б, і выдаваў адзін з двух адказаў: «Так» або «Не», — у залежнасці ад таго, ці з’яўляецца зацверджанне «S» заўсёды сапраўдным, гэта значыць сапраўдным у кожнай структуры, якая задавальняе аксіёмы.David Hilbert and Wilhlem Ackermann. Grundzüge der Theoretischen Logik. Springer, Berlin, Germany, 1928. English translation: David Hilbert and Wilhelm Ackermann. Principles of Mathematical Logic. AMS Chelsea Publishing, Providence, Rhode Island, USA, 1950. Адказ не патрабуе абгрунтаванняў, але павінен быць дакладным.

Такі алгарытм мог бы, на прыклад, пацвердзіць гіпотэзу Гольдбаха і гіпотэзу Рымана нягледзячы на ​​тое, што доказы (і абвяржэння) пакуль невядомыя. Неразвязальнасць праблемы вырашальнасці (невырашальнасць мноства праўдзівых формул арыфметыкі) для мовы арыфметыкі, якая змяшчае «роўнасць», «складанне» і «множанне», з’яўляецца следствам неарыфметычнасці гэтага мноства. Неарыфметычнасць з’яўляецца следствам тэарэмы Тарскага аб невыказальнасці паняцця праўдзівасці ў мове сродкамі той жа мовы"В. А. Успенский, А. Л. Семёнов Теория алгоритмов: основные открытия и приложения, М., Наука, 1987, 288 c., 2.3 Приложения к математической логике: анализ формализованных языков логики и арифметики.

Тэарэма паўнаты Згодна з тэарэмай паўнаты логікі першага парадку, сцвярджэнне з’яўляецца агульнасапраўдным тады і толькі тады, калі яго можна вывесці з аксіём, таму праблему вырашальнасці таксама можна разглядаць як запыт пра алгарытм, які вырашыць, ці даказана дадзенае сцвярджэнне з аксіём, выкарыстоўваючы правілы логікі.

У 1936 годзе — Алонза Чорч і незалежна ад яго Алан Цьюрынг апублікавалі працыАртыкул Чорча быў прадстаўлены Амерыканскаму матэматычнаму таварыству 19 красавіка 1935 г. і апублікаваны 15 красавіка 1936 г. Цьюрынг, які дасягнуў істотнага прагрэсу апісваючы ўласныя вынікі, быў расчараваны, даведаўшыся пра доказы Чорча пасля яго публікацыі (гл. перапіску паміж Максам Ньюманам і Чорчам у дакументах Чорча, Алонза). Цьюрынг хутка дапісаў сваю працу і паспяшаўся яе выдаць у «Працах Лонданскага матэматычнага таварыства» ў двух падзелах: у частцы 3 (старонкі 230—240), выдадзенай 30 лістапада 1936 г., і ў частцы 4 (старонкі 241—265), выдадзенай 23 снежня 1936 г.; Цюрынг дадаў выпраўленні ў том 43 (1937), стар. 544—546., у якіх паказалі, што не існуе алгарытму для вызначэння праўдзівасці сцвярджэнняў арыфметыкі, а таму і больш агульная праблема вырашальнасці таксама не мае рашэння. Гэты вынік атрымаў назву: «тэарэма Чорча — Цьюрынга».

Гісторыя праблемы Паходжанне праблемы вырашальнасці ўзыходзіць да Готфрыда Лейбніца, які ў XVII стагоддзі пасля пабудовы паспяховай механічнай вылічальнай машыны марыў пабудаваць машыну, якая можа маніпуляваць сімваламі дзеля таго, каб вызначыць праўдзівасць матэматычных выказванняў.Дэвіс 2000: стар. 3-20 Ён зразумеў, што першым крокам павінна быць вызначэнне чыстай фармальнай мовы, і большая частка яго наступнай працы была накіравана на гэтую мэту. У 1928 г. Дэвід Гільберт і Вільгельм Акерман паставілі пытанне ў форме, выкладзенай вышэй.

У працяг сваёй «праграмы» Гільберт паставіў тры пытанні на міжнароднай канферэнцыі ў 1928 г., трэцяе з якіх стала называцца «Гільбертавай праблемай вырашальнасці.» Ходжэс стар. 91 У 1929 г. Майсей Шэйнфінкель апублікаваў артыкул пра асаблівыя выпадкі праблемы вырашальнасці, падрыхтаваны Паулем Бернайсам.

Ужо ў 1930 г. Гільберт лічыў, што не можа быць невырашальнай праблемы.Ходжэс стар. 92, цытуючы Гільберта

Адмоўны адказ Перш чым можна было адказаць на пытанне вырашальнасці, трэба было фармальна вызначыць паняцце «алгарытм». Гэта зрабіў Алонза Чорч у 1935 г. з канцэпцыяй «эфектыўнай вылічальнасці», заснаванай на яго λ-вылічэнні, і Алан Цьюрынг у наступным годзе з яго канцэпцыяй машыны Цьюрынга с. Цьюрынг адразу зразумеў, што гэта эквівалентныя мадэлі вылічэнняў.

Адмоўны адказ на вырашэнне праблемы вырашальнасці быў дадзены Алонзам Чорчам у 1935—1936 (Тэарэма Чорча) і незалежна неўзабаве пасля гэтага Аланам Цьюрынгам у 1936 г. (доказ Цьюрынга). Чорч даказаў, што не існуе вылічальнай функцыі, якая вырашае для двух дадзеных выразаў λ-вылічэння, эквівалентныя яны ці не. Ён у значнай ступені абапіраўся на ранейшыя працы Стывена Кліна. Цьюрынг звёў пытанне аб існаванні «агульнага метаду», які вырашае, ці спыняецца якая-небудзь машына Цьюрынга (праблема спынення), да пытання пра існаванне «алгарытму» альбо «агульнага метаду», здольнага вырашыць праблему вырашальнасці. Калі «Алгарытм» разумеецца як эквівалент машыны Цюрынга, а адказ на апошняе пытанне адмоўны (ўвогуле), тады і на пытанне аб існаванні алгарытму для праблемы вырашальнасці адказ таксама павінны быць адмоўным у цэлым. У сваёй працы 1936 г. Цьюрынг кажа: "Адпаведна кожнай вылічальнай машыне «it», мы ствараем формулу «Un(it)» і паказваем, што калі існуе агульны метад вызначэння даказальнасці «Un(it)», тады існуе і агульны метад вызначэння таго, ці надрукуе «it» калі-небудзь 0 ".

На працу Чорча і Цьюрынга моцна паўплывала больш ранняя праца Курта Гёдэля над яго Тэарэмай незавершанасці, асабліва метадам прысваення лікаў нумарацыі Гёдэля да лагічных формул, каб звесці логіку да арыфметыкі.

Праблема вырашальнасці звязана з дзесятай праблемай Гільберта, якая запытвае алгарытм, ці мае ўраўненне Дыяфанта вырашэнне. Неіснаванне такога алгарытму, усталяванае Юрыем Матыясевічам у 1970 г., таксама прадугледжвае адмоўны адказ на праблему вырашальнасці.

Некаторыя тэорыі першага парадку можна алгарытмічна вырашаць; прыклады гэтага ўключаюць арыфметыку Прэсбургера, рэальнае закрытае поле s і сістэмы статычнага тыпу з многіх моваў праграмавання. Агульную тэорыю першага парадку натуральнага ліку, выражаную ў аксіёмах Пеано, нельга вырашыць з дапамогай алгарытму.

Практычныя працэдуры прыняцця рашэння Цэннай уяўляецца наяўнасць практычных працэдур прыняцця рашэнняў для класаў лагічных формул для праверкі праграмы і праверкі схем. Чыстыя лагічныя формулы звычайна вырашаюцца з выкарыстаннем методык праблемы выкананасці булевых формул, заснаваных на поўным алгарытме пошуку з вяртаннем. Кан’юнктыўныя формулы над лінейнай рэальнай альбо рацыянальнай арыфметыкай можна вырашыць, выкарыстоўваючы сімплексны алгарытм, формулы ў лінейнай цэлалікавай арыфметыцы (арыфметыка Прэсбургера) можна вырашыць, выкарыстоўваючы алгарытм Купера альбо тэст Амега Уільяма П’ю. Формулы з адмаўленнямі, злучнікамі і дыз’юнкцыямі спалучаюць цяжкасці праверкі выкананасці з праблемамі рашэння злучнікаў; яны звычайна вырашаюцца ў наш час з выкарыстаннем рашэння тэорыі модуля выкананасці, якія спалучаюць рашэнне тэорыі модуля выкананасці з працэдурамі прыняцця рашэнняў для спалучэння і метадаў распаўсюджвання. Сапраўдная паліномная арыфметыка, таксама вядомая як тэорыя рэальнага замкнёнага поля s, можа быць вырашана; гэта тэарэма Тарскага – Зайдэнберга, якая была рэалізавана ў камп’ютарах з выкарыстаннем цыліндрычнага алгебраічнага раскладання.

Гл. таксама Разборлівасць (логіка) Аўтаматызаванае даказанне тэарэмы Другая праблема Гільберта Машына Oracle Доказ Цьюрынга

Заўвагі

Літаратура

Эндру Ходжэс, Алан Цьюрынг: Загадка, Сайман і Шустэр, Нью-Ёрк, 1983 г. Біяграфія Алана М. Цьюрынга. Гл. Раздзел «Дух праўды» пра гісторыю з’яўлення яго доказу, і абмеркаванне доказу.

Катэгорыя:Тэорыя алгарытмаў Катэгорыя:Матэматычная логіка Катэгорыя:Тэорыя вылічальнасці Катэгорыя:Метатэарэмы Катэгорыя:Невырашальныя праблемы