Теорема Райса простыми словамиПочему нельзя проверить любую программу и что с этим делать

Суть: что запрещает теорема Райса

Теорема Райса говорит, что все нетривиальные смысловые свойства программ неразрешимы. Доказал её Генри Гордон Райс в диссертации 1951 года. В трёх словах этой формулировки вся теорема.

Какой бы умной ни была проверка, найдётся программа, на которой она ответит неверно.

Как это понимать на бытовом уровне. Представьте проверяющего, которому приносят любую программу и спрашивают: «Спишет ли она когда-нибудь деньги без заказа?» Проверяющий может быть сколько угодно умным, работать сколько угодно долго и знать все языки программирования. Теорема говорит, что всё равно найдётся программа, на которой он ответит неверно или не ответит вовсе. Это свойство самой задачи, и улучшение проверяющего его не снимает, как улучшение конструкции не даёт вечного двигателя.

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

Предикат: вопрос о записи или вопрос о поведении

Предикат — вопрос о программе с ответом «да» или «нет». Таких вопросов два вида, и теорема Райса касается только второго.

Код один и тот же. Разница в том, на что нужно посмотреть, чтобы ответить: на конечный текст или на бесконечное число запусков.

Почему слово «смысловое» здесь ключевое. Смысловое свойство зависит только от того, что программа делает, и не зависит от того, как она написана. Если две программы на всех входах ведут себя одинаково, у них одинаковый ответ на смысловой вопрос. Пример: одна программа считает сумму покупок циклом, другая — готовой функцией. Тексты разные, поведение одно, и на вопрос «бывает ли сумма отрицательной» у них общий ответ. А на вопрос «есть ли в коде цикл» ответы разные, потому что это вопрос о записи.

Близкая аналогия — императивный и декларативный подходы. Код записывает шаги, то есть «как», а правило о результате — утверждение, то есть «что». Теорема Райса говорит, что из шагов в общем случае нельзя механически вывести, верно ли утверждение о результате. Оговорка: на мощном декларативном языке поведение тоже не проверить по тексту. Точный ответ дают бедные записи вроде ограничения в базе: в них поведение видно из самой записи.

Доказательство на одном примере

Проверка правила для $Q$ ответила бы, остановится ли $P(w)$, а на этот вопрос не отвечает ни одна программа.

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

Возьмём любую программу $P$ со входом $w$ и соберём из неё новую программу $Q$:

Шаг $B(x)$ правило нарушает, а программа, которая работает вечно, его не нарушает. Значит, $Q$ доходит до нарушения, только если $P(w)$ когда-нибудь закончится:

Если бы существовала проверка правила для любой программы, она, получив $Q$, ответила бы и на вопрос, остановится ли $P(w)$. Но Алан Тьюринг доказал, что на этот вопрос, проблему остановки, не отвечает ни одна программа. Значит, и универсальной проверки правила нет. Правило здесь любое: вместо «деньги без заказа» можно подставить любое нетривиальное свойство поведения.

Те же шаги по порядку:

1. Берём любое нетривиальное правило о поведении. Раз оно нетривиальное, есть программа, которая его нарушает. Её часть, которая нарушает правило, и есть шаг $B$.
2. Берём любую программу $P$ и её вход $w$, про которые хотим узнать, остановится ли $P(w)$.
3. Склеиваем $Q$: сначала $P(w)$, потом $B$. Склейку делает простая механическая процедура, её можно написать за минуту.
4. Отдаём $Q$ воображаемой универсальной проверке. Её ответ «нарушает» значит «$P(w)$ остановилась», ответ «не нарушает» значит «не остановилась».
5. Получилось решение проблемы остановки, которого не бывает. Значит, не бывает и универсальной проверки.

Одна оговорка для точности. В построении считается, что программа, которая работает вечно и ничего не делает, правило не нарушает. Если для какого-то правила это не так, берут обратное правило: его проверка ничем не легче, и рассуждение повторяется слово в слово.

Откуда приём: проблема остановки и парадокс брадобрея

Теорема Райса сводит любую проверку поведения к проблеме остановки и этим наследует её неразрешимость. А проблема остановки доказывается приёмом, которому больше ста лет: вопросом о самом себе.

Спорщик спрашивает судью о себе и поступает наоборот, поэтому судья ошибается при любом ответе.

Допустим, есть судья, который про любую программу говорит, остановится ли она. Напишем программу-спорщика: она спрашивает судью о самой себе и поступает наоборот. Судья сказал «остановится» — спорщик крутится вечно; сказал «не остановится» — спорщик сразу останавливается. Судья ошибается в любом случае, значит, его не бывает.

Брадобрей бреет всех, кто не бреет себя сам. Сам он не попадает ни в одно из двух множеств.

Тот же приём в парадоксе брадобрея, наглядном варианте парадокса Рассела 1901 года. Жители делятся на множество $A$ — те, кто бреет себя сам, и множество $B$ — те, кого бреет брадобрей, и каждый попадает ровно в одно. Брадобрею места нет: в $A$ он оказывается в $B$, в $B$ — в $A$. У Рассела то же про множества: $R = {x : x \notin x}$, и $R \in R \iff R \notin R$.

Почему вопрос о самом себе так силён. Программа — это тоже текст, а значит, её можно подать на вход другой программе и даже самой себе. Как только проверяющий умеет говорить о любой программе, он обязан уметь говорить и о программе, которая спрашивает его о себе и поступает наоборот. Тогда любой его ответ оказывается неверным. Тот же ход есть в парадоксе брадобрея, в парадоксе Рассела и в теореме Гёделя о неполноте.

Что делать: три рамки, внутри которых ответ точный

Теорема запрещает проверку для любой программы. Для программ внутри рамки проверка возможна.

Теорема запрещает одно сочетание из трёх условий сразу: проверка должна работать для любой программы, на любой вопрос о поведении отвечать точно «да» или «нет». Доказательство опирается на все три: оно строит программу $Q$, которую проверка обязана принять, задаёт про неё вопрос о поведении и требует однозначный ответ. Каждый способ убирает одно условие, и доказательство перестаёт работать.

Каждый из трёх ответов точен только в своих пределах. Перебор доказывает, что правило держится в модели с 3 комнатами и 5 бронями, но не в боевой базе с тысячами броней. Поиск доказывает, что в коде нет записи в обход, но не то, что само ограничение в базе написано верно. Ответ «соблюдено» точен, но часть правок всё равно уходит человеку. Поэтому способы используют вместе: модель проверяет замысел до кода, ограничение и поиск проверяют сам код, а человек смотрит то, что осталось с меткой.

У любой проверки, которая работает внутри рамки, бывают ошибки двух видов. Полезно заранее решить, какую из них можно терпеть.

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

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

Связь с теоремой CAP: общее ядро, разные причины

Теорема CAP — известный запрет из распределённых систем. Когда данные лежат на нескольких серверах и связь между ними оборвалась, система не может одновременно отвечать на каждый запрос и показывать всем одни и те же данные. Приходится выбирать: ждать восстановления связи или отвечать по своей копии, которая могла устареть. Эрик Брюер высказал это в 2000 году, Сет Гилберт и Нэнси Линч доказали в 2002-м.

Общее ядро. В обоих запретах: пока событие не произошло, нельзя понять, случится ли оно позже или не случится никогда, сколько бы ни ждать. Сервер не знает, потеряно сообщение соседа или просто опаздывает. Проверка программы не знает, закончится программа через миллиард шагов или не закончится никогда. Пока время ожидания ничем не ограничено, у обоих ровно два выхода, и выбрать можно только один из них: ждать или ответить сейчас.

Верх схемы — развилка из двух взаимоисключающих выходов. Низ — третий путь: он меняет условие, из-за которого развилка возникла.

Как выглядят две ветки развилки в сети и в проверке программы:

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

Разные причины. Серверу в CAP не хватает сведений: даже бесконечно умный сервер не узнает, что происходит у соседа за оборванной связью. Проверке программы сведений хватает, весь код перед ней, но ответ из этого кода нельзя вычислить. Это разные виды невозможности, поэтому теорема Райса и CAP — не одно и то же.

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

Частые вопросы