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

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

Теорема

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

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

История проблемы

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

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

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

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

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

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

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

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

Обобщения

Основная статья: Разрешимость (логика) § Разрешимость теории

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

Фрагменты

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

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

Некоторые обозначения: ${\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$, оба ${\rm {{Sat}(\exists ^{n}\forall ^{*})}}$ и ${\rm {{Sat}([\exists ^{n}\forall ^{*}]_{=})}}$ являются NEXPTIME-полными (теорема 5.1).
  • Это означает, что ${\rm {{Sat}([\exists ^{*}\forall ^{*}]_{=})}}$ разрешима — результат, впервые опубликованный Бернейсом и Шенфинкелем.
• Для любого $n\geq 0,m\geq 2$, ${\rm {{Sat}(\exists ^{n}\forall \exists ^{m})}}$ является EXPTIME полным (раздел 5.4.1).
• Для любого $n\geq 0$, ${\rm {{Sat}([\exists ^{n}\forall \exists ^{*}]_{=})}}$ является NEXPTIME-завершенным (раздел 5.4.2).
  • Это означает, что ${\rm {{Sat}(\exists ^{*}\forall ^{*}\exists ^{*})}}$ разрешима — результат, впервые опубликованный Аккерманом.
• Для любого $n\geq 0$, ${\rm {{Sat}(\exists ^{n}\forall \exists )}}$ и ${\rm {{Sat}([\exists ^{n}\forall \exists ]_{=})}}$ являются PSPACE-полными (раздел 5.4.3).

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

процедуры

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

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

См. также

• Автоматизированное доказательство теорем
• Вторая проблема Гильберта
• машина Oracle
• Доказательство Тьюринга

Ссылки

• Гильберт, Дэвид ; Акерманн, Вильгельм (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 и далее.

Внешние ссылки

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