Алгоритмическая разрешимость: различия между версиями

[отпатрулированная версия][непроверенная версия]
Содержимое удалено Содержимое добавлено
м исправление ссылка
Нет описания правки
Строка 5:
Понятия алгоритма и аксиоматической системы имеют давнюю историю. И то и другое известно ещё со времён [[античность|античности]]. Достаточно вспомнить [[Евклидова геометрия|постулаты геометрии]] [[Евклид]]а и [[алгоритм Евклида|алгоритм нахождения наибольшего общего делителя]] того же Евклида. Несмотря на это, чёткого математического определения исчисления и особенно алгоритма не существовало очень долгое время. Особенность проблемы, связанной с формальным определением неразрешимости состояла в том, что для того, чтобы показать, что некоторый алгоритм существует, достаточно его просто найти и продемонстрировать. Если же алгоритм не находится, возможно его не существует и это тогда требуется строго доказать. А для этого нужно точно знать, что такое алгоритм.
 
Большой прогресс в формализации этих понятий был достигнут в начале [[XX векстолетие|XX-го столетия]]а [[Гильберт, Давид|Гильбертом]] и его школой. Тогда, сначала, сформировались понятия исчисления и формального вывода, а затем Гильбертом же, в его знаменитой [[программа Гильберта|программе обоснования математики]] была поставлена амбициозная цель формализации всей математики. Это предусматривало, в том числе, возможность автоматической проверки любой математической формулы на предмет истинности. Отталкиваясь от работ Гильберта [[Гёдель, Курт|Гёдель]] впервые описал класс так называемых [[рекурсивная функция|рекурсивных функций]], с помощью которой доказал свои знаменитые [[теоремы Гёделя о неполноте|теоремы о неполноте]]. Впоследствии был введён ряд других формализмов, таких как [[машина Тьюринга]], [[лямбда-исчисление|λ-исчисление]], оказавшихся эквивалентными рекурсивным функциям. В настоящее время, каждый из них считается формальным эквивалентом интуитивного понятия вычислимой функции. Эта эквивалентность постулируется [[тезис Чёрча|тезисом Чёрча]].
 
Когда понятия исчисления и алгоритма были уточнены, последовал ряд результатов о неразрешимости различных теорий. Одним из первых таких результатов была теорема, доказанная [[Новиков, Пётр Сергеевич|Новиковым]], о неразрешимости [[проблема слов|проблемы слов]] в [[группа]]х. Разрешимые же теории были известны задолго до этого.