Разговор с Оракулом

Прошлая глава кончилась вопросом: любой ли точный вопрос имеет ответ, который найдёт машина? Один из таких вопросов встречался нам уже трижды. В главе 0 — три строки про Коллатца, о которых никто не знает, остановятся ли они на каждом числе. В главе 53 — желание написать проверку посильнее проверки типов: программу, которая читает любую программу и говорит, не зависнет ли та. В прошлой главе — симулятор, который умеет только ждать. На вопрос прошлой главы ответ — «нет», но верить на слово не нужно: мы получим этот ответ в споре с тем, кто уверен в обратном.

Глава написана как диалог, по образцу Дугласа Хофштадтера и его книги «Гёдель, Эшер, Бах» (1979): между главами у него беседуют Ахилл и Черепаха, позаимствованные у Льюиса Кэрролла, а через их споры проходят самые трудные идеи книги. Ваш собеседник — Оракул. Это слово — тоже заимствование: в 1938 году Тьюринг в диссертации, написанной в Принстоне под руководством Чёрча, рассматривал машины, которые на трудный вопрос могут обратиться к «оракулу»: как он работает, Тьюринг не объясняет, но ответы его всегда верны. Наш Оракул утверждает, что он и есть такое устройство.

Кёнигсберг, сентябрь 1930

Гёдель накануне подорвал одну половину этой уверенности: не всякое истинное утверждение можно доказать. Об этом — в «Царице наук», в главе о Гёделе. Вторую половину — что для любого точного вопроса найдётся способ отвечать механически — через шесть лет опровергли Чёрч и Тьюринг. К их ответу мы и придём в разговоре.

Прелюдия. Лавка Оракула

Это первая и самая естественная попытка: запустить программу и подождать. Модуль курса cs.oracle содержит такого Оракула: функция halts(source, steps) выполняет программу, считая строки, и если программа не закончилась за steps строк, отвечает «не остановится». Поймать его нетрудно.

Терпеливая программа выполняет две строки на круг — проверку условия и прибавление, — всего 120 002 строки, и в бюджет в сто тысяч не помещается. Оракул объявил её вечной, хотя она закончится через доли секунды. Любой бюджет ломается так же: для лимита в миллион найдётся программа, которой нужен миллион и одна строка.

Сформулируем вопрос, о котором спорим. Проблема остановки — по тексту программы и её входу определить, закончит ли программа работу. Задачу с ответом «да» или «нет» называют разрешимой, если есть программа, которая на любом входе останавливается и даёт верный ответ. Вся тяжесть определения лежит на двух словах. «На любом» — Оракул обязан справляться не только с теми программами, которые ему приятны. «Останавливается» — ответ «подождите ещё» не считается.

Действие первое. Упрямец

Попробуйте сыграть за Оракула. Отвечайте что угодно и сколько угодно раз, меняйте стратегию от раза к разу.

Оракул проигрывает всегда, и дело не в неудачном выборе. Упрямец устроен так, что делает противоположное любому ответу. Значит, верного ответа на вопрос «остановится ли упрямец» Оракул дать не может — а ведь ответ существует: упрямец либо останавливается, либо нет. Остаётся одно: такого Оракула не бывает. Запишем это строго.

Доказательство короче этого абзаца, и в этом его сила: оно не зависит от того, как halts устроена внутри. Простая она или сложная, перебирает ли она варианты, обучена ли на миллионе программ — упрямец строится по ней одной и тот же. Стоит запомнить и то, чего теорема не говорит: она не утверждает, что про остановку конкретной программы ничего нельзя узнать, — про while True: pass можно. Не бывает лишь одного способа на все программы.

Действие второе. Зеркало

В главе 7 мы разобрали, как устроен куайн: шаблон программы с одной дыркой, в которую подставляется запись самого шаблона. Тем же приёмом программа может получить свой текст для любого дела, печать — лишь одно из них. Вот упрямец, которого можно запустить. Он спрашивает Оракула, что сам напечатает, — «да» или «нет», — и печатает обратное. Это та же ловушка, только вместо «остановлюсь ли я» — «что я скажу», так её проще проверить. Сначала мы отдадим его честному Оракулу из cs.oracle, который отвечает, запуская программу, а потом двум Оракулам, которые отвечают не думая.

Первые четыре строки вывода — сам упрямец, программа конечная и вполне обычная. Честный Оракул, чтобы узнать, что она напечатает, запускает её — и она снова спрашивает Оракула, и тот снова запускает её. Он никогда не ответит, и мы останавливаем его на четвёртом круге. Два «нечестных» Оракула отвечают сразу и оба ошибаются: упрямец говорит наоборот. Последняя строка подтверждает, что Оракулу упрямец передал свой текст буква в букву.

То, что сработало здесь, работает всегда. В 1938 году Стивен Клини доказал теорему о рекурсии: какое бы преобразование текстов программ мы ни взяли, найдётся программа, которая получает собственный текст и применяет к нему это преобразование. Напечатать себя — частный случай, преобразование «ничего не менять»; это куайн из главы 0. Спросить о себе Оракула и сделать наоборот — другой.

