Проблема решения

В математике и информатике Entscheidungsproblem ; ( по -немецки «проблема решения») произносится [ɛntˈʃaɪ̯dʊŋspʁoˌbleːm] ) — это вызов, поставленный Дэвидом Гильбертом и Вильгельмом Аккерманом в 1928 году. ^[1] Задача требует алгоритма , который рассматривает в качестве входных данных утверждение и отвечает «да» или «нет» в зависимости от того, является ли это утверждение универсально допустимым , то есть допустимым в любой структуре .

Теорема о полноте

Согласно теореме о полноте логики первого порядка , утверждение является универсально действительным тогда и только тогда, когда оно может быть выведено с использованием логических правил и аксиом, поэтому проблему Entscheidungsproblem можно также рассматривать как требование алгоритма решить, доказуемо ли данное утверждение, используя правила логики .

В 1936 году Алонсо Чёрч и Алан Тьюринг опубликовали независимые статьи. ^[2]показывая, что общее решение проблемы Entscheidungsproblem невозможно , предполагая, что интуитивное понятие « эффективно вычислимого » фиксируется функциями, вычислимыми машиной Тьюринга (или, что то же самое, теми, которые выражаются в лямбда-исчислении ). Это предположение теперь известно как тезис Чёрча-Тьюринга .

История проблемы [ править ]

Истоки проблемы Entscheidungsproblem восходят к Готфриду Лейбницу , который в семнадцатом веке, после создания успешной механической вычислительной машины , мечтал построить машину, которая могла бы манипулировать символами, чтобы определять истинностные значения математических утверждений. ^[3]Он понял, что первым шагом должен стать чистый формальный язык , и большая часть его последующей работы была направлена на достижение этой цели. В 1928 году Давид Гильберт и Вильгельм Акерман поставили вопрос в форме, изложенной выше.

В продолжение своей «программы» Гильберт поставил на международной конференции в 1928 году три вопроса, третий из которых стал известен как «проблема Гильберта Entscheidungs ». ^[4] В 1929 году Мозес Шёнфинкель опубликовал статью об особых случаях проблемы принятия решений, подготовленную Полем Бернейсом . ^[5]

Еще в 1930 году Гильберт считал, что неразрешимой проблемы не существует. ^[6]

Отрицательный ответ [ править ]

Прежде чем можно было ответить на этот вопрос, необходимо было формально определить понятие «алгоритм». Это было сделано Алонсо Чёрчем в 1935 году с концепцией «эффективной вычислимости», основанной на его λ-исчислении , и Аланом Тьюрингом в следующем году с его концепцией машин Тьюринга . Тьюринг сразу понял, что это эквивалентные модели вычислений .

Отрицательный ответ на проблему Entscheidungsproblem был затем дан Алонзо Чёрчем в 1935–36 годах ( теорема Чёрча ) и независимо вскоре после этого Аланом Тьюрингом в 1936 году ( доказательство Тьюринга ). Чёрч доказал, что не существует вычислимой функции , которая бы решала для двух заданных выражений λ-исчисления, эквивалентны они или нет. Он во многом полагался на более ранние работы Стивена Клини . Тьюринг свел вопрос о существовании «алгоритма» или «общего метода», способного решить проблему Entscheidungs, к вопросу о существовании «общего метода», который решает, остановится или нет какая-либо данная машина Тьюринга ( проблема остановки ). Если под «алгоритмом» понимать метод, который можно представить в виде машины Тьюринга, и при отрицательном (вообще) ответе на последний вопрос, то вопрос о существовании алгоритма для задачи Entscheidungs также должен быть отрицательным (в общий). В своей статье 1936 года Тьюринг говорит: «Соответствуя каждой вычислительной машине «оно», мы конструируем формулу «Un(it)» и показываем, что, если существует общий метод определения того, доказуемо ли «Un(it)», тогда существует общий метод определения того, печатает ли он когда-либо 0".

На работу Чёрча и Тьюринга сильно повлияла более ранняя работа Курта Гёделя над его теоремой о неполноте , особенно методом присвоения чисел ( нумерация Гёделя ) логическим формулам с целью свести логику к арифметике.

Проблема Entscheidungsproblem связана с десятой проблемой Гильберта , которая требует алгоритма , позволяющего определить, имеют ли диофантовые уравнения решение. Отсутствие такого алгоритма, установленного работой Юрия Матиясевича , Джулии Робинсон , Мартина Дэвиса и Хилари Патнэм с последней частью доказательства в 1970 году, также подразумевает отрицательный ответ на Entscheidungsproblem .

