Проблема останова: вопрос, на который не отвечает ни одна программа

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

Как думаешь, можно ли находить все бесконечные циклы

Редактор кода подчёркивает while True без выхода. Компилятор предупреждает о недостижимом коде после бесконечного цикла. Частные случаи ловятся хорошо.

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

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

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

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

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

Механизм: программа, которая делает наоборот

Проблема останова - язык всех пар «текст программы P, вход x», в которых P на входе x останавливается.

Язык распознаваем: выполняем P на x, как это делает универсальная машина, и если P остановилась - приняв или отвергнув, всё равно, - принимаем.

Теорема. Проблема останова неразрешима.

Предположим обратное: существует программа ostanavlivaetsya(P, x), которая на любых P и x останавливается сама и возвращает True, если P останавливается на x, и False, если нет. Тогда можно написать ещё одну программу. Ниже набросок, а не запускаемый код: P - текст программы, справа от команд стоят пояснения.

def naoborot(P):
    if ostanavlivaetsya(P, P):    спросить: остановится ли P
                                  на собственном тексте?
        работать вечно            да - тогда зациклиться
    else:
        остановиться              нет - тогда остановиться

Это законная программа: она вызывает ostanavlivaetsya, которая по предположению всегда возвращает ответ, и потом делает одно из двух. Теперь запустим naoborot на её собственном тексте.

naoborot(naoborot) остановилась
    →  значит, ostanavlivaetsya(naoborot, naoborot) вернула False
    →  значит, naoborot на naoborot не останавливается - противоречие

naoborot(naoborot) не остановилась
    →  значит, ostanavlivaetsya(naoborot, naoborot) вернула True
    →  значит, naoborot на naoborot останавливается - противоречие

Оба случая невозможны. Ошибка может быть только в предположении: программы ostanavlivaetsya нет.

Где диагональ. Выпишем все программы в список: P₀, P₁, P₂, … Построим таблицу: в клетке (i, j) - останавливается ли Pᵢ на тексте Pⱼ. Программа naoborot устроена так, чтобы на тексте Pᵢ вести себя противоположно клетке (i, i). Значит, её строка отличается от строки каждой Pᵢ на диагонали. Но naoborot - программа и сама должна стоять в списке под каким-то номером k; в клетке (k, k) ей пришлось бы отличаться от самой себя.

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

Правило

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

Разбор: диагональ на пяти настоящих машинах

Возьмём пять машин в формате прошлой главы и построим таблицу: принимает ли машина i двоичный код машины j. Программа моделирования и кодирование те же, только исход ? означает «за пятьсот шагов ответа нет». Последняя строка вывода - диагональный язык: «да» там, где машина не приняла собственный код. В механизме клетка отвечала на вопрос «останавливается ли», здесь - «принимает ли»: язык соседний, довод тот же.

def universalnaya(opisanie, vhod, predel):
    tabl = {}
    for pravilo in opisanie.split(" "):
        tabl[pravilo[0] + pravilo[1]] = [pravilo[2], pravilo[3],
                                         pravilo[4]]
    lenta = list(vhod)
    if len(lenta) == 0:
        lenta.append("_")
    sostoyanie = "0"
    poz = 0
    shagov = 0
    while sostoyanie != "+":
        klyuch = sostoyanie + lenta[poz]
        if klyuch not in tabl:
            return "нет"
        if shagov == predel:
            return "?"
        hod = tabl[klyuch]
        lenta[poz] = hod[0]
        if hod[1] == "R":
            poz = poz + 1
            if poz == len(lenta):
                lenta.append("_")
        elif poz > 0:
            poz = poz - 1
        sostoyanie = hod[2]
        shagov = shagov + 1
    return "да"

def v_bity(tekst):
    alfavit = "012_+RL "
    bity = ""
    for simvol in tekst:
        nomer = 0
        while alfavit[nomer] != simvol:
            nomer = nomer + 1
        bity = (bity + str(nomer // 4) + str(nomer // 2 % 2)
                + str(nomer % 2))
    return bity

mashiny = ["010R0 001R+ 0_1R+", "000R0 011R1 100R1 110R0 0__R+",
           "000R0 011R1 100R1 110R0 1__R+"]
mashiny = mashiny + ["000R0 011R1 111R1 100R0 1__R+",
                     "000R0 011R1 100R1 110R0 0__R+ 1__R2 2__R2"]
kody = []
for m in mashiny:
    kody.append(v_bity(m))
diagonal = []
for i in range(len(mashiny)):
    ryad = []
    for j in range(len(mashiny)):
        ryad.append(universalnaya(mashiny[i], kody[j], 500))
    print(i, ryad)
    if ryad[i] == "да":
        diagonal.append("нет")
    else:
        diagonal.append("да")
print("D", diagonal)

0 ['да', 'да', 'да', 'да', 'да']
1 ['нет', 'да', 'нет', 'да', 'да']
2 ['да', 'нет', 'да', 'нет', 'нет']
3 ['нет', 'нет', 'нет', 'нет', 'нет']
4 ['?', 'да', '?', 'да', 'да']
D ['нет', 'нет', 'нет', 'да', 'нет']

Машины по порядку: прибавление единицы (принимает всё), чётное число единиц, нечётное число единиц, последний знак - единица, и пятая - принимает при чётном числе единиц, а при нечётном уходит вправо навсегда. На диагонали стоит да, да, да, нет, да; строка D - противоположная.

Строка D не совпадает ни с одной из пяти: от строки 0 она отличается в столбце 0, от строки 1 - в столбце 1, и так до конца. Если бы таблица содержала все машины, язык D - «машина не принимает собственный код» - не распознавался бы ни одной из них, по той же причине.

Обрати внимание на клетки с вопросом. Машина из строки 4 на кодах машин 0 и 2 не остановилась за пятьсот шагов, и программа честно не знает, что туда писать. На диагональ вопросы здесь не попали - иначе программа записала бы в строку D «да» наугад, считая, что машина свой код не примет. Чтобы заполнить всю бесконечную таблицу и вычислить D, нужна была бы именно та программа, которой нет: умеющая сказать «не остановится».

Разбор: при ограниченной памяти вопрос решается

Дадим машине ленту фиксированной длины: упёршись в край, головка остаётся на месте. Теперь конфигураций конечное число: состояние, положение головки, содержимое ленты. Если конфигурация повторилась, дальше всё пойдёт по кругу - машина не остановится никогда. Функция s_pamyatyu запоминает все встреченные конфигурации и возвращает вердикт, число шагов и число разных конфигураций, в которых машина побывала до остановки (последняя, где она остановилась, не в счёт); лента должна быть непустой. Вердиктов три: приняла и отвергла - машина остановилась, не остановится - конфигурация повторилась.

def s_pamyatyu(opisanie, vhod):
    tabl = {}
    for pravilo in opisanie.split(" "):
        tabl[pravilo[0] + pravilo[1]] = [pravilo[2], pravilo[3],
                                         pravilo[4]]
    lenta = list(vhod)
    sostoyanie = "0"
    poz = 0
    videli = set()
    shagov = 0
    while sostoyanie != "+":
        konfiguraciya = sostoyanie + str(poz) + ":" + "".join(lenta)
        if konfiguraciya in videli:
            return ["не остановится", shagov, len(videli)]
        videli.add(konfiguraciya)
        klyuch = sostoyanie + lenta[poz]
        if klyuch not in tabl:
            return ["отвергла", shagov, len(videli)]
        hod = tabl[klyuch]
        lenta[poz] = hod[0]
        if hod[1] == "R" and poz < len(lenta) - 1:
            poz = poz + 1
        elif hod[1] == "L" and poz > 0:
            poz = poz - 1
        sostoyanie = hod[2]
        shagov = shagov + 1
    return ["приняла", shagov, len(videli)]

tuda_syuda = "000R0 011R0 0__L1 100L1 111L1 1__R0"
schyotchik = "0__R1 110R1 101L2 1__R+ 200L2 211L2 2__R1"
print(s_pamyatyu(tuda_syuda, "_0110_"))
for n in [2, 4, 6, 8]:
    print(n, s_pamyatyu(schyotchik, "_" + "0" * n + "_"))
print(s_pamyatyu("000R0 0__R0 011R+", "0000"))

['не остановится', 11, 11]
2 ['приняла', 12, 12]
4 ['приняла', 58, 58]
6 ['приняла', 248, 248]
8 ['приняла', 1014, 1014]
['не остановится', 4, 4]

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

Вторая машина - двоичный счётчик: прибавляет единицу к числу на ленте (младший разряд слева), пока оно не переполнится. Она останавливается, но через 12, 58, 248 и 1014 шагов при 2, 4, 6 и 8 разрядах: каждые два разряда увеличивают работу примерно вчетверо. Ни одна конфигурация не повторилась, и запомнить пришлось все.

Отсюда видно, где проходит граница. На ленте из m клеток конфигураций конечное число: число состояний, умноженное на m положений головки и на sᵐ содержимых ленты, где s - число символов (у машин урока их три). Машина либо остановится, либо повторится. Вопрос разрешим, хотя цена экспоненциальна. Третья машина из вывода идёт вправо, пока не встретит единицу; на ленте её нет. На конечной ленте она упирается в край и повторяется. На бесконечной её конфигурации все разные: головка каждый раз на новой клетке. Повтора не будет, и способ, работавший минуту назад, не срабатывает никогда. Способ, на котором держалось решение, исчезает вместе с ограничением на память; неразрешимость проблемы останова - свойство машин с неограниченной лентой.

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

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

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

Неразрешимое путают с долгим. Задача, которую решают миллиард лет, разрешима. Здесь алгоритма нет вообще, сколько бы времени ни дали.

«Мой компьютер конечен, ко мне это не относится». Формально да: у него конечное число конфигураций. Но при килобайте памяти их не меньше 2⁸⁰⁰⁰, и «дождаться повтора» не план. Программы пишут так, будто память не ограничена, поэтому и рассуждать о них приходится в этой модели.

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

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

Языки, в которых всё завершается. Системы формальных доказательств разрешают рекурсию только по уменьшающемуся аргументу; языки проверяемых фильтров запрещают неограниченные циклы. Завершаемость там гарантирована устройством языка, а не анализом.

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

Теперь сам

1. Что делает программа naoborot, если ostanavlivaetsya(P, P) вернула True?
2. Почему в доказательстве naoborot запускают именно на её собственном тексте?
3. Проблема останова распознаваема. Как выглядит распознающая программа?
4. На диагонали таблицы стоит да, нет, нет, да. Какова строка диагонального языка?
5. У машины лента из десяти клеток, два символа и три состояния. Оцени сверху число её конфигураций.