Действие третье. Диагональ

Все программы можно выписать в один бесконечный список: программы — конечные тексты, а конечные тексты можно упорядочить сначала по длине, а при равной длине — по алфавиту. Пусть $P_0, P_1, P_2, \ldots$ — этот список. Входы тоже пронумеруем: $0, 1, 2, \ldots$ Составим бесконечную таблицу: в клетке $(i, j)$ — останавливается ли программа $P_i$ на входе $j$. Если бы Оракул существовал, он умел бы заполнить любую клетку.

Теперь пройдём по диагонали — по клеткам $(0, 0), (1, 1), (2, 2), \ldots$ — и построим программу $D$, которая на входе $n$ делает наоборот по сравнению с клеткой $(n, n)$: если $P_n$ на входе $n$ останавливается, $D$ зацикливается, и наоборот. $D$ отличается от $P_0$ на входе 0, от $P_1$ — на входе 1, от каждой $P_n$ — на входе $n$. Значит, $D$ нет в списке. Но в списке все программы, а $D$ — программа: если Оракул есть, её можно написать, вызывая его на каждой диагональной клетке. Противоречие то же, что с упрямцем, — упрямец и есть $D$, спрошенная о себе.

Тем же приёмом Георг Кантор в 1891 году доказал, что действительных чисел больше, чем натуральных, — день третий в «Бесконечностях» «Царицы наук». И у него есть следствие покрепче самой теоремы. Программ — счётное множество: их можно перенумеровать. А задач с ответом «да» или «нет» о натуральных числах столько же, сколько подмножеств натурального ряда: каждая задача — это множество чисел, на которых ответ «да». Таких множеств, по той же диагонали Кантора, несчётно много. Программ на всех не хватит, и неразрешимые задачи составляют подавляющее большинство. Странно скорее другое: задачи, которые нам попадаются, так часто оказываются разрешимыми.

Действие четвёртое. Скромные вопросы

Это рассуждение называют сведением. Задача A сводится к задаче B, если любой вход A можно механически переделать во вход B с тем же ответом. Тогда решатель B решал бы и A. И обратно: если A неразрешима, то неразрешима и B — иначе решатель B решил бы A. Сведение — главный инструмент этой части курса: в следующей главе им же будут доказывать, что задача трудна.

Схема сведения к вопросу о «привете» — три строки:

Слово «молча» здесь не украшение. Если P сама печатает «привет» и потом зависает, Q не должна выдать её ответ за свой. И если P падает с ошибкой — это тоже остановка, и Q должна дожить до своей последней строки. Довести схему до работающего кода — задача «Сведение» в конце главы. Та же схема годится и для любого другого «скромного» вопроса.

Ни один из вопросов конструктора не говорит об остановке. «Будет ли деление на ноль», «обратится ли программа к сети», «вернёт ли 42», «удалит ли файл» — это вопросы о том, что программа делает. И для каждого сработала одна и та же схема: выполнить P молча, а потом сделать то, о чём спрашивают. В 1951 году Генри Гордон Райс заметил, что так можно поступить с любым подобным вопросом, и доказал это в диссертации; напечатана теорема в 1953 году.

Теорема Райса — это короткий ответ на множество практических вопросов. Идеального антивируса нет: «программа заражает другие файлы» — свойство поведения. Фред Коэн, один из первых исследователей компьютерных вирусов, ставил опыты уже в 1983 году, когда учился у Леонарда Адлемана (это его «A» в названии RSA из главы 60). В статье 1984 года (журнальная версия вышла в 1987-м) Коэн доказал, что никакой алгоритм не обнаруживает все возможные вирусы. Идеальной проверки типов нет: «программа никогда не сложит строку с числом» — свойство поведения, и поэтому mypy в главе 53 отвергал невиновные программы. По той же причине ни один линтер не найдёт весь мёртвый код, ни один оптимизатор не построит лучшую программу, а тесты не докажут, что ошибок нет.

И всё же анализаторы существуют и приносят пользу: каждый нарушает одно из трёх обещаний Оракула — отвечать всегда, отвечать верно, отвечать про любую программу, — а какое, выбирает сам. Одни отвечают не всегда: «не знаю» — тоже ответ, так работают проверки, которые просят подсказать им типы. Другие ошибаются, но в безопасную сторону: проверка типов отвергает сомнительное (лучше ложная тревога, чем пропущенная ошибка), а антивирус по сигнатурам, наоборот, пропускает незнакомое, зато почти не поднимает ложных тревог. Частый случай — лимит времени, стратегия Оракула из прелюдии, только признанная открыто: когда время вышло, честный инструмент говорит «не знаю», а торопливый рискует ошибиться. А третьи меняют язык: если программы пишутся на языке, неполном по Тьюрингу, как конфигурации Starlark из прошлой главы, теорема Райса на них не распространяется, и многое становится разрешимым.

Действие пятое. Бобры

Мы встречали их на шестом уровне игры в прошлой главе. В 1962 году Тибор Радо задал вопрос: сколько шагов может сделать машина Тьюринга с $n$ состояниями и символами 0 и 1, запущенная на пустой ленте, — при условии, что она в конце концов остановится? Максимум называют числом усердного бобра $BB(n)$, а машину, которая его достигает, — чемпионом.