Обобщения [ править ]

Используя теорему о дедукции , проблема Entscheidungs охватывает более общую проблему определения того, влечет ли данное предложение первого порядка заданный конечный набор предложений, но достоверность в теориях первого порядка с бесконечным количеством аксиом не может быть напрямую сведена к проблеме Entscheidungs. Однако такие более общие проблемы принятия решений представляют практический интерес. Некоторые теории первого порядка алгоритмически разрешимы ; примеры этого включают арифметику Пресбургера , реальные закрытые поля и системы статических типов многих языков программирования . С другой стороны, теория натуральных чисел первого порядка со сложением и умножением, выраженная аксиомами Пеано, не может быть решена с помощью алгоритма.

Фрагменты [ править ]

По умолчанию в разделе используются цитаты из Pratt-Hartmann (2023). ^[7]

Классическая Entscheidungsproblem спрашивает, верна ли данная формула первого порядка во всех моделях. Финитарная проблема спрашивает, верно ли это для всех конечных моделей. Теорема Трахтенброта показывает, что это тоже неразрешимо. ^[8]^[7]

Некоторые обозначения: ${\rm {{Sat}(\Phi )}}$ означает проблему решения, существует ли модель набора логических формул $\Phi$ . ${\rm {{FinSat}(\Phi )}}$ та же проблема, но для конечных моделей. ${\rm {Sat}}$ -задача для логического фрагмента называется разрешимой, если существует программа, способная решить для каждого $\Phi$ конечное множество логических формул во фрагменте, будь то ${\rm {{Sat}(\Phi )}}$ или нет.

Существует иерархия разрешимостей. Наверху — неразрешимые проблемы. Ниже приведены решаемые проблемы. Кроме того, решаемые проблемы можно разделить по иерархии сложности.

Аристотелевский и реляционный [ править ]

Аристотелева логика рассматривает 4 вида предложений: «Все p суть q», «Все p не являются q», «Некоторые p есть q», «Некоторые p не являются q». Мы можем формализовать такие предложения как фрагмент логики первого порядка:

\forall x,p(x)\to \pm q(x),\quad \exists x,p(x)\wedge \pm q(x)

где

p,q

являются атомарными предикатами, а

+q:=q,\;-q:=\neg q

. Учитывая конечный набор аристотелевских логических формул, NLOGSPACE -полно, чтобы решить его.

{\rm {Sat}}

. Это также NLOGSPACE-полно, чтобы решить

{\rm {Sat}}

для небольшого расширения (теорема 2.7):

\forall x,\pm p(x)\to \pm q(x),\quad \exists x,\pm p(x)\wedge \pm q(x)

Реляционная логика расширяет аристотелевскую логику, допуская реляционный предикат. Например, «Каждый кого-то любит» можно записать так:

{\textstyle \forall x,{\rm {{body}(x),\exists y,{\rm {{body}(y)\wedge {\rm {{love}(x,y)}}}}}}}

. Обычно у нас есть 8 видов предложений:

{\begin{aligned}\forall x,p(x)\to (\forall y,q(x)\to \pm r(x,y)),&\quad \forall x,p(x)\to (\exists y,q(x)\wedge \pm r(x,y))\\\exists x,p(x)\wedge (\forall y,q(x)\to \pm r(x,y)),&\quad \exists x,p(x)\wedge (\exists y,q(x)\wedge \pm r(x,y))\end{aligned}}

Это NLOGSPACE -полный, чтобы решить

{\rm {Sat}}

(теорема 2.15). Реляционная логика может быть расширена до 32 видов предложений, позволяя

\pm p,\pm q

, но это расширение является EXPTIME -полным (теорема 2.24).

Арити [ править ]

Фрагмент логики первого порядка, в котором есть только имена переменных. $x,y$ является NEXPTIME -полным (теорема 3.18). С $x,y,z$ , RE -полна, чтобы решить ${\rm {Sat}}$ , и со-RE-завершить, чтобы решить ${\rm {FinSat}}$ (теорема 3.15), поэтому неразрешима.

Монадическое исчисление предикатов представляет собой фрагмент, в котором каждая формула содержит только одномерные предикаты и не содержит функциональных символов. Его ${\rm {Sat}}$ является NEXPTIME-полным (теорема 3.22).

Префикс квантификатора [ править ]

Любая формула первого порядка имеет пренексную нормальную форму. Для каждого возможного префикса квантора пренексной нормальной формы у нас есть фрагмент логики первого порядка. Например, класс Бернейса–Шенфинкеля , $[\exists ^{*}\forall ^{*}]_{=}$ , — класс формул первого порядка с префиксом квантора $\exists \cdots \exists \forall \cdots \forall$ , символы равенства и отсутствие функциональных символов .

Например, в статье Тьюринга 1936 года (стр. 263) отмечалось, что, поскольку проблема остановки для каждой машины Тьюринга эквивалентна логической формуле первого порядка вида $\forall \exists \forall \exists ^{6}$ , проблема ${\rm {{Sat}(\forall \exists \forall \exists ^{6})}}$ является неразрешимым.

Точные границы известны, резко:

${\rm {{Sat}(\forall \exists \forall )}}$ и ${\rm {{Sat}([\forall \exists \forall ]_{=})}}$ являются ко-RE-полными, а ${\rm {FinSat}}$ задачи RE-полны (теорема 5.2).
То же самое для $\forall ^{3}\exists$ (теорема 5.3).
$\exists ^{*}\forall ^{2}\exists ^{*}$ разрешима, что независимо доказали Гёдель, Шютте и Кальмар.
$[\forall ^{2}\exists ]_{=}$ является неразрешимым.
Для любого $n\geq 0$ $n\geq 0$ , оба ${\rm {{Sat}(\exists ^{n}\forall ^{*})}}$ ${\rm {{Сб}(\exists ^{n}\forall ^{*})}}$ и ${\rm {{Sat}([\exists ^{n}\forall ^{*}]_{=})}}$ ${\rm {{Сб}([\exists ^{n}\forall ^{*}]_{=})}}$ являются NEXPTIME-полными (теорема 5.1).
- Это означает, что ${\rm {{Sat}([\exists ^{*}\forall ^{*}]_{=})}}$ разрешима — результат, впервые опубликованный Бернейсом и Шенфинкелем. ^[9]
Для любого $n\geq 0,m\geq 2$ , ${\rm {{Sat}(\exists ^{n}\forall \exists ^{m})}}$ является EXPTIME полным (раздел 5.4.1).
Для любого $n\geq 0$ $n\geq 0$ , ${\rm {{Sat}([\exists ^{n}\forall \exists ^{*}]_{=})}}$ ${\rm {{Сб}([\exists ^{n}\forall \exists ^{*}]_{=})}}$ является NEXPTIME-завершенным (раздел 5.4.2).
- Это означает, что ${\rm {{Sat}(\exists ^{*}\forall ^{*}\exists ^{*})}}$ разрешима — результат, впервые опубликованный Аккерманом. ^[10]
Для любого $n\geq 0$ , ${\rm {{Sat}(\exists ^{n}\forall \exists )}}$ и ${\rm {{Sat}([\exists ^{n}\forall \exists ]_{=})}}$ являются PSPACE-полными (раздел 5.4.3).

Бёргер и др. (2001) ^[11] описывает уровень вычислительной сложности для каждого возможного фрагмента со всеми возможными комбинациями префикса квантора, функциональной арности, арности предиката и равенства/отсутствия равенства.

процедуры принятия Практические решений

Наличие практических процедур принятия решений для классов логических формул представляет значительный интерес для проверки программ и схем. Чисто логические формулы обычно решаются с использованием методов решения SAT, основанных на алгоритме DPLL .

Для более общих задач решения теорий первого порядка конъюнктивные формулы над линейной вещественной или рациональной арифметикой могут быть решены с использованием симплекс-алгоритма , формулы в линейной целочисленной арифметике ( арифметика Пресбургера ) могут быть решены с использованием алгоритма Купера или Уильяма Пью Омега-теста . Формулы с отрицаниями, конъюнктами и дизъюнкциями сочетают в себе трудности проверки выполнимости с трудностью решения конъюнкций; в настоящее время они обычно решаются с использованием методов SMT-решения , которые сочетают в себе решение SAT с процедурами принятия решений для соединений и методов распространения. Действительная полиномиальная арифметика, также известная как теория действительных замкнутых полей , разрешима; это теорема Тарского-Зейденберга , которая была реализована в компьютерах с помощью цилиндрического алгебраического разложения .

См. также [ править ]

Примечания [ править ]

^ Дэвид Гильберт и Вильгельм Акерманн. Основные принципы теоретической логики. Шпрингер, Берлин, Германия, 1928 год. Английский перевод: Дэвид Гильберт и Вильгельм Акерманн. Принципы математической логики. Издательство AMS Chelsea Publishing, Провиденс, Род-Айленд, США, 1950 г.
↑ Статья Чёрча была представлена Американскому математическому обществу 19 апреля 1935 года и опубликована 15 апреля 1936 года. Тьюринг, добившийся значительного прогресса в описании своих собственных результатов, был разочарован, узнав о доказательстве Чёрча после его публикации (см. переписку между Максом Ньюман и Чёрч в документах Алонзо Чёрча ). Тьюринг быстро завершил свою статью и поспешил ее опубликовать; он был получен в Трудах Лондонского математического общества 28 мая 1936 г., прочитан 12 ноября 1936 г. и опубликован в серии 2, том 42 (1936–7); он появился в двух разделах: в Части 3 (страницы 230–240), выпущенной 30 ноября 1936 года, и в Части 4 (страницы 241–265), выпущенной 23 декабря 1936 года; Тьюринг добавил исправления в том 43 (1937), стр. 544–546. См. сноску в конце Soare: 1996.
^ Дэвис 2001 , стр. 3–20
^ Ходжес 1983 , с. 91
^ Kline, G. L.; Anovskaa, S. A. (1951), "Review of Foundations of mathematics and mathematical logic by S. A. Yanovskaya", Journal of Symbolic Logic, 16 (1): 46–48, doi:10.2307/2268665, JSTOR 2268665, S2CID 119004002
^ Ходжес 1983 , с. 92, цитата из Гильберта
^ Перейти обратно: ^а ^б Пратт-Хартманн, Ян (30 марта 2023 г.). Фрагменты логики первого порядка . Издательство Оксфордского университета. ISBN 978-0-19-196006-2 .
^ Б. Трахтенброт. Невозможность алгоритма решения проблемы для конечных моделей . Доклады Академии Наук, 70:572–596, 1950. Английский перевод: AMS Translations Series 2, vol. 33 (1963), стр. 1–6.
^ Бернейс, Пол; Шенфинкель, Моисей (декабрь 1928 г.). «О решении задач математической логики» . Математические анналы (на немецком языке). 99 (1): 342–372. дои : 10.1007/BF01459101 . ISSN 0025-5831 . S2CID 122312654 .
^ Акерманн, Вильгельм (1 декабря 1928 г.). «О выполнимости некоторых счетных выражений» . Математические анналы (на немецком языке). 100 (1): 638–649. дои : 10.1007/BF01448869 . ISSN 1432-1807 . S2CID 119646624 .
^ Бёргер, Эгон; Гредель, Эрих; Гуревич, Юрий; Гуревич, Юрий (2001). Классическая проблема решения . Университетский текст (2-е издание 1-го изд.). Берлин: Шпрингер. ISBN 978-3-540-42324-9 .

Ссылки [ править ]

Гильберт, Дэвид ; Акерманн, Вильгельм (1928). математической логики ( Основы на немецком языке). Издательство Спрингер . ISBN 0821820249 .
Алонзо Чёрч , «Неразрешимая проблема элементарной теории чисел », American Journal of Mathematics, 58 (1936), стр. 345–363.
Алонзо Чёрч , «Заметка о проблеме Entscheidungs», Journal of Символическая логика, 1 (1936), стр. 40–41.
Дэвис, Мартин (2001). Логические машины: математики и происхождение компьютера . Norton в мягкой обложке (1. Опубликовано под ред. Norton в мягкой обложке). Нью-Йорк, Нью-Йорк Лондон: Нортон. ISBN 978-0-393-32229-3 .
Алан Тьюринг , « О вычислимых числах с применением к проблеме Entscheidungs », Труды Лондонского математического общества , серия 2, 42 (1936–7), стр. 230–265. Онлайн-версии: с сайта журнала , из Turing Digital Archive , с abelard.org . Опечатки появились в серии 2, 43 (1937), стр. 544–546.
Дэвис, Мартин , «Неразрешимые, основные статьи о неразрешимых предложениях, неразрешимых проблемах и вычислимых функциях», Raven Press, Нью-Йорк, 1965. Статья Тьюринга занимает третье место в этом томе. Среди статей есть статьи Гёделя, Чёрча, Россера, Клини и Поста.
Ходжес, Эндрю (1983). Алан Тьюринг: загадка . Нью-Йорк: Саймон и Шустер. ISBN 978-0-671-49207-6 . Биография Алана М. Тьюринга. См. главу «Дух истины», где представлена история, ведущая к его доказательству, и его обсуждение.
Соаре, Роберт И. , «Вычислимость и рекурсия», Bull. Символическая логика 2 (1996), вып. 3, 284–321.
Тулмин, Стивен , «Падение гения», рецензия на книгу « Алан Тьюринг: Загадка Эндрю Ходжеса», в The New York Review of Books, 19 января 1984 г., стр. 3 и далее.
Уайтхед, Альфред Норт ; Рассел, Бертран , Principia Mathematica to *56, Cambridge at University Press, 1962. В отношении проблемы парадоксов авторы обсуждают проблему, заключающуюся в том, что множество не должно быть объектом ни в одной из своих «определяющих функций», в частности « Введение, гл. 1 стр. 24 «...трудности, возникающие в формальной логике», и гл. 2.I. «Принцип порочного круга» стр. 37 и далее, и гл. 2.VIII. .60 и далее.

Внешние ссылки [ править ]

Словарное определение проблемы треффунгс в Викисловаре

[1] Дэвид Гильберт и Вильгельм Акерманн. Основные принципы теоретической логики. Шпрингер, Берлин, Германия, 1928 год. Английский перевод: Дэвид Гильберт и Вильгельм Акерманн. Принципы математической логики. Издательство AMS Chelsea Publishing, Провиденс, Род-Айленд, США, 1950 г.

[2] Статья Чёрча была представлена Американскому математическому обществу 19 апреля 1935 года и опубликована 15 апреля 1936 года. Тьюринг, добившийся значительного прогресса в описании своих собственных результатов, был разочарован, узнав о доказательстве Чёрча после его публикации (см. переписку между Максом Ньюман и Чёрч в документах Алонзо Чёрча ). Тьюринг быстро завершил свою статью и поспешил ее опубликовать; он был получен в Трудах Лондонского математического общества 28 мая 1936 г., прочитан 12 ноября 1936 г. и опубликован в серии 2, том 42 (1936–7); он появился в двух разделах: в Части 3 (страницы 230–240), выпущенной 30 ноября 1936 года, и в Части 4 (страницы 241–265), выпущенной 23 декабря 1936 года; Тьюринг добавил исправления в том 43 (1937), стр. 544–546. См. сноску в конце Soare: 1996.

[3] Дэвис 2001 , стр. 3–20

[4] Ходжес 1983 , с. 91

[Kline-5] Kline, G. L.; Anovskaa, S. A. (1951), "Review of Foundations of mathematics and mathematical logic by S. A. Yanovskaya", Journal of Symbolic Logic, 16 (1): 46–48, doi:10.2307/2268665, JSTOR 2268665, S2CID 119004002

[6] Ходжес 1983 , с. 92, цитата из Гильберта

[:0-7] Перейти обратно: ^а ^б Пратт-Хартманн, Ян (30 марта 2023 г.). Фрагменты логики первого порядка . Издательство Оксфордского университета. ISBN 978-0-19-196006-2 .

[8] Б. Трахтенброт. Невозможность алгоритма решения проблемы для конечных моделей . Доклады Академии Наук, 70:572–596, 1950. Английский перевод: AMS Translations Series 2, vol. 33 (1963), стр. 1–6.

[9] Бернейс, Пол; Шенфинкель, Моисей (декабрь 1928 г.). «О решении задач математической логики» . Математические анналы (на немецком языке). 99 (1): 342–372. дои : 10.1007/BF01459101 . ISSN 0025-5831 . S2CID 122312654 .

[10] Акерманн, Вильгельм (1 декабря 1928 г.). «О выполнимости некоторых счетных выражений» . Математические анналы (на немецком языке). 100 (1): 638–649. дои : 10.1007/BF01448869 . ISSN 1432-1807 . S2CID 119646624 .

[11] Бёргер, Эгон; Гредель, Эрих; Гуревич, Юрий; Гуревич, Юрий (2001). Классическая проблема решения . Университетский текст (2-е издание 1-го изд.). Берлин: Шпрингер. ISBN 978-3-540-42324-9 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

Теорема о полноте ​