Неразрешимость задачи об определении

Введение

Невозможная задача в вычислениях

В математике и информатике — это задача, поставленная Дэвидом Гильбертом и Вильгельмом Акерманном в 1928 году. Задача заключается в создании алгоритма, который принимает на вход утверждение и отвечает "да" или "нет" в зависимости от того, является ли утверждение универсально истинным, то есть истинным во всех структурах.

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

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

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

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

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

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

Before the question could be answered, the notion of "algorithm" had to be formally defined. This was done by Alonzo Church in 1935 with the concept of "effective calculability" based on his λ calculus, and by Alan Turing the next year with his concept of Turing machines. Turing immediately recognized that these are equivalent models of computation. A negative answer to the Entscheidungsproblem was then given by Alonzo Church in 1935–36 (Church's theorem) and independently shortly thereafter by Alan Turing in 1936 (Turing's proof). Church proved that there is no computable function which decides, for two given λ calculus expressions, whether they are equivalent or not. He relied heavily on earlier work by Stephen Kleene. Turing reduced the question of the existence of an 'algorithm' or 'general method' able to solve the Entscheidungsproblem to the question of the existence of a 'general method' which decides whether any given Turing machine halts or not (the halting problem). If 'algorithm' is understood as meaning a method that can be represented as a Turing machine, and with the answer to the latter question negative (in general), the question about the existence of an algorithm for the Entscheidungsproblem also must be negative (in general). In his 1936 paper, Turing says: "Corresponding to each computing machine 'it' we construct a formula 'Un(it)' and we show that, if there is a general method for determining whether 'Un(it)' is provable, then there is a general method for determining whether 'it' ever prints 0". The work of both Church and Turing was heavily influenced by Kurt Gödel's earlier work on his incompleteness theorem, especially by the method of assigning numbers (a Gödel numbering) to logical formulas in order to reduce logic to arithmetic. The Entscheidungsproblem is related to Hilbert's tenth problem, which asks for an algorithm to decide whether Diophantine equations have a solution. The non existence of such an algorithm, established by the work of Yuri Matiyasevich, Julia Robinson, Martin Davis, and Hilary Putnam, with the final piece of the proof in 1970, also implies a negative answer to the Entscheidungsproblem.

Обобщения

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

Фрагменты

По умолчанию, ссылки в разделе приводятся из Pratt Hartmann (2023). Классическая проблема разрешимости (Entscheidungsproblem) ставит вопрос, истинна ли данная формула первого порядка во всех моделях. Факторная проблема спрашивает, истинна ли она во всех конечных моделях. Теорема Трахтенброта показывает, что и эта проблема также неразрешима. Для любого , является EXPTIME-полной (раздел 5.4.1). Для любого , является NEXPTIME-полной (раздел 5.4.2). Из этого следует, что является разрешимой, результат, впервые опубликованный Аккерманном. Для любого , и являются PSPACE-полными (раздел 5.4.3). Börger et al. (2001) описывает уровень вычислительной сложности для каждого возможного фрагмента с каждой возможной комбинацией префикса кванторов, функциональной арности, предикатной арности и наличия/отсутствия равенства.

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

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