Машины ниже записаны так, как их пишут участники проекта bbchallenge: строка на состояние, в строке по правилу на каждый символ — что записать, куда сдвинуться и куда перейти; Z — остановка. Модуль cs.turing из прошлой главы читает эту запись функцией standard.

Шесть шагов, двадцать один, сто семь. Чемпион с пятью состояниями за миллион шагов не остановился и не собирается: ему нужно 47 176 870 шагов. В песочнице курса это заняло бы секунды, а на загруженном сервере могло бы не уложиться в лимит ячейки. Браузеру хватает доли секунды: в гонке ниже чемпиона можно досчитать до конца.

С пятью состояниями пришлось так трудно, а с шестью, возможно, не выйдет никогда, потому что бобры — та же проблема остановки в другой одежде.

То же рассуждение показывает, что $BB(n)$ растёт быстрее любой вычислимой функции: если бы для какой-то вычислимой $f$ было $BB(n) \le f(n)$ при всех $n$, то $f$ заменила бы $BB$ в доказательстве. Цифры это подтверждают. Для шести состояний известно, что $BB(6)$ не меньше числа $2 \uparrow\uparrow\uparrow 5$ — это башня из двоек, высота которой равна башне из двоек высотой 65 536. И есть машина с 745 состояниями, которая останавливается, только если противоречива ZFC — система аксиом, на которой стоит почти вся математика. Если ZFC непротиворечива, то в ней невозможно доказать, что эта машина не останавливается, а значит, и узнать в ней значение $BB(745)$. Здесь проблема остановки встречается с теоремой Гёделя из Кёнигсберга.

Действие шестое. Коллатц

В конце июня 2024 года, когда доказательство для пяти состояний было уже готово, участник bbchallenge mxdys сообщил о машине с шестью состояниями, поведение которой выглядело случайным, а вскоре участник под ником Racheline понял, что она делает. Машину назвали «Антигидрой». Если отбросить подробности, она выполняет вот такой процесс:

Число раз за разом умножается на полтора с отбрасыванием половинки, а счётчик получает два очка за каждое чётное значение и теряет одно за нечётное. Машина остановится, если нечётных значений когда-нибудь окажется больше, чем удвоенное число чётных, — тогда счётчик уйдёт в минус. Если чётность чисел ведёт себя как монетка, нечётных в среднем столько же, сколько чётных, счётчик растёт, и уйти в минус ему всё труднее. Скорее всего, Антигидра не остановится никогда. Но доказать это — значит решить задачу того же рода, что гипотеза Коллатца: про поведение простого арифметического правила на всех шагах сразу. Такие задачи математика решать пока не умеет, и поэтому $BB(6)$ упирается в нерешённую проблему ещё до того, как дело дойдёт до неразрешимости.

Связь Коллатца с этой главой глубже совпадения. В 1972 году Джон Конвей, автор «Жизни» из прошлой главы, рассмотрел обобщённые правила Коллатца вида «если число $n$ даёт остаток $r$ при делении на $m$, замени его на $a_r n + b_r$»; дробные коэффициенты в них подобраны так, чтобы результат оставался целым. Конвей доказал, что вопрос «дойдёт ли число до единицы» для таких правил неразрешим: на них можно запрограммировать любую машину Тьюринга. Позже он построил на этой основе язык FRACTRAN, где вся программа — список дробей. Сама гипотеза Коллатца может оказаться верной, неверной или недоказуемой; но вопрос, к которому она принадлежит, в общем виде неразрешим.

Финал. Лавка закрывается

Задачи

Три задачи. В первой вы сами становитесь упрямцем: программа должна получить свой текст без чтения файла и обмануть любого Оракула. Во второй — доводите до рабочего кода сведение из четвёртого действия, и тесты проверяют те ловушки, на которых оно ломается. В третьей — пишете симулятор бобров, достаточно быстрый, чтобы гонять миллионы шагов.

Куда дальше

Граница проведена: есть задачи, которые не решит никакая машина. Но с другой стороны границы не всё так безоблачно. Возьмите формулу из ста логических переменных, соединённых «и», «или», «не», и спросите, можно ли подобрать значения так, чтобы она стала истинной. Эта задача разрешима — проще некуда: переберите все наборы значений, их конечное число. Только этих наборов $2^{100}$, около $1{,}3 \cdot 10^{30}$, и компьютер, проверяющий миллиард наборов в секунду, переберёт их примерно за три тысячи возрастов Вселенной.

Разрешимо — ещё не значит решаемо: есть задачи, которые ждут дольше жизни Вселенной. Можно ли решить такую задачу быстро, не перебирая всё? Проверить готовый ответ легко — подставить значения в формулу. А найти? В 1956 году Курт Гёдель написал об этом письмо Джону фон Нейману, который когда-то в Кёнигсберге отвёл его в сторону после доклада. Фон Нейман тогда уже умирал, а вопрос из письма открыт до сих пор. О нём — следующая глава.