Теория вычислимости: машина Тьюринга, лямбда-исчисление, проблема остановки

Каждый инженер рано или поздно упирается в стену, которая выглядит как баг, но багом не является. Линтер не ловит очевидную бесконечную петлю. Компилятор TypeScript падает с «Type instantiation is excessively deep». Антивирус пропускает вирус, написанный за десять минут. Тестовый прогон висит, и никто не может сказать, сломался он или просто долго считает.

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

Статья опирается на Логику и доказательства (доказательство от противного, кванторы) и на Теорию множеств — прежде всего на счётность и диагональный метод Кантора, который окажется здесь главным инструментом.

Зачем это программисту: четыре сцены

Сцена 1. Линтер, который не может. Вы просите статический анализатор доказать, что в коде нет бесконечных циклов. Он даёт ложные срабатывания на нормальном коде и молчит на плохом. Это не лень авторов: задача неразрешима, и любой реальный анализатор обязан быть либо неполным (пропускает), либо несостоятельным (врёт), либо не всегда завершающимся. Выбрать можно ровно два свойства из трёх.

Сцена 2. Система типов, которая зависла. Система типов TypeScript тьюринг-полна: на ней реализовали интерпретатор SQL и решатель судоку. Следствие — компилятор не может гарантированно завершить проверку типов, поэтому в нём стоят искусственные ограничители глубины. То же с дженериками Java: их проверка типов неразрешима (Grigore, «Java Generics are Turing Complete», https://arxiv.org/abs/1605.05274).

Сцена 3. Газ в блокчейне. Почему EVM берёт плату за каждую операцию, а не за «программу целиком»? Потому что заранее узнать, остановится ли контракт, невозможно. Единственная реализуемая защита — бюджет шагов, то есть перевод неразрешимого вопроса в разрешимый «остановится ли за N шагов».

Сцена 4. Идеальный антивирус. Задача «содержит ли файл вредоносный код» в общей постановке неразрешима (Fred Cohen, «Computer Viruses: Theory and Experiments», 1987). Отсюда сигнатуры, эвристики, песочницы и вечная гонка — не потому что инженеры не старались, а потому что точного алгоритма не существует.

Все четыре сцены про одно: есть вопросы о поведении программ, на которые не может ответить никакая программа. Чтобы это доказать, нужно строго определить, что такое «программа».

Что вообще значит «вычислимо»

До 1930-х слово «алгоритм» было неформальным: «конечный набор механических правил». Гильберт в 1928 году поставил Entscheidungsproblem — задачу разрешения: найти алгоритм, который по любой формуле логики первого порядка отвечает, выводима ли она. Чтобы доказать, что такого алгоритма нет, потребовалось сначала определить, что такое алгоритм вообще: доказать несуществование объекта нельзя, пока не сказано, что это за объект.

За пять лет появились три независимых ответа — и все оказались эквивалентны.

Три модели: машина Тьюринга (механическая: лента, головка, таблица правил), лямбда-исчисление (функциональная: всё есть функция одного аргумента) и общерекурсивные функции (арифметическая: базовые функции плюс правила комбинирования). Модели выглядят абсолютно по-разному — и определяют один и тот же класс вычислимых функций. Это совпадение и есть главный аргумент в пользу тезиса Чёрча–Тьюринга.

Машина Тьюринга: строгое определение

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

Определение. Детерминированная машина Тьюринга — семёрка M = (Q, S, G, delta, q0, q_acc, q_rej):

Q      — конечное множество состояний
G      — конечный ленточный алфавит, содержащий пустой символ _
S      — входной алфавит, подмножество G без _
delta  — функция переходов
         delta: (Q без q_acc, q_rej) × G  ->  Q × G × {L, R}
q0     — начальное состояние
q_acc  — принимающее состояние
q_rej  — отвергающее состояние, отличное от q_acc

Читать delta(q, a) = (q', b, D) надо так: «находясь в состоянии q и видя под головкой символ a, перейди в q', запиши вместо a символ b, сдвинь головку в направлении D».

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

Вычисление — последовательность конфигураций, где каждая следующая получена применением delta. Машина принимает вход, если достигла q_acc, отвергает при q_rej и зацикливается, если не достигла ни того ни другого никогда. Вот эта третья возможность — источник всех неприятностей в статье. Уберите её, и половина теории вычислимости исчезнет.

Язык машины: L(M) = { w : M принимает w }. Он разрешим (recursive, класс R), если есть машина, которая на любом входе останавливается с верным ответом да/нет, и перечислим (recursively enumerable, класс RE), если есть машина, принимающая все слова языка, а на остальных вольная отвергнуть или зациклиться. Разница между R и RE — вся суть дальнейшего.

Разбираем машину руками

Построим машину, прибавляющую единицу к двоичному числу. Алгоритм школьный: дойти до конца числа, потом идти назад, превращая 1 в 0, пока не встретим 0 (его меняем на 1 и останавливаемся) или начало числа (тогда дописываем 1).

Прогон на входе 1011 (это 11), головка стартует на левом символе:

q=right  [1]011      -> идём вправо
q=right  1[0]11
q=right  10[1]1
q=right  101[1]
q=right  1011[_]     -> конец числа, разворот
q=carry  101[1]      -> 1 становится 0, перенос дальше
q=carry  10[1]0
q=carry  1[0]00      -> 0 становится 1, перенос погашен
q=done   1100        -> 12. Готово.

Восемь шагов: O(n) на проход вправо плюс O(n) на перенос, итого O(n) времени и O(n) памяти. Обратите внимание: сложение единицы, которое процессор делает за такт, здесь стоит линейного времени. Машина Тьюринга — модель для рассуждений о возможности, а не о скорости; аккуратные оценки скорости живут в теории сложности.

Симулятор на Python

from collections import defaultdict

BLANK = "_"

class TuringMachine:
    """Одноленточная детерминированная МТ. Лента — словарь с дефолтом BLANK:
    так моделируется бесконечность в обе стороны без выделения памяти."""

    def __init__(self, delta, start, halt):
        self.delta, self.start, self.halt = delta, start, halt

    def run(self, word, max_steps=10_000):
        tape = defaultdict(lambda: BLANK)
        for i, ch in enumerate(word):
            tape[i] = ch
        head, q, steps = 0, self.start, 0
        while q != self.halt:
            if steps >= max_steps:
                # Единственный честный способ бороться с зацикливанием — бюджет шагов.
                # Ответить «зациклится» в общем случае невозможно, и это доказано ниже.
                raise TimeoutError("превышен бюджет шагов")
            if (q, tape[head]) not in self.delta:
                break                       # нет правила — застряли, считаем остановкой
            q, write, move = self.delta[(q, tape[head])]
            tape[head] = write
            head += {"L": -1, "R": 1, "N": 0}[move]
            steps += 1
        ks = [k for k, v in tape.items() if v != BLANK]
        return "".join(tape[i] for i in range(min(ks), max(ks) + 1)) if ks else "", steps


INC = {
    ("right", "0"):   ("right", "0",   "R"),
    ("right", "1"):   ("right", "1",   "R"),
    ("right", BLANK): ("carry", BLANK, "L"),
    ("carry", "1"):   ("carry", "0",   "L"),
    ("carry", "0"):   ("done",  "1",   "N"),
    ("carry", BLANK): ("done",  "1",   "N"),   # число состояло из одних единиц
}

tm = TuringMachine(INC, start="right", halt="done")
for w in ["1011", "111", "0", "10011"]:
    tape, steps = tm.run(w)
    print(f"{w} -> {tape}  ({int(w, 2)} + 1 = {int(tape, 2)}, шагов: {steps})")

# 1011 -> 1100 (11 + 1 = 12, шагов: 8)   |   111   -> 1000  (7 + 1 = 8,   шагов: 8)
# 0    -> 1    (0 + 1 = 1,  шагов: 3)    |   10011 -> 10100 (19 + 1 = 20, шагов: 9)

Обратите внимание на max_steps. Симулятор не может отличить долгое вычисление от бесконечного — и это не недоработка автора, а ровно то, что мы докажем ниже.

Робастность модели: почему одной ленты достаточно

Естественное возражение: «одна лента — слишком слабо, дайте машине массив с произвольным доступом, и она станет мощнее». Не станет. Все разумные расширения моделируются исходной моделью с полиномиальным замедлением.

Важная деталь: недетерминизм не расширяет класс вычислимого — только меняет стоимость. Именно поэтому вопрос P против NP — вопрос о ресурсах, а не о вычислимости, и он живёт в следующей статье.

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

Универсальная машина: код как данные

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

Теорема (Тьюринг, 1936). Существует универсальная машина U, такая что для любых M и w вычисление U(code(M), w) ведёт себя ровно так же, как M(w): принимает, если принимает M; отвергает, если отвергает M; зацикливается, если зацикливается M.

Это самая недооценённая теорема в информатике. Из неё следует, что не нужна отдельная машина под каждую задачу — достаточно одной, которая читает описание задачи. Это интерпретатор. Это виртуальная машина. Это операционная система, запускающая произвольные бинарники. Это eval. Идея «программа — это данные» родилась здесь, за десять лет до архитектуры фон Неймана.

Побочный, но критический эффект: раз code(M) — обычная строка, машине можно скормить её собственный код. Самоприменение M(code(M)) совершенно законно — как python interpreter.py interpreter.py. Из этой законности и вырастает противоречие. Технический фундамент под этим — теорема о параметризации (s-m-n) Клини: по коду программы двух аргументов и значению первого можно эффективно построить код программы одного аргумента. На практике это каррирование и functools.partial; в теории — то, что позволяет строить редукции механически.

Лямбда-исчисление: вычисления без машин

Чёрч зашёл с другой стороны: убрал ленту, состояния и время. Осталось три конструкции.

Терм ::= x              переменная
       | (\x. M)        абстракция — функция одного аргумента
       | (M N)          аппликация — применение функции к аргументу

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

Свободные и связанные переменные. В \x. x y переменная x связана абстракцией, y свободна:

FV(x)      = {x}
FV(\x. M)  = FV(M) без {x}
FV(M N)    = FV(M) объединить FV(N)

Три правила преобразования:

alpha:  \x. M       =   \y. M[x := y]     переименование связанной переменной
                                          (y не должна быть свободна в M)
beta:   (\x. M) N   ->  M[x := N]         собственно вычисление
eta:    \x. (M x)   =   M                 если x не свободна в M

Бета-редукция — единственный «двигатель». Подстановка M[x := N] требует осторожности: если N содержит свободную переменную с именем, связанным внутри M, её нужно предварительно переименовать. Это захват переменных — классический источник багов в макросах и компиляторах; гигиенические макросы Scheme решают ровно эту проблему.

Кодируем данные функциями

Нумералы Чёрча. Число n — это «применить функцию n раз»: 0 = \f.\x. x, 1 = \f.\x. f x, 2 = \f.\x. f (f x).

# Нумералы Чёрча прямо на лямбдах Python: никаких int внутри.
zero = lambda f: lambda x: x
succ = lambda n: lambda f: lambda x: f(n(f)(x))
add  = lambda m: lambda n: lambda f: lambda x: m(f)(n(f)(x))
mul  = lambda m: lambda n: lambda f: m(n(f))           # композиция
exp  = lambda m: lambda n: n(m)                        # n-кратное применение m
to_int = lambda n: n(lambda k: k + 1)(0)               # мост в мир Python

three, four = succ(succ(succ(zero))), succ(succ(succ(succ(zero))))
print(to_int(add(three)(four)), to_int(mul(three)(four)), to_int(exp(three)(four)))
# 7 12 81

# Булевы значения — это выбор из двух вариантов
true  = lambda a: lambda b: a
false = lambda a: lambda b: b
ifte  = lambda c: lambda a: lambda b: c(a)(b)
is_zero = lambda n: n(lambda _: false)(true)           # n раз выкинуть аргумент
print(ifte(is_zero(zero))("да")("нет"), ifte(is_zero(three))("да")("нет"))   # да нет

# Пара — функция, отдающая свои компоненты потребителю (это буквально CPS)
pair = lambda a: lambda b: lambda s: s(a)(b)
fst, snd = lambda p: p(true), lambda p: p(false)

# Предшественник — трюк Клини: тащим пару (n-1, n) и в конце берём первую компоненту
shift = lambda p: pair(snd(p))(succ(snd(p)))
pred  = lambda n: fst(n(shift)(pair(zero)(zero)))
print(to_int(pred(four)))   # 3

Кодирование пары через «функцию, принимающую потребителя» — это continuation-passing style и church encoding из функционального программирования. Тот же приём лежит в основе представления алгебраических типов данных; подробнее — в статье Теория категорий в программировании.

Рекурсия без имён: комбинатор неподвижной точки

В лямбда-исчислении функция не имеет имени, поэтому не может позвать себя по имени. Выход — комбинатор неподвижной точки Y, для которого Y f = f (Y f):

Y = \f. (\x. f (x x)) (\x. f (x x))

В языке со строгой стратегией вычисления Y расходится, поэтому используют его вариант Z с явной задержкой:

# Z-комбинатор: рекурсия из ниоткуда — без def, без имени функции.
Z = lambda f: (lambda x: f(lambda v: x(x)(v)))(lambda x: f(lambda v: x(x)(v)))

fact = Z(lambda rec: lambda n: 1 if n == 0 else n * rec(n - 1))
fib  = Z(lambda rec: lambda n: n if n < 2 else rec(n - 1) + rec(n - 2))
print(fact(10), fib(20))   # 3628800 6765

Отсюда прямая линия к практике: fix в Haskell, рекурсивные типы через Fix f, letrec в компиляторах, схемы рекурсии. И важное наблюдение: возможность выразить рекурсию через самоприменение x x — та же самая возможность, что делает проблему остановки неразрешимой. Это не совпадение, а два проявления диагонализации.

Стратегии редукции и теорема Чёрча–Россера

Теорема (Чёрч–Россер, конфлюэнтность). Если терм M редуцируется двумя разными путями к N1 и N2, то существует P, к которому редуцируются оба. Следствие: нормальная форма, если существует, единственна с точностью до alpha-переименования. Но существует она не всегда, и стратегия редукции решает, найдёте ли вы её.

Классический пример — (\x. \y. x) I Omega, где Omega = (\x. x x) (\x. x x). Нормальный порядок отбросит Omega, не глядя, и вернёт I. Аппликативный сначала попытается вычислить Omega и зависнет навсегда. Отсюда практическое правило: if, &&, || во всех строгих языках сделаны специальными формами, а не функциями — иначе они вычисляли бы обе ветки.

Var, Lam, App = (lambda n: ("var", n)), (lambda p, b: ("lam", p, b)), (lambda f, a: ("app", f, a))
_c = [0]

def free_vars(t):
    if t[0] == "var": return {t[1]}
    if t[0] == "lam": return free_vars(t[2]) - {t[1]}
    return free_vars(t[1]) | free_vars(t[2])

def subst(t, name, val):
    """M[name := val] с alpha-переименованием во избежание захвата переменных."""
    if t[0] == "var": return val if t[1] == name else t
    if t[0] == "app": return App(subst(t[1], name, val), subst(t[2], name, val))
    p, b = t[1], t[2]
    if p == name: return t                       # переменная перекрыта — подставлять некуда
    if p in free_vars(val):                      # опасность захвата -> переименуем связанную
        _c[0] += 1; p2 = f"{p}#{_c[0]}"; b = subst(b, p, Var(p2)); p = p2
    return Lam(p, subst(b, name, val))

def normalize(t, fuel=None):
    """Нормальный порядок: самый левый внешний редекс первым. fuel — бюджет бета-шагов,
    без него функция не завершилась бы на термах вроде omega."""
    fuel = fuel or [10_000]
    while t[0] == "app":
        if fuel[0] <= 0: raise TimeoutError("бюджет редукций исчерпан")
        f = normalize(t[1], fuel)
        if f[0] != "lam": return App(f, t[2])
        fuel[0] -= 1
        t = subst(f[2], f[1], t[2])              # бета-шаг
    return Lam(t[1], normalize(t[2], fuel)) if t[0] == "lam" else t

def show(t):
    if t[0] == "var": return t[1]
    return f"(\\{t[1]}. {show(t[2])})" if t[0] == "lam" else f"({show(t[1])} {show(t[2])})"

I = Lam("x", Var("x"))
K = Lam("x", Lam("y", Var("x")))
S = Lam("x", Lam("y", Lam("z", App(App(Var("x"), Var("z")), App(Var("y"), Var("z"))))))
omega = App(Lam("x", App(Var("x"), Var("x"))), Lam("x", App(Var("x"), Var("x"))))

print(show(normalize(App(App(S, K), K))))              # (\z. z) — знаменитое SKK = I
print(show(normalize(App(App(K, I), omega), [200])))   # (\x. x) — нормальный порядок отбросил omega
# normalize(omega) -> TimeoutError: нормальной формы не существует

Комбинаторов S и K достаточно, чтобы выразить любой замкнутый лямбда-терм вообще без переменных. На этом стоит комбинаторная логика Шейнфинкеля и Карри и техника bracket abstraction из ранних реализаций Haskell.

Третий взгляд и тезис Чёрча–Тьюринга

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

def ackermann(m, n):
    """Тотальная (всегда завершается), но не примитивно рекурсивная.
    ackermann(4, 2) — число из 19 729 знаков."""
    if m == 0: return n + 1
    if n == 0: return ackermann(m - 1, 1)
    return ackermann(m - 1, ackermann(m, n - 1))

print(ackermann(2, 3), ackermann(3, 3), ackermann(3, 5))   # 9 61 253

Добавляем мю-оператор — «наименьший y, при котором f(x, y) = 0», то есть неограниченный поиск, while без гарантии выхода. Получаем частично рекурсивные функции, и они в точности совпадают с вычислимыми по Тьюрингу. Именно while без гарантии выхода превращает всегда-завершающуюся модель в тьюринг-полную — и одновременно делает остановку неразрешимой. Такова цена.

Тезис Чёрча–Тьюринга. Всякая функция, вычислимая алгоритмом в интуитивном смысле, вычислима машиной Тьюринга.

Что важно понимать про тезис:

• Это не теорема. Он связывает формальное понятие с неформальным и потому недоказуем в принципе — его можно только опровергнуть, предъявив «интуитивно алгоритмический» процесс вне модели. За 90 лет не предъявили.
• Он не про эффективность. Расширенный (физический) тезис — «всё физически вычислимое вычислимо с полиномиальными накладными расходами» — гораздо более спорен: алгоритм Шора для факторизации считается свидетельством против него.
• Он не запрещает гипотетические модели вроде машин с оракулом, а утверждает лишь, что физически реализуемого способа их построить нет.

Проблема остановки

Теперь всё готово. Формулируем задачу:

HALT = { пара (code(M), w) : машина M останавливается на входе w }

Теорема (Тьюринг, 1936). HALT неразрешима: не существует машины, которая на любой такой паре останавливается и правильно отвечает да/нет.

Доказательство

Предположим противное: существует всегда останавливающаяся машина H, для которой H(code(M), w) принимает, когда M останавливается на w, и отвергает, когда M зацикливается. Построим из неё машину D (от diagonal), принимающую один аргумент — описание машины:

D(code(M)):
    если H(code(M), code(M)) = ПРИНЯТЬ:   войти в бесконечный цикл
    иначе:                                остановиться

D — совершенно законная программа: она вызывает H (по предположению существующую) и делает ветвление. Теперь запустим D на её собственном коде:

• Если D(code(D)) останавливается, то H вернула ПРИНЯТЬ, значит по своему коду D уходит в бесконечный цикл — то есть не останавливается. Противоречие.
• Если D(code(D)) не останавливается, то H вернула ОТВЕРГНУТЬ, значит по своему коду D останавливается. Снова противоречие.

Оба варианта невозможны, а третьего нет. Единственное недоказанное допущение — существование H. Значит H не существует.

# Тот же аргумент на Python. Код НЕ запускается: halts не существует —
# именно поэтому его нельзя написать, а не потому, что автор поленился.

def halts(source: str, arg: str) -> bool:
    """Гипотетический анализатор: True <=> программа source завершается на arg."""
    ...

def D(source: str):
    if halts(source, source):
        while True: pass       # сказали «остановится» — не останавливаемся
    return "стоп"              # сказали «зациклится» — останавливаемся

# Теперь halts(D_source, D_source): что бы ни вернуло, оно неправо.
# True  -> D зацикливается   -> ответ был ложью
# False -> D останавливается -> ответ был ложью

Почему это тот же аргумент, что у Кантора

Схема ровно та же, что в доказательстве несчётности вещественных чисел (см. Теорию множеств). Строим таблицу: строки — все программы (их счётное число, ведь программа есть конечная строка), столбцы — те же программы в роли входов. В клетке (i, j) — останавливается ли Pi на коде Pj. Берём диагональ и инвертируем её. Полученная строка отличается от каждой строки таблицы хотя бы в одной клетке — значит её в таблице нет. Но она задаётся программой, а все программы в таблице есть. Противоречие.

Тот же приём порождает несчётность R, теоремы Гёделя о неполноте, парадокс Рассела и теорему Тарского о невыразимости истины. Это одна идея в пяти костюмах: самоприменение плюс отрицание.

Почему таймаут не решает проблему

Частое возражение: «просто запустим и подождём». Запустив программу и увидев остановку за 10 секунд, вы узнали ответ «да». Не увидев остановки — вы не узнали ничего: программа может завершиться на 11-й секунде или через миллион лет. Задача «остановится ли за N шагов» разрешима тривиально (симулируем N шагов), но это другая задача. Разрыв между ними чудовищен: пятисостоянийная машина Тьюринга может работать 47 176 870 шагов и всё-таки остановиться. Правильная формулировка того, что даёт таймаут: HALT полуразрешима.

Разрешимость, полуразрешимость и дополнение

Три класса: R (разрешимые) — машина всегда останавливается с верным ответом; RE (перечислимые) — на «да» машина отвечает «да», на «нет» может зациклиться; co-RE — наоборот, отвечаем на «нет», а на «да» можем зациклиться.

Теорема Поста. R = RE ∩ co-RE. Если и задача, и её дополнение полуразрешимы, задача разрешима.

HALT лежит в RE: симулируем M(w) и говорим «да», как только она встала. HALT не лежит в co-RE — иначе по теореме Поста она была бы разрешима. То есть не-остановку принципиально нельзя даже подтвердить перебором.

def enumerate_halting(programs, inputs, simulate):
    """Полуразрешающая процедура — dovetailing («переплетение»).
    Ключевой приём: не запускать одно вычисление до упора, а вести все параллельно.
    Каждая останавливающаяся пара рано или поздно будет выдана;
    ни одна незавершающаяся пара не блокирует остальные."""
    n = 0
    while True:
        n += 1
        for i in range(n):                     # первые n программ
            for j in range(n):                 # первые n входов
                if simulate(programs[i], inputs[j], steps=n):
                    yield (i, j, n)            # остановилась не более чем за n шагов

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

Отдельно стоит задача соответствий Поста (PCP): даны пары строк-«домино», нужно выложить последовательность так, чтобы верхняя строка совпала с нижней. Постановка выглядит как головоломка из детского журнала, а задача неразрешима — и служит удобным источником редукций, в том числе для доказательства неразрешимости эквивалентности КС-грамматик.

Сводимость и теорема Райса

Доказывать неразрешимость каждый раз диагонализацией мучительно. Стандартный приём — сведение.

Определение. A сводится по Карпу (many-one) к B, запись A <=m B, если существует вычислимая тотальная функция f, такая что x принадлежит A тогда и только тогда, когда f(x) принадлежит B.

Смысл: решив B, мы решили бы и A. Отсюда контрапозиция, которой мы и пользуемся: если A неразрешима и A <=m B, то B неразрешима.

Пример: докажем, что задача «печатает ли программа строку hello» неразрешима. Сводим к ней HALT: по паре (M, w) строим программу

def build(M, w):
    """Возвращает исходник новой программы. Работает всегда и быстро —
    это тотальная вычислимая функция, что и требуется для сведения."""
    return f"""
simulate({M!r}, {w!r})     # если M на w зациклится — до print мы не дойдём никогда
print("hello")
"""

Построенная программа печатает hello тогда и только тогда, когда M останавливается на w. Значит анализатор «печатает ли hello» дал бы решение HALT. Такого анализатора нет. Обобщение приёма — одна из самых полезных теорем для практикующего инженера.

Теорема Райса (1953). Пусть P — любое нетривиальное семантическое свойство программ. Тогда задача «обладает ли данная программа свойством P» неразрешима.

Расшифровка условий. Семантическое — свойство зависит только от вычисляемой функции (от поведения), а не от текста программы: «завершается на всех входах» семантическое, а «в исходнике меньше 100 строк» синтаксическое и прекрасно разрешимое. Нетривиальное — свойством обладают не все программы и не ни одной.

Следствия, которые стоит держать в голове на каждом код-ревью:

Отсюда фундаментальное правило проектирования любого статического анализатора: из трёх свойств — состоятельность, полнота, завершаемость — можно выбрать любые два. Реальные инструменты честно выбирают. Borrow checker в Rust состоятелен и завершается, но неполон: отвергает корректные программы, которые приходится писать через unsafe или Rc<RefCell<T>>. Большинство линтеров завершаются и «полны на практике», но несостоятельны — молчат на реальных багах. Coq, Agda и Lean состоятельны и завершаются, но неполны: требуют, чтобы вы сами доказали завершаемость рекурсии структурным убыванием аргумента.

Есть и уточнение — теорема Райса–Шапиро, описывающая, какие семантические свойства хотя бы полуразрешимы: только те, что наблюдаемы на конечном куске поведения. Это ровно та причина, по которой мониторинг и трассировка находят проблемы, а статический анализ — нет.

Что это меняет в инженерной практике

Инженерных ответов на неразрешимость всего четыре, и все они видны в промышленных инструментах.

Огрубить анализ. Неразрешимость касается точных ответов на всех программах. Согласившись на приблизительный ответ («точно нет» либо «может быть»), задачу можно решить. Это абстрактная интерпретация Кузо: заменяем конкретные значения абстрактными (знак, интервал, множество типов), теряем точность, получаем завершаемость. Так работают Infer от Meta, Astrée (верифицировавший ПО Airbus A380) и escape-анализ в JVM.

Сузить язык. Отказаться от тьюринг-полноты там, где она не нужна. eBPF-верификатор в ядре Linux требует, чтобы программа доказуемо завершалась — иначе ядро зависнет (https://docs.kernel.org/bpf/verifier.html); циклы там долго были запрещены вовсе, теперь допускаются только ограниченные. Dhall специально спроектирован как не-тьюринг-полный язык конфигураций: конфиг обязан вычисляться. Starlark в Bazel — то же самое. Это осознанный размен выразительности на предсказуемость.

Переложить доказательство на человека. Coq и Agda требуют, чтобы каждая рекурсия убывала по структурному аргументу; когда автоматика не справляется, вы предъявляете фундированный порядок вручную, а Dafny и Why3 просят явные decreases. Машина не решает проблему остановки — она проверяет предъявленное вами доказательство, а проверка доказательства разрешима, в отличие от его поиска.

Ограничить ресурс. Самое частое решение и, как мы видели, единственное универсальное: газ в EVM, statement_timeout в PostgreSQL, лимит бэктрекинга в regex-движках (без него катастрофический бэктрекинг превращается в ReDoS), максимальная глубина инстанцирования шаблонов в C++ (-ftemplate-depth, по умолчанию 900).

Полезно помнить и обратное: тьюринг-полнота возникает случайно и почти всегда некстати. Тьюринг-полны шаблоны C++, типы TypeScript, дженерики Java, sendmail.cf, MediaWiki-шаблоны, Magic: The Gathering и формулы Excel с LAMBDA. Каждый раз это означает, что анализ подсистемы неразрешим, а инструменты вокруг неё обречены на эвристики.

Колмогоровская сложность и Busy Beaver

Ещё два лица той же невычислимости. Колмогоровская сложность K(x) строки x — длина кратчайшей программы (в фиксированном языке), печатающей x; она измеряет, сколько в строке настоящей информации, а сколько избыточности. У строки абабабабабабабабабаб сложность мала («напечатать ‘аб’ 10 раз»), у двадцати случайных символов — порядка самой длины строки.

Теорема. K невычислима. Набросок доказательства — парадокс Берри: предположим, K вычислима, и напишем программу, перебирающую строки и печатающую первую со сложностью больше 10^6. Эта программа коротка — скажем, 5000 бит. Но печатает она строку, для которой по построению нужно больше миллиона бит. Противоречие.

Практические следствия: идеального компрессора не существует (счётный аргумент: любой компрессор без потерь, сжимающий хоть какие-то файлы, обязан увеличивать размер других — отсюда специализация под классы данных); случайность определяется через несжимаемость — строка случайна, если K(x) близко к длине x, что связывает вычислимость с теорией вероятностей; минимальная длина описания (MDL) в машинном обучении — инженерная реализация той же идеи, а регуляризация есть приближение невычислимого K.

Функция Busy Beaver. BB(n) — максимальное число шагов, которое может сделать останавливающаяся машина Тьюринга с n состояниями и двумя символами (Радо, 1962). Она невычислима и растёт быстрее любой вычислимой функции:

BB(1) = 1
BB(2) = 6
BB(3) = 21
BB(4) = 107
BB(5) = 47 176 870        (доказано коллаборацией bbchallenge, 2024)
BB(6) — известные нижние оценки уже не выражаются в обычной степенной записи

Вот почему BB — идеальный аргумент против «просто подождём»: чтобы отличить зацикливание от долгой работы у пятисостоянийной машины, нужно ждать 47 миллионов шагов, а у шестисостоянийной — дольше, чем существует Вселенная. Причём знать BB(n) в общем случае невозможно: вычислимая BB дала бы решение проблемы остановки (симулировать BB(n) шагов и, если машина не встала, ответить «зациклится»).

from collections import defaultdict
from itertools import product

def busy_beaver_2(max_steps=50):
    """Перебор всех МТ с 2 состояниями: 6^4 = 1296 машин, мгновенно.
    Для n = 5 таких машин около 16.7 миллиарда — на их разбор ушли годы работы сообщества."""
    states = ["A", "B"]
    cells = [(q, s) for q in states for s in (0, 1)]              # 4 клетки таблицы переходов
    options = list(product([0, 1], ["L", "R"], states + ["H"]))   # что писать, куда идти, куда перейти
    best, winner = -1, None
    for combo in product(options, repeat=4):
        delta = dict(zip(cells, combo))
        tape, head, q, steps = defaultdict(int), 0, "A", 0
        while q != "H" and steps < max_steps:   # max_steps здесь не оптимизация, а необходимость
            w, mv, q = delta[(q, tape[head])]
            tape[head] = w
            head += 1 if mv == "R" else -1
            steps += 1
        if q == "H" and sum(tape.values()) > best:   # засчитываем только остановившиеся
            best, winner = sum(tape.values()), delta
    return best, winner

print("BB(2): максимум единиц на ленте =", busy_beaver_2()[0])   # 4

Заметьте структуру кода: без max_steps перебор зависнет на первой же незавершающейся машине, а выбрать «правильный» max_steps мы можем только потому, что BB(2) уже известна. Для больших n этот аргумент рассыпается — в этом и состоит вся сложность проекта bbchallenge (https://bbchallenge.org/).

Оракулы и степени неразрешимости

А если дать машине «волшебную коробку», решающую проблему остановки? Такая машина с оракулом действительно решит HALT — но у неё появится своя проблема остановки, неразрешимая уже для неё. Процесс повторяется бесконечно, порождая иерархию тьюринговых степеней и арифметическую иерархию: Sigma_1 — это RE («существует свидетель»), Pi_1 — это co-RE, выше лежат «пуст ли язык M» и «эквивалентны ли M1 и M2».

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

Типичные заблуждения

«Проблема остановки неразрешима только для машины Тьюринга, а реальные компьютеры конечны». Формально верно и практически бессмысленно. Конечный автомат с 8 ГБ памяти имеет 2^(8 * 2^33) состояний; «алгоритм» проверки — обнаружить повтор конфигурации — потребует больше памяти, чем атомов во Вселенной. Разрешимость без осуществимости пуста. Родственное заблуждение — «достаточно проверить программу на всех входах»: входов бесконечно много даже для функции от одной строки, а для конкретного входа проверка упирается ровно в проблему остановки.

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

«Неразрешимость означает, что задача безнадёжна». Наоборот: неразрешимость касается точного ответа на всех входах, а на практике почти всегда достаточно правильного ответа на программах, которые люди действительно пишут. Terminator от Microsoft Research доказывал завершаемость реальных драйверов Windows; SPARK верифицирует авионику. Неразрешимость запрещает универсальный инструмент, а не полезный.

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

«Гёдель и Тьюринг — про разные вещи». Это два ракурса одной теоремы. Из неразрешимости HALT теоремы Гёделя о неполноте выводятся почти немедленно: если бы всякое истинное утверждение вида «M не останавливается на w» было доказуемо, перечисление доказательств давало бы разрешающую процедуру. Подробнее — в статье Логика и доказательства.

Мини-итог

• Вычислимость — свойство функции, а не устройства. Три несвязанные формализации дали один и тот же класс; тезис Чёрча–Тьюринга фиксирует это как рабочее определение алгоритма.
• Машина Тьюринга проста намеренно. Все расширения — многоленточность, недетерминизм, произвольный доступ, квантовость — не расширяют класс вычислимого, а лишь меняют цену.
• Универсальная машина — исток идеи «код как данные». Интерпретаторы, ВМ, eval и самоприменение растут отсюда; из самоприменения растёт и неразрешимость.
• Лямбда-исчисление показывает, что достаточно функций. Чёрч–Россер гарантирует единственность нормальной формы, но не её существование, поэтому стратегия редукции — вопрос семантики, а не оптимизации.
• Проблема остановки неразрешима, но полуразрешима. «Да» подтверждается симуляцией, «нет» — никогда. Таймаут не решает задачу, а заменяет её другой, разрешимой.
• Теорема Райса делает это правилом, а не исключением. Любое нетривиальное свойство поведения неразрешимо, поэтому у статического анализатора выбор: состоятельность, полнота, завершаемость — любые два.
• Инженерных ответов четыре: огрубить анализ, сузить язык, потребовать доказательство от человека, ограничить ресурс.

Источники

• Alan M. Turing, «On Computable Numbers, with an Application to the Entscheidungsproblem», 1936 — оригинал, читается на удивление легко: https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
• Michael Sipser, «Introduction to the Theory of Computation», 3rd ed. — лучший учебник для входа; главы 3–5 покрывают всю эту статью.
• John Hopcroft, Rajeev Motwani, Jeffrey Ullman, «Introduction to Automata Theory, Languages, and Computation» — классика, много про связь с грамматиками.
• Hartley Rogers, «Theory of Recursive Functions and Effective Computability» — справочник по теории рекурсии: теоремы Райса, s-m-n, степени неразрешимости.
• Henk Barendregt, «The Lambda Calculus: Its Syntax and Semantics»; краткий обзор — https://plato.stanford.edu/entries/lambda-calculus/
• Raúl Rojas, «A Tutorial Introduction to the Lambda Calculus»: https://arxiv.org/abs/1503.09060
• H. G. Rice, «Classes of Recursively Enumerable Sets and Their Decision Problems», 1953: https://www.ams.org/journals/tran/1953-074-02/S0002-9947-1953-0053041-6/
• Fred Cohen, «Computer Viruses: Theory and Experiments», 1987: https://web.eecs.umich.edu/~aprakash/eecs588/handouts/cohen-viruses.html
• Radu Grigore, «Java Generics are Turing Complete», POPL 2017: https://arxiv.org/abs/1605.05274
• Patrick Cousot, Radhia Cousot, «Abstract Interpretation», POPL 1977: https://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml
• Ming Li, Paul Vitányi, «An Introduction to Kolmogorov Complexity and Its Applications».
• Scott Aaronson, «Why Philosophers Should Care About Computational Complexity»: https://arxiv.org/abs/1108.1791
• Проект bbchallenge — доказательство BB(5) = 47 176 870: https://bbchallenge.org/story
• Документация верификатора eBPF в ядре Linux: https://docs.kernel.org/bpf/verifier.html
• Stanford Encyclopedia of Philosophy, «The Church–Turing Thesis»: https://plato.stanford.edu/entries/church-turing/

Что дальше

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

Следующая статья меняет вопрос с «возможно ли» на «сколько это стоит»: классы P и NP, PSPACE, полиномиальные редукции (мы уже потренировались на сводимости здесь), NP-полнота и теорема Кука–Левина, а также практический вывод — что делать, когда ваша задача оказалась NP-трудной.

Теория сложности: классы P, NP, PSPACE, редукции и полнота