Праблема вырашальнасці

У матэматыцы і інфарматыцы, Праблема вырашальнасці (ням.: Entscheidungsproblem — нямецкая для «праблемы вырашэння») — задача з вобласці падстаў матэматыкі, сфармуляваная Давідам Гільбертам і Вільгельмам Акерманам у 1928 годзе: знайсці алгарытм, які б прымаў у якасці ўваходных дадзеных апісанне любой фармальнай мовы і матэматычнага сцвярджэння «S» на гэтай мове — і, пасля канчатковага ліку крокаў, спыняўся б, і выдаваў адзін з двух адказаў: «Так» або «Не», — у залежнасці ад таго, ці з’яўляецца зацверджанне «S» заўсёды сапраўдным, гэта значыць сапраўдным у кожнай структуры, якая задавальняе аксіёмы.[1]. Адказ не патрабуе абгрунтаванняў, але павінен быць дакладным.

Такі алгарытм мог бы, на прыклад, пацвердзіць гіпотэзу Гольдбаха і гіпотэзу Рымана нягледзячы на ​​тое, што доказы (і абвяржэння) пакуль невядомыя. Неразвязальнасць праблемы вырашальнасці (невырашальнасць мноства праўдзівых формул арыфметыкі) для мовы арыфметыкі, якая змяшчае «роўнасць», «складанне» і «множанне», з’яўляецца следствам неарыфметычнасці гэтага мноства. Неарыфметычнасць з’яўляецца следствам тэарэмы Тарскага аб невыказальнасці паняцця праўдзівасці ў мове сродкамі той жа мовы"[2].

Тэарэма паўнаты

[правіць | правіць зыходнік]

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

У 1936 годзе — Алонза Чорч і незалежна ад яго Алан Цьюрынг апублікавалі працы[3], у якіх паказалі, што не існуе алгарытму для вызначэння праўдзівасці сцвярджэнняў арыфметыкі, а таму і больш агульная праблема вырашальнасці таксама не мае рашэння. Гэты вынік атрымаў назву: «тэарэма Чорча — Цьюрынга».

Гісторыя праблемы

[правіць | правіць зыходнік]

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

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

Ужо ў 1930 г. Гільберт лічыў, што не можа быць невырашальнай праблемы.[7]

Адмоўны адказ

[правіць | правіць зыходнік]

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

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

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

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

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

Практычныя працэдуры прыняцця рашэння

[правіць | правіць зыходнік]

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

Гл. таксама

[правіць | правіць зыходнік]

Заўвагі

[правіць | правіць зыходнік]
  1. ↑ 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
  2. ↑ В. А. Успенский, А. Л. Семёнов Теория алгоритмов: основные открытия и приложения, М., Наука, 1987, 288 c., 2.3 Приложения к математической логике: анализ формализованных языков логики и арифметики
  3. ↑ Артыкул Чорча быў прадстаўлены Амерыканскаму матэматычнаму таварыству 19 красавіка 1935 г. і апублікаваны 15 красавіка 1936 г. Цьюрынг, які дасягнуў істотнага прагрэсу апісваючы ўласныя вынікі, быў расчараваны, даведаўшыся пра доказы Чорча пасля яго публікацыі (гл. перапіску паміж Максам Ньюманам і Чорчам у дакументах Чорча, Алонза). Цьюрынг хутка дапісаў сваю працу і паспяшаўся яе выдаць у «Працах Лонданскага матэматычнага таварыства» ў двух падзелах: у частцы 3 (старонкі 230—240), выдадзенай 30 лістапада 1936 г., і ў частцы 4 (старонкі 241—265), выдадзенай 23 снежня 1936 г.; Цюрынг дадаў выпраўленні ў том 43 (1937), стар. 544—546.
  4. ↑ Дэвіс 2000: стар. 3-20
  5. ↑ Ходжэс стар. 91
  6. ↑ Г. Л. Кляйн Агляд асноў матэматыкі і матэматычнай логікі С. А. Яноўскай. — 1951. — В. 1. — С. 46–48. — DOI:10.2307 / 2268665
  7. ↑ Ходжэс стар. 92, цытуючы Гільберта

Літаратура

[правіць | правіць зыходнік]