Тезис Чёрча-Тьюринга

1936 год: два математика на разных континентах задают один вопрос 'что значит вычислить?' и получают один ответ. Чёрч - через λ-исчисление, Тьюринг - через воображаемую машину. Выясняется: это одно и то же. И оба устанавливают предел: есть задачи, которые не решит ни один алгоритм - никогда, ни на каком железе.

• **Haskell как λ-исчисление:** Haskell - прямая реализация λ-исчисления с типами. Монады, функторы, аппликативы - это конкретные паттерны λ-терминов. Тезис гарантирует: Haskell вычисляет ровно то, что вычисляет МТ
• **Coq и доказательства:** Coq - язык формальных доказательств, основанный на λ-исчислении с зависимыми типами (CIC). Используется для верификации компилятора CompCert (C), криптографических протоколов (FIPS), математических теорем (4-цветная теорема)
• **Kolmogorov complexity в ML:** несжимаемые строки (высокая K-сложность) - это 'случайные' строки. Overfitting в ML = запоминание случайных данных. MDL (minimum description length) - принцип выбора моделей, основанный на K-сложности
• **Rule 110 - Тьюринг-полный клеточный автомат:** доказано Стивеном Вольфрамом и Мэтью Куком в 2004. Простейшее 1D правило реализует произвольные вычисления - демонстрирует повсеместность вычислений в природе

Тезис: любое вычисление реализуется МТ

1936 год. Алонзо Чёрч и Алан Тьюринг независимо формализовали понятие «алгоритм» - через λ-исчисление и машины Тьюринга соответственно. Удивительное открытие: обе формализации эквивалентны. Из этого Чёрч и Тьюринг сделали смелое предположение, ставшее **тезисом**: любое интуитивно вычислимое значение вычисляется МТ.

**Тезис Чёрча-Тьюринга:** класс функций, вычислимых МТ, совпадает с классом функций, вычислимых «эффективной процедурой» в интуитивном смысле. Это **не теорема** - нельзя математически доказать утверждение о «интуитивном смысле». Это **научный тезис** - подтверждается тем, что все известные модели вычислений оказываются эквивалентными МТ.

λ-исчисление и его эквивалентность МТ

λ-исчисление - система, придуманная Чёрчем в 1932-м: функции, применение, абстракция. Три правила вывода - и этого достаточно для выражения любого алгоритма. Haskell, Erlang, F#, Rust (замыкания), Python (lambda) - всё это реализации λ-исчисления. Чёрч доказал: любая функция, вычислимая МТ, выражается λ-термом. И наоборот.

Теорема Чёрча-Тьюринга (строгая, доказанная): λ-вычислимые функции = рекурсивные функции = МТ-вычислимые функции. Это даёт языку Haskell математическое основание: любая Haskell-программа вычисляет то, что вычисляет МТ. И то, что не вычисляет МТ - не вычисляет и Haskell.

Физический тезис Чёрча-Тьюринга

Усиленная версия тезиса: любой физический процесс может быть симулирован МТ с полиномиальным замедлением. Это смелее оригинального тезиса - он касается не только алгоритмов, но и самой природы. Квантовые вычисления бросили вызов этому тезису: возможно, квантовые системы вычисляют быстрее чем любая классическая МТ.

Модель BCSS (Blum-Cucker-Shub-Smale) над вещественными числами с точной арифметикой **мощнее МТ** - она вычисляет функции, недоступные МТ. Но физические компьютеры не реализуют точную вещественную арифметику - они работают с числами с плавающей точкой (IEEE 754). Поэтому практически физический тезис не нарушается.

Пределы вычислимости

Тезис Чёрча-Тьюринга устанавливает предел: есть задачи, которые **невозможно решить алгоритмически**. Проблема остановки, Post correspondence problem, проверка эквивалентности грамматик - невычислимы. Это не временное ограничение технологий, это математическая теорема.

Понимание пределов вычислимости важно практически: **статический анализ** не может точно определить, является ли программа правильной (теорема Райса). **Компиляторы** не могут полностью оптимизировать произвольный код. **Формальная верификация** ограничена - TLA+ и Coq проверяют только те свойства, которые удаётся закодировать в разрешимой логике.

Ключевые идеи

• **Тезис Чёрча-Тьюринга:** интуитивно вычислимое = МТ-вычислимое. Научный тезис, не теорема - нельзя формально доказать утверждение об 'интуиции'
• **λ-исчисление ≡ МТ ≡ рекурсивные функции:** строгая теорема. Все известные модели вычислений эквивалентны. Квантовые компьютеры быстрее, но не вычисляют больше
• **Физический тезис:** физические процессы симулируются МТ с полиномиальным замедлением. Оспаривается квантовыми вычислениями (по скорости), не по вычислимости
• **Пределы вычислимости:** halting problem, K-сложность, эквивалентность программ - математически невычислимы. Не технологическое ограничение, а предел концепции алгоритма

Связанные темы

Тезис Чёрча-Тьюринга - философское основание всей теории вычислимости:

• Проблема остановки — Первая конкретная невычислимая задача - прямое следствие пределов МТ
• Теорема Райса — Обобщение невычислимости: любое непрямолинейное семантическое свойство программ невычислимо
• Машина Тьюринга — Формальная модель, на которую опирается тезис

Вопросы для размышления

• Тезис Чёрча-Тьюринга нельзя доказать математически. Какие аргументы убеждают в его истинности? Что могло бы его опровергнуть?
• Мозг человека - физическая система. По физическому тезису, его можно симулировать МТ. Означает ли это, что искусственный интеллект принципиально достижим?
• BCSS-модель над точными вещественными числами мощнее МТ. Почему это не противоречит тезису на практике?

Связанные уроки

• comp-02
• ml-10