Entscheidungsproblem

Невыполнимая задача в вычислительной технике

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

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

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

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

История

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

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

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

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

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

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

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

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

Обобщения

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

Фрагменты

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

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

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

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

Аристотелевский и реляционный

Аристотелевская логика рассматривает 4 вида предложений: «Все p есть q», «Все p не есть q», «Некоторые p есть q», «Некоторые p не есть q». Мы можем формализовать эти виды предложений как фрагмент логики первого порядка: где — атомарные предикаты, и . Учитывая конечный набор формул аристотелевской логики, NLOGSPACE -полно решить, что . Также NLOGSPACE-полно решить, что небольшое расширение (теорема 2.7): Реляционная логика расширяет аристотелевскую логику, допуская реляционный предикат. Например, «Все любят кого-то» можно записать как . В общем случае у нас есть 8 видов предложений: NLOGSPACE - полно решить, что (теорема 2.15). Реляционную логику можно расширить до 32 видов предложений, разрешив , но это расширение является EXPTIME -полным (теорема 2.24). $${\displaystyle \forall x,p(x)\to \pm q(x),\quad \exists x,p(x)\wedge \pm q(x)}$$ ${\displaystyle p,q}$ ${\displaystyle +q:=q,\;-q:=\neg q}$ ${\displaystyle {\rm {Sat}}}$ ${\displaystyle {\rm {Sat}}}$ $${\displaystyle \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)}}}}}}}$ $${\displaystyle {\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}}}$$ ${\displaystyle {\rm {Sat}}}$ ${\displaystyle \pm p,\pm q}$

Арити

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

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

Префикс квантификатора

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

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

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

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

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

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

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

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

Смотрите также

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

Примечания

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
5. Клайн, GL; Ановская, SA (1951), «Обзор основ математики и математической логики С.А. Яновской», Журнал символической логики , 16 (1): 46–48, doi :10.2307/2268665, JSTOR  2268665, S2CID  119004002
6. Hodges 1983, стр. 92, цитата из Гильберта
7. Pratt-Hartmann, Ian (30 марта 2023 г.). Фрагменты логики первого порядка. Oxford University Press. ISBN 978-0-19-196006-2.
8. Б. Трахтенброт. Невозможность алгоритма для задачи принятия решения для конечных моделей . Доклады Академии Наук, 70:572–596, 1950. Английский перевод: AMS Translations Series 2, т. 33 (1963), стр. 1–6.
9. Бернейс, Пол; Шенфинкель, Моисей (декабрь 1928 г.). «Zum Entscheidungsproblem der Mathematischen Logik». Mathematische Annalen (на немецком языке). 99 (1): 342–372. дои : 10.1007/BF01459101. ISSN  0025-5831. S2CID  122312654.
10. Акерманн, Вильгельм (1 декабря 1928 г.). «Über die Erfüllbarkeit gewisser Zählausdrücke». Mathematische Annalen (на немецком языке). 100 (1): 638–649. дои : 10.1007/BF01448869. ISSN  1432-1807. S2CID  119646624.
11. Бёргер, Эгон; Гредель, Эрих; Гуревич, Юрий; Гуревич, Юрий (2001). Классическая проблема решения . Университеттекст (2-е издание 1-го изд.). Берлин: Шпрингер. ISBN 978-3-540-42324-9.

Ссылки

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

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

• Словарное определение entscheidungsproblem в Викисловаре