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

З пляцоўкі Вікіпедыя

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

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

Тэарэма паўнаты[правіць | правіць зыходнік]

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

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

Гісторыя праблемы[правіць | правіць зыходнік]

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

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

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

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

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

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

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

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

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

Практычныя працэдуры прыняцця рашэння[правіць | правіць зыходнік]

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

Глядзіце таксама[правіць | правіць зыходнік]

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

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

  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 г. Цьюрынг, якi дасягнуў істотнага прагрэсу апісваючы ўласныя вынікі, быў расчараваны, даведаўшыся пра доказы Чорча пасля яго публікацыі (гл. перапіску паміж Максам Ньюманам і Чорчам у дакументах Чорча, Алонза). Цьюрынг хутка дапісаў сваю працу і паспяшаўся яе выдаць у «Працах Лонданскага матэматычнага таварыства» ў двух падзелах: у частцы 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, цытуючы Гільберта