Праблема вырашальнасці
Артыкул — машынны пераклад іншамоўнага тэксту. |
У матэматыцы і інфарматыцы, Праблема вырашальнасці (ням.: 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, можа быць вырашана; гэта тэарэма Тарскага – Зайдэнберга, якая была рэалізавана ў камп’ютарах з выкарыстаннем цыліндрычнага алгебраічнага раскладання.
Гл. таксама
правіцьЗаўвагі
правіць- ↑ 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 Приложения к математической логике: анализ формализованных языков логики и арифметики
- ↑ Артыкул Чорча быў прадстаўлены Амерыканскаму матэматычнаму таварыству 19 красавіка 1935 г. і апублікаваны 15 красавіка 1936 г. Цьюрынг, які дасягнуў істотнага прагрэсу апісваючы ўласныя вынікі, быў расчараваны, даведаўшыся пра доказы Чорча пасля яго публікацыі (гл. перапіску паміж Максам Ньюманам і Чорчам у дакументах Чорча, Алонза). Цьюрынг хутка дапісаў сваю працу і паспяшаўся яе выдаць у «Працах Лонданскага матэматычнага таварыства» ў двух падзелах: у частцы 3 (старонкі 230—240), выдадзенай 30 лістапада 1936 г., і ў частцы 4 (старонкі 241—265), выдадзенай 23 снежня 1936 г.; Цюрынг дадаў выпраўленні ў том 43 (1937), стар. 544—546.
- ↑ Дэвіс 2000: стар. 3-20
- ↑ Ходжэс стар. 91
- ↑ Г. Л. Кляйн Агляд асноў матэматыкі і матэматычнай логікі С. А. Яноўскай. — 1951. — В. 1. — С. 46–48. — DOI:10.2307 / 2268665
- ↑ Ходжэс стар. 92, цытуючы Гільберта
Літаратура
правіць- Alonzo Church An unsolvable problem of elementary number theory // American Journal of Mathematics. — 1936. — Vol. 58. — P. 345—363. — DOI:10.2307/2371045
- Alonzo Church A note on the Entscheidungsproblem // Journal of Symbolic Logic. — 1936. — Vol. 1. — P. 40—41.
- Turing A. On Computable Numbers, with an Application to the Entscheidungsproblem // Proceedings of the London Mathematical Society — London Mathematical Society, 1937. — Vol. s2-42, Iss. 1. — P. 230–265. — ISSN 0024-6115; 1460-244X; 0024-6115 — doi:10.1112/PLMS/S2-42.1.230
- Turing A. M. On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction // Proceedings of the London Mathematical Society — London Mathematical Society, 1938. — Vol. s2-43, Iss. 6. — P. 544–546. — ISSN 0024-6115; 1460-244X; 0024-6115 — doi:10.1112/PLMS/S2-43.6.544
- Эдельман С.Л. Математическая логика. — М.: Высшая школа, 1975.
- Эндру Ходжэс, Алан Цьюрынг: Загадка, Сайман і Шустэр, Нью-Ёрк, 1983 г. Біяграфія Алана М. Цьюрынга. Гл. Раздзел «Дух праўды» пра гісторыю з’яўлення яго доказу, і абмеркаванне доказу.