Сведения и теорема Райса: о поведении программ нельзя узнать почти ничего

Если ты проведёшь сведение проблемы останова к другой задаче и не перепутаешь направление, сформулируешь теорему Райса и объяснишь, почему анализатор кода обязан либо пропускать ошибки, либо выдавать ложные тревоги, - листай до «Теперь сам».

Как думаешь, можно ли узнать, удаляет ли программа файлы

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

Ответь себе до чтения: проще ли этот вопрос, чем проблема останова? Не проще. Возьмём любую программу P, запустим её взаперти - так, чтобы сама она ничего удалить не могла, - а после её завершения вызовем удаление. Новая программа удаляет файлы тогда и только тогда, когда P доходит до конца, то есть останавливается. Точная проверка «удаляет ли» ответила бы и на вопрос «останавливается ли», а на него ответа нет. И так почти с любым вопросом о том, что программа делает.

На что это похоже

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

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

Механизм: сведение и его направление

Сведение задачи A к задаче B - алгоритм, который любой вход x задачи A превращает во вход f(x) задачи B так, что ответы совпадают: на x ответ «да» тогда и только тогда, когда на f(x) ответ «да». Сам алгоритм превращения обязан всегда останавливаться.

Если A сводится к B, то B не легче A:

B разрешима    →  A разрешима:  превратить x в f(x) и спросить решателя B
A неразрешима  →  B неразрешима:  иначе по строке выше решалась бы и A

Направление. Чтобы доказать, что новая задача B неразрешима, к ней сводят известную неразрешимую: из решателя B собирают решатель проблемы останова. Свести в обратную сторону - B к проблеме останова - значит показать лишь, что B не труднее неразрешимой задачи, а это верно и для самых простых задач.

Теорема Райса. Назовём свойство программ свойством поведения, если оно зависит только от того, что программа делает со входами - какие принимает, что выдаёт, - а не от её текста. Свойство нетривиально, если хотя бы одна программа им обладает и хотя бы одна не обладает. Теорема: всякое нетривиальное свойство поведения неразрешимо.

свойство поведения, неразрешимо    свойство текста, разрешимо
принимает ли пустую строку         длиннее ли текст ста строк
возвращает ли когда-нибудь ноль    встречается ли в тексте слово while
вычисляет ли ту же функцию,        совпадает ли текст с эталоном
что эталон                         посимвольно
останавливается ли на всех входах  есть ли в тексте вызов функции
                                   с таким именем

Правый столбец проверяется чтением текста. Левый - нет: два разных текста могут вести себя одинаково, а почти одинаковые тексты - по-разному.

Идея доказательства та же, что в примере с удалением файлов. Договоримся, что у программы, которая не останавливается ни на одном входе, свойства нет; если оно у неё есть, те же рассуждения проводят для противоположного свойства - разрешить свойство и разрешить его отрицание одно и то же умение, ответ достаточно перевернуть. Берём программу Q, у которой свойство есть. По паре P, x строим программу: «сначала выполнить P на x, потом вести себя как Q». Если P останавливается, новая программа ведёт себя как Q; если нет - зависает на любом входе, то есть ведёт себя как программа, у которой по договорённости свойства нет. Решатель свойства отличил бы одно от другого.

Правило

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

Разбор: три вопроса и три сведения

Каждый раз дана пара P, x, и по ней строится текст новой программы. Строит его обычная программа, которая просто склеивает строки и поэтому всегда останавливается. Слова «выполнить P на x» ниже означают: выполнить взаперти - вложенной универсальной машиной из прошлой главы, которая отбрасывает всё, что P печатает и пытается сделать снаружи, - иначе P могла бы сама напечатать нужное слово и зациклиться. Значок ⇔ в блоках читается «тогда и только тогда, когда».

Напечатает ли программа слово готово?

построенная программа:
    выполнить P на x      если P не остановится, до следующей строки
    print("готово")       дело не дойдёт
P останавливается на x   ⇔   построенная программа печатает «готово»

Выполнится ли когда-нибудь строка с пометкой? Это вопрос о недостижимом коде. Под теорему Райса он не подпадает - это свойство хода выполнения, а не ответов программы, - но прямое сведение работает и здесь.

построенная программа:
    выполнить P на x
    y = 0                     # пометка
P останавливается на x   ⇔   помеченная строка достижима

Одинаково ли ведут себя две программы?

первая программа:                        вторая программа:
    выполнить P на x                         print("готово")
    print("готово")
P останавливается на x   ⇔   программы ведут себя одинаково

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

Заметь, чего сведение не требует: запускать P. Строится только текст. Запуск происходил бы внутри воображаемого решателя, и это уже его забота.

Разбор: анализатор, который ошибается в одну сторону

Точного ответа нет, но можно отвечать с запасом. Задача: в программе из присваиваний найти деления, где делитель может оказаться нулём, при любом целом входе x. Анализатор не вычисляет значения, а следит за знаками: для каждой переменной хранит строку из возможных знаков - -, 0, +; "-0+" значит «любой». Вычитание он считает как сложение с числом противоположного знака, а умножение переменной на саму себя - отдельной веткой. Сумма положительных положительна, квадрат не отрицателен, а разность двух положительных может быть любой.

Команда - список «куда, левый операнд, операция, правый операнд». Функция analiz возвращает номера команд, где делитель может быть нулём. Функция na_dele проверяет это по-настоящему для x от −30 до 30.

def znak_summy(a, b):
    if a == "0":
        return b
    if b == "0":
        return a
    if a == b:
        return a
    return "-0+"

def znak_proizvedeniya(a, b):
    if a == "0" or b == "0":
        return "0"
    if a == b:
        return "+"
    return "-"

def znaki(operand, sreda):
    if operand in sreda:
        return sreda[operand]
    if operand < 0:
        return "-"
    if operand == 0:
        return "0"
    return "+"

def analiz(programma):
    sreda = {"x": "-0+"}
    zamechaniya = []
    for nomer in range(len(programma)):
        komanda = programma[nomer]
        levye = znaki(komanda[1], sreda)
        pravye = znaki(komanda[3], sreda)
        if komanda[2] == "/" and "0" in pravye:
            zamechaniya.append(nomer + 1)
        vozmozhnye = ""
        for a in levye:
            for b in pravye:
                if komanda[2] == "+":
                    itog = znak_summy(a, b)
                elif komanda[2] == "-":
                    itog = znak_summy(a, znak_proizvedeniya(b, "-"))
                elif komanda[2] == "/":
                    itog = "-0+"
                elif komanda[1] == komanda[3]:
                    itog = znak_proizvedeniya(a, a)
                else:
                    itog = znak_proizvedeniya(a, b)
                vozmozhnye = vozmozhnye + itog
        sobrano = ""
        for z in "-0+":
            if z in vozmozhnye:
                sobrano = sobrano + z
        sreda[komanda[0]] = sobrano
    return zamechaniya

def na_dele(programma):
    plohie = []
    for x in range(-30, 31):
        sreda = {"x": x}
        for komanda in programma:
            a = komanda[1]
            if a in sreda:
                a = sreda[a]
            b = komanda[3]
            if b in sreda:
                b = sreda[b]
            if komanda[2] == "+":
                sreda[komanda[0]] = a + b
            elif komanda[2] == "-":
                sreda[komanda[0]] = a - b
            elif komanda[2] == "*":
                sreda[komanda[0]] = a * b
            elif b == 0:
                plohie.append(x)
                break
            else:
                sreda[komanda[0]] = a // b
    return plohie

pervaya = [["y", "x", "*", "x"], ["z", "y", "+", 1],
           ["r", 100, "/", "z"]]
vtoraya = [["y", "x", "*", "x"], ["r", 100, "/", "y"]]
tretya = [["y", "x", "*", "x"], ["z", "y", "-", 4], ["r", 100, "/", "z"]]
chetvyortaya = [["y", "x", "*", "x"], ["z", "y", "+", 2],
                ["w", "z", "-", 1], ["r", 100, "/", "w"]]
for programma in [pervaya, vtoraya, tretya, chetvyortaya]:
    print(analiz(programma), na_dele(programma))

[] []
[2] [0]
[3] [-2, 2]
[4] []

В каждой строке - замечания анализатора и значения x, при которых деление на ноль случилось на деле.

Первая программа делит на x² + 1. Анализатор вывел: квадрат - 0 или +, плюс единица - +, ноль невозможен; замечаний нет, и это верно. Вторая делит на x²: замечание к команде 2, и действительно, при x = 0 программа падает. Третья делит на x² − 4: замечание есть, падение при x = ±2.

Четвёртая делит на x² + 2 − 1. Это x² + 1, ноль невозможен, и проверка на деле ничего не нашла. Но анализатор видит разность двух положительных величин, знает о ней только знаки и честно говорит: «может быть ноль». Ложная тревога.

Анализатор надёжен: если он промолчал, деления на ноль нет ни при каком x - не только при проверенных шестидесяти одном. И он не полон: ругается и на некоторые правильные программы. Для произвольных программ - с циклами и ветвлениями - обойти это нельзя: к вопросу «делит ли программа на ноль» проблема останова сводится тем же приёмом, что в первом разборе, и точного анализатора нет. Можно уточнять модель - хранить не знаки, а отрезки, - ложных тревог станет меньше, но до нуля они не дойдут.

Что ломается без этого

Сведение в обратную сторону. «Моя задача сводится к проблеме останова, значит неразрешима» - ошибка: к ней сводится и вопрос «чётно ли число»: достаточно построить программу, которая на чётном останавливается, а на нечётном зацикливается. Сводить нужно от известной трудной задачи к своей.

Теорему Райса применяют к тексту. Число строк, наличие ключевого слова, соответствие правилам оформления - разрешимы и проверяются точно; этим заняты линтеры, программы проверки текста по правилам.

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

Ложные тревоги считают дефектом инструмента. У надёжного анализатора они неизбежны; дефект - когда их больше, чем нужно.

Зачем это в работе

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

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

Обнаружение вредоносных программ. Точного определителя «делает ли программа вредное» нет по той же теореме. Остаются сигнатуры - свойства текста, - наблюдение за запущенной программой и эвристики; каждое средство обходится, и это не временное состояние отрасли.

Теперь сам

1. Нужно доказать, что задача B неразрешима. Что к чему сводить?
2. Какие из свойств подпадают под теорему Райса: «программа короче килобайта», «программа на входе 5 возвращает 7», «программа ни на одном входе не останавливается»?
3. Сведи проблему останова к вопросу «возвращает ли программа число 42 хотя бы на одном входе».
4. Анализатор знаков получил команды y = x * x, z = y + 3, w = z - 3, r = 1 / w. Что он скажет и прав ли он?
5. Инструмент обещает для любой программы за конечное время ответить, есть ли в ней утечка памяти, - без пропусков и без ложных срабатываний. Что не так?