Математическая логика
Рекурсивные функции и теория вычислимости
1936 год: три математика независимо формализуют понятие «вычисление» - Черч через λ-исчисление, Тьюринг через машины, Гёдель и Эрбран через рекурсивные функции. Три совершенно разных подхода. И все три - одно и то же. Это совпадение настолько поразительно, что стало основой тезиса Черча-Тьюринга: любое интуитивно вычислимое есть рекурсивно вычислимое.
- Теорема о неполноте Гёделя использует примитивно рекурсивную арифметику
- Доказательство PH полноты (NP-полнота SAT) требует понятия вычислимости
- Системы типов с зависимыми типами - функции, гарантированно завершающиеся
Три независимых формализации вычислимости
В 1936 году произошло одно из величайших совпадений в математике: Алан Тьюринг и Алонзо Чёрч независимо опубликовали формализации понятия «алгоритм». Тьюринг - через машины с лентой, Чёрч - через λ-исчисление. Стефан Клини доказал эквивалентность обоих подходов рекурсивным функциям Гёделя-Эрбрана.
Примитивно рекурсивные функции
Примитивно рекурсивные функции строятся из базовых функций (нуль, следующий, проекция) тремя операциями: подстановкой и примитивной рекурсией. Все они гарантированно завершаются.
Примитивно рекурсивные функции не охватывают все вычислимые функции. Функция Аккермана A(m,n) вычислима, но не примитивно рекурсивна: она растёт быстрее любой примитивно рекурсивной функции.
Почему примитивно рекурсивные функции гарантированно завершаются?
μ-рекурсивные функции
Класс μ-рекурсивных (частично рекурсивных) функций добавляет операцию минимизации (μ-оператор): μy[f(x,y)=0] - наименьшее y, при котором f(x,y)=0. Эта операция может не завершиться. Это расширяет класс до всех вычислимых частичных функций.
Что добавляет μ-оператор к классу функций по сравнению с примитивно рекурсивными?
Тезис Чёрча-Тьюринга
Тезис Чёрча-Тьюринга: любая «эффективно вычислимая» функция является рекурсивной (и вычислимой машиной Тьюринга, и λ-исчислением). Это тезис, а не теорема - он не имеет строгого доказательства, поскольку «эффективно вычислимый» - неформальное понятие.
Тезис Чёрча-Тьюринга - основа всей теории вычислений. На него опираются все доказательства неразрешимости: если задача не решается машиной Тьюринга, то «в принципе неразрешима» никаким алгоритмом.
Почему тезис Чёрча-Тьюринга является тезисом (гипотезой), а не теоремой?
Неразрешимость и теорема об остановке
Проблема остановки: не существует алгоритма, который для произвольной программы P и входа x определяет, завершится ли P(x) или будет работать бесконечно. Тьюринг доказал это в 1936 году, тем же диагональным аргументом.
Из неразрешимости остановки выводятся сотни других неразрешимых задач: Post Correspondence Problem, тождественность слов в группах, определение эквивалентности двух программ, выполнимость Диофантовых уравнений (теорема Матиясевича-Робинсон-Дэвис-Путнэм).
Квантовые компьютеры могут решить проблему остановки
Квантовые компьютеры вычисляют то же множество функций, что и классические машины Тьюринга (тезис КТ не нарушен). Квантовое ускорение - в сложности вычисления, а не в расширении множества разрешимых задач.
Неразрешимость - это не «слишком долго», а «принципиально невозможно». Квантовое ускорение не помогает с задачами, которые невозможны в принципе.
Неразрешимость и теорема об остановке?
Review the concept above.
Рекурсивные функции и вычислимость: ключевые идеи
- Примитивно рекурсивные функции: строятся из базовых операций, гарантированно завершаются
- μ-рекурсивные функции: добавляют минимизацию, порождают частичные (незавершающиеся) функции
- Тезис Чёрча-Тьюринга: три формализации вычислимости эквивалентны
- Проблема остановки: нет алгоритма, решающего её для всех программ (диагональный аргумент)
- Неразрешимость - принципиальное ограничение, не снимаемое ускорением или квантовыми компьютерами
Вычислимость и математическая логика
Связь между рекурсивными функциями и теоремами о неполноте Гёделя глубока: предикат Provable(n) примитивно рекурсивен, что и позволяет строить самореференцию. Тьюринг независимо пришёл к аналогичным результатам через задачу Entscheidungsproblem.
- ml-06 — Related lesson
Вопросы для размышления
- Если HALT(P,P) неразрешима, то почему антивирусы успешно находят вредоносные программы? В чём разница?
- Теорема Райса: любое содержательное свойство поведения программы неразрешимо. Как это влияет на статический анализ кода?
- Функция Бобра (Busy Beaver) растёт быстрее любой вычислимой функции. Почему её значения принципиально нельзя вычислить для больших n?