В математике и информатике , то проблема разрешения ( произносится [ɛntʃaɪ̯dʊŋspʁoˌbleːm] , немецкий для «проблемы решения») является проблема , порождаемая Давида Гильберта и Вильгельм Аккерман в 1928 году [1] Проблема просит для алгоритма , который учитывает, в качестве входных данных, а утверждение и отвечает «Да» или «Нет» в зависимости от того, является ли утверждение универсальным , т. е. действительным в каждой структуре, удовлетворяющей аксиомам.
Теорема полноты
Согласно теореме о полноте логики первого порядка , утверждение универсально справедливо тогда и только тогда, когда оно может быть выведено из аксиом, поэтому Entscheidungsproblem также может рассматриваться как запрос алгоритма, чтобы решить, доказуемо ли данное утверждение из аксиом. используя правила логики .
В 1936 году Алонзо Черч и Алан Тьюринг опубликовали независимые статьи [2], показывающие, что общее решение проблемы Entscheidungs невозможно, если предположить, что интуитивное понятие « эффективно вычислимого» улавливается функциями, вычисляемыми машиной Тьюринга (или, что эквивалентно, те, которые можно выразить в лямбда-исчислении ). Это предположение теперь известно как тезис Черча – Тьюринга .
История проблемы
Происхождение проблемы Entscheidungs восходит к Готфриду Лейбницу , который в семнадцатом веке, после создания успешной механической вычислительной машины , мечтал построить машину, которая могла бы манипулировать символами, чтобы определять значения истинности математических утверждений. [3] Он понял, что первым шагом должен быть чистый формальный язык , и большая часть его последующей работы была направлена на достижение этой цели. В 1928 году Давид Гильберт и Вильгельм Акерманн поставили вопрос в изложенной выше форме.
В продолжение своей «программы» Гильберт задал три вопроса на международной конференции в 1928 году, третий из которых стал известен как « Entscheidungsproblem Гильберта» . [4] В 1929 году Моисей Шенфинкель опубликовал одну статью о частных случаях проблемы принятия решений, которую подготовил Пол Бернейс . [5]
Еще в 1930 году Гильберт считал, что неразрешимой проблемы не будет. [6]
Отрицательный ответ
Прежде чем можно было ответить на вопрос, нужно было формально определить понятие «алгоритм». Это было сделано Алонзо Черчем в 1935 году с концепцией «эффективной вычислимости», основанной на его λ-исчислении, и Аланом Тьюрингом в следующем году с его концепцией машин Тьюринга . Тьюринг сразу понял, что это эквивалентные модели вычислений .
Отрицательный ответ на проблему Entscheidungs затем был дан Алонзо Черчем в 1935–36 годах ( теорема Черча ) и независимо вскоре после этого Аланом Тьюрингом в 1936 году ( доказательство Тьюринга ). Чёрч доказал, что не существует вычислимой функции, которая решала бы для двух заданных выражений λ-исчисления, эквивалентны они или нет. Он во многом полагался на более ранние работы Стивена Клини . Тьюринг свел вопрос о существовании «общего метода», который решает, останавливается ли данная машина Тьюринга или нет ( проблема остановки ), к вопросу о существовании «алгоритма» или «общего метода», способного решить проблему Entscheidungs . Если «алгоритм» понимается как эквивалент машины Тьюринга и с отрицательным ответом на последний вопрос (в общем), вопрос о существовании алгоритма для Entscheidungsproblem также должен быть отрицательным (в общем). В своей статье 1936 года Тьюринг говорит: «В соответствии с каждой вычислительной машиной 'it' мы строим формулу 'Un (it)' и показываем, что, если существует общий метод определения доказуемости 'Un (it)', затем существует общий метод определения того, выводит ли "оно" когда-либо 0 " .
На работу Чёрча и Тьюринга сильно повлияла более ранняя работа Курта Гёделя над его теоремой о неполноте , особенно методом присвоения чисел ( нумерация Гёделя ) логическим формулам, чтобы свести логику к арифметике.
Проблема Entscheidungs связана с десятой проблемой Гильберта , которая требует алгоритма, чтобы определить, есть ли решение у диофантовых уравнений . Отсутствие такого алгоритма, установленного Юрием Матиясевичем в 1970 году, также подразумевает отрицательный ответ на проблему Entscheidungs.
Некоторые теории первого порядка разрешимы алгоритмически; Примеры этого включают арифметику Пресбургера , реальные закрытые поля и системы статических типов многих языков программирования . Однако общая теория натуральных чисел первого порядка, выраженная в аксиомах Пеано, не может быть решена с помощью алгоритма.
Практические процедуры принятия решений
Наличие практических процедур принятия решений для классов логических формул представляет значительный интерес для верификации программ и схем. Чистые булевы логические формулы обычно решаются с использованием методов решения SAT , основанных на алгоритме DPLL . Присоединительные формулы над линейной реальной или рациональной арифметикой могут быть решены с помощью симплексного алгоритма , формулы в линейном целочисленных арифметической ( Пресбургере арифметике ) могут быть решены с помощью алгоритма Купера или Уильям Пью «s тест Omega . Формулы с отрицаниями, союзами и дизъюнкциями сочетают в себе трудности проверки выполнимости с трудностями определения союзов; в настоящее время они обычно решаются с использованием методов SMT-решения , которые сочетают SAT-решение с процедурами принятия решения для соединений и методов распространения. Действительная полиномиальная арифметика, также известная как теория вещественных замкнутых полей , разрешима; это теорема Тарского – Зайденберга , реализованная в компьютерах с использованием цилиндрического алгебраического разложения .
Смотрите также
- Разрешимость (логика)
- Автоматическое доказательство теорем
- Вторая проблема Гильберта
- Машина Oracle
- Доказательство Тьюринга
Заметки
- ^ Дэвид Гильберт и Вильлем Аккерманн. Grundzüge der Theoretischen Logik. Шпрингер, Берлин, Германия, 1928. Английский перевод: Давид Гильберт и Вильгельм Аккерманн. Принципы математической логики. AMS Chelsea Publishing, Провиденс, Род-Айленд, США, 1950.
- ↑ Статья Черча была представлена Американскому математическому обществу 19 апреля 1935 года и опубликована 15 апреля 1936 года. Тьюринг, добившийся значительного прогресса в написании собственных результатов, был разочарован, узнав о доказательстве Черча после его публикации (см. Переписку между Максом Ньюман и Черч в документах Алонзо Черча ). Тьюринг быстро завершил свою статью и поспешил ее опубликовать; он был получен Трудами Лондонского математического общества 28 мая 1936 г., прочитан 12 ноября 1936 г. и опубликован в серии 2, том 42 (1936–197); он состоял из двух разделов: в части 3 (страницы 230–240), выпущенной 30 ноября 1936 г., и в части 4 (страницы 241–265), выпущенной 23 декабря 1936 года; Тьюринг внес исправления в том 43 (1937), стр. 544–546. См. Сноску в конце Soare: 1996.
- Перейти ↑ Davis 2000: pp. 3–20
- ^ Ходжес стр. 91
- ^ Клайн, GL; Anovskaa, SA (1951), "Обзор Основы математики и математической логики С. А. Яновская", журнал символической логики , 16 (1): 46-48, DOI : 10,2307 / 2268665 , JSTOR 2268665
- ^ Ходжес стр. 92, цитата из Гильберта
Рекомендации
- Давид Гильберт и Вильгельм Аккерманн (1928). Grundzüge der Theoretischen Logik ( Принципы математической логики ). Спрингер-Верлаг, 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 », Proceedings of the London Mathematical Society , Series 2, 42 (1936–7), pp 230–265. Онлайн-версии: с сайта журнала [ мертвая ссылка ] , из Turing Digital Archive , с 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 the University Press, 1962. Что касается проблемы парадоксов, то авторы обсуждают проблему того, что множество не может быть объектом ни в одной из своих «определяющих функций», в в частности, «Введение, гл. 1, стр. 24« ... трудности, возникающие в формальной логике », и гл. 2.I.« Принцип порочного круга », стр. 37ff, и гл. 2.VIII.« Противоречия ». "стр. 60 и сл.
Внешние ссылки
- Словарное определение entscheidungsproblem в Викисловаре