Entscheidungsproblem -Entscheidungsproblem
В математике и информатике , то проблема разрешения ( произносится [ɛntʃaɪ̯dʊŋspʁoˌbleːm] , немецкий для «проблемы решения») является проблема , порождаемая Давида Гильберта и Вильгельм Аккерман в 1928 г. Проблема запрашивает алгоритм , который учитывает, в качестве входных данных, заявление и ответы «Да» или «Нет» в зависимости от того, является ли утверждение универсальным , т. Е. Действительным для каждой структуры, удовлетворяющей аксиомам.
Теорема полноты
Согласно теореме о полноте логики первого порядка , утверждение универсально справедливо тогда и только тогда, когда оно может быть выведено из аксиом, поэтому Entscheidungsproblem также может рассматриваться как запрос алгоритма, чтобы решить, доказуемо ли данное утверждение из аксиом. используя правила логики .
В 1936 году Алонзо Черч и Алан Тьюринг опубликовали независимые статьи, показывающие, что общее решение проблемы Entscheidungs невозможно, если предположить, что интуитивное понятие « эффективно вычислимого» улавливается функциями, вычисляемыми машиной Тьюринга (или, что эквивалентно, теми, которые выражаются в лямбда - исчисление ). Это предположение теперь известно как тезис Черча – Тьюринга .
История проблемы
Происхождение проблемы Entscheidungs восходит к Готфриду Лейбницу , который в семнадцатом веке, построив успешную механическую вычислительную машину , мечтал построить машину, которая могла бы манипулировать символами, чтобы определять значения истинности математических утверждений. Он понял, что первым шагом должен быть чистый формальный язык , и большая часть его последующей работы была направлена на достижение этой цели. В 1928 году Давид Гильберт и Вильгельм Акерманн поставили вопрос в изложенной выше форме.
В продолжение своей «программы» Гильберт задал три вопроса на международной конференции в 1928 году, третий из которых стал известен как « Entscheidungsproblem Гильберта» . В 1929 году Моисей Шенфинкель опубликовал одну статью о частных случаях проблемы принятия решений, которую подготовил Пол Бернейс .
Еще в 1930 году Гильберт считал, что неразрешимой проблемы не будет.
Отрицательный ответ
Прежде чем можно было ответить на вопрос, нужно было формально определить понятие «алгоритм». Это было сделано Алонзо Черчем в 1935 году с концепцией «эффективной вычислимости», основанной на его λ-исчислении, и Аланом Тьюрингом в следующем году с его концепцией машин Тьюринга . Тьюринг сразу понял, что это эквивалентные модели вычислений .
Отрицательный ответ на проблему Entscheidungs затем был дан Алонзо Черчем в 1935–36 годах ( теорема Черча ) и независимо вскоре после этого Аланом Тьюрингом в 1936 году ( доказательство Тьюринга ). Чёрч доказал, что не существует вычислимой функции, которая решала бы для двух заданных выражений λ-исчисления, эквивалентны они или нет. Он во многом полагался на более ранние работы Стивена Клини . Тьюринг свел вопрос о существовании «общего метода», который решает, останавливается ли данная машина Тьюринга или нет ( проблема остановки ), к вопросу о существовании «алгоритма» или «общего метода», способного решить проблему Entscheidungs . Если «алгоритм» понимается как эквивалент машины Тьюринга и с отрицательным ответом на последний вопрос (в общем), вопрос о существовании алгоритма для Entscheidungsproblem также должен быть отрицательным (в общем). В своей статье 1936 года Тьюринг говорит: «В соответствии с каждой вычислительной машиной 'it' мы строим формулу 'Un (it)' и показываем, что если существует общий метод определения доказуемости 'Un (it)', тогда существует общий метод определения того, выводит ли "оно" когда-либо 0 " .
На работу Чёрча и Тьюринга сильно повлияла более ранняя работа Курта Гёделя над его теоремой о неполноте , особенно методом присвоения чисел ( нумерация Гёделя ) логическим формулам, чтобы свести логику к арифметике.
Проблема Entscheidungs связана с десятой проблемой Гильберта , которая требует от алгоритма определения, есть ли решение у диофантовых уравнений . Отсутствие такого алгоритма, установленного Юрием Матиясевичем в 1970 году, также подразумевает отрицательный ответ на проблему Entscheidungs.
Некоторые теории первого порядка разрешимы алгоритмически; Примеры этого включают арифметику Пресбургера , реальные закрытые поля и системы статических типов многих языков программирования . Однако общая теория натуральных чисел первого порядка, выраженная в аксиомах Пеано, не может быть решена с помощью алгоритма.
Практические процедуры принятия решений
Наличие практических процедур принятия решений для классов логических формул представляет значительный интерес для верификации программ и схем. Чистые булевы логические формулы обычно решаются с использованием методов решения SAT , основанных на алгоритме DPLL . Присоединительные формулы над линейной реальной или рациональной арифметикой могут быть решены с помощью симплексного алгоритма , формулы в линейном целочисленных арифметической ( Пресбургере арифметике ) могут быть решены с помощью алгоритма Купера или Уильям Пью «s тест Omega . Формулы с отрицаниями, союзами и дизъюнкциями сочетают в себе трудности проверки выполнимости с трудностями определения союзов; в настоящее время они обычно решаются с использованием методов SMT-решения , которые сочетают SAT-решение с процедурами принятия решения для соединений и методов распространения. Действительная полиномиальная арифметика, также известная как теория вещественных замкнутых полей , разрешима; это теорема Тарского – Зайденберга , которая была реализована в компьютерах с помощью цилиндрического алгебраического разложения .
Смотрите также
- Разрешимость (логика)
- Автоматическое доказательство теорем
- Вторая проблема Гильберта
- Машина Oracle
- Доказательство Тьюринга
Примечания
использованная литература
- Давид Гильберт и Вильгельм Аккерманн (1928). Grundzüge der Theoretischen Logik ( Принципы математической логики ). Springer-Verlag, ISBN 0-8218-2024-9 .
- Алонзо Черч , «Неразрешимая проблема элементарной теории чисел », American Journal of Mathematics, 58 (1936), стр. 345–363.
- Алонсо Чёрч , «Заметка о проблеме Entscheidungsproblem», Journal of Symbolic Logic, 1 (1936), стр. 40–41.
- Мартин Дэвис , 2000, Двигатели логики , WW Norton & Company, Лондон, ISBN 0-393-32229-7 pbk.
- Алан Тьюринг , « О вычислимых числах в приложении к Entscheidungsproblem », Труды Лондонского математического общества , серия 2, 42 (1936–7), стр 230–265. Онлайн-версии: с сайта журнала , из цифрового архива Тьюринга , из abelard.org . Исправления появились в Series 2, 43 (1937), pp 544–546.
- Мартин Дэвис , «Неразрешимые, основные статьи о неразрешимых предложениях, неразрешимых задачах и вычислимых функциях», Raven Press, New York, 1965. Статья Тьюринга занимает третье место в этом томе. Среди статей - Гедель, Черч, Россер, Клини и Пост.
- Эндрю Ходжес , Алан Тьюринг: Загадка , Саймон и Шустер , Нью-Йорк, 1983. Биография Алана М. Тьюринга. См. Главу «Дух истины» с историей, ведущей к его доказательству, и его обсуждением.
- Роберт Соар , "Вычислимость и рекурсия", Bull. Символическая логика 2 (1996), вып. 3, 284–321.
- Стивен Тулмин , «Падение гения», рецензия на книгу « Алан Тьюринг: Загадка Эндрю Ходжеса», в The New York Review of Books, 19 января 1984 г., стр. 3ff.
- Альфред Норт Уайтхед и Бертран Рассел , Principia Mathematica to * 56, Cambridge at University Press, 1962. Что касается проблемы парадоксов, то авторы обсуждают проблему того, что множество не может быть объектом ни в одной из своих «определяющих функций», в в частности, «Введение, гл. 1, стр. 24« ... трудности, возникающие в формальной логике », и гл. 2.I.« Принцип порочного круга », стр. 37ff, и гл. 2.VIII.« Противоречия ». "стр. 60 и сл.
внешние ссылки
- Словарное определение entscheidungsproblem в Викисловаре