Post Correspondence Problem

1946 год. Эмиль Пост публикует задачу о плитках домино. Набор карточек, у каждой - верхняя и нижняя строки. Можно ли разложить последовательность карточек (с повторениями) так, чтобы верхние строки слились в одно слово, и нижние слились в то же слово? Звучит как пазл для детей. Оказалось - это один из самых мощных инструментов доказательства неразрешимости в теоретической информатике. Через него рушится надежда на автоматическую проверку неоднозначности грамматик, на которых строится синтаксический анализ в каждом компиляторе.

• Парсеры компиляторов (GCC, LLVM, rustc) используют однозначные КС-грамматики - не потому что так удобнее, а потому что проверка неоднозначности КС-грамматики неразрешима через PCP
• Yacc/Bison/ANTLR требуют от программиста вручную разрешать конфликты shift-reduce - автоматической проверки нет и быть не может
• Верификация синтаксических спецификаций языков (JSON Schema, XML DTD) ограничена теми же математическими запретами
• Формальные методы верификации протоколов (TLA+, Alloy) обходят PCP, ограничивая выразительность или требуя конечных моделей

Формулировка задачи Поста

1946 год. Bell Labs. Эмиль Пост, польско-американский математик, которому уже принадлежат нормальные системы Поста и машины Поста, публикует задачу, которую называет "correspondance problem". Простая как детская игра - и неразрешимая.

Дан набор из $k$ карточек-домино. Каждая карточка $i$ содержит верхнюю строку $u_i$ и нижнюю строку $v_i$ над некоторым алфавитом $\Sigma$. Задача: найти последовательность индексов $i_1, i_2, \ldots, i_n$ (индексы можно повторять, порядок важен), такую что конкатенация верхних строк совпадёт с конкатенацией нижних:

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

**Формально:** PCP = $\{\langle P \rangle \mid P$ - набор пар строк, имеющий соответствие$\}$. Это язык неразрешим: нет МТ, которая принимает все экземпляры с решением и отвергает все без решения.

Важный нюанс: PCP перечислимо (recursively enumerable). Если решение есть - систематический перебор его найдёт. Не остановимся только в случае, когда решения нет. Это именно тот паттерн, что и у Halting Problem: полуразрешимость без разрешимости.

Редукция от Halting Problem

Почему PCP неразрешимо? Потому что любое вычисление машины Тьюринга можно закодировать в виде набора карточек. Если машина останавливается - набор имеет решение. Если нет - не имеет. Это редукция: $HP \leq_m PCP$.

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

Это не просто элегантная конструкция - это шаблон. Любую задачу, которую можно выразить как "существует ли вычислительная история с таким-то свойством", можно свести к PCP. Именно поэтому PCP стал таким мощным инструментом.

Полное доказательство редукции $HP \leq_m PCP$ технически сложно: нужно аккуратно закодировать все конфигурации МТ. На экзаменах часто достаточно понять схему и знать, что конструкция существует. Детали - в Sipser, Chapter 5.2.

Следствие немедленное: если бы PCP был разрешим, то был бы разрешим и HP. HP неразрешим - значит, PCP неразрешим. Цепочка рассуждений в одну строку, когда редукция построена.

Неоднозначность КС-грамматик

Самое неожиданное применение PCP - убийство надежды на автоматическую проверку грамматик. КС-грамматика неоднозначна, если одна и та же строка имеет два разных дерева вывода. Это смертельно для парсеров: если грамматика неоднозначна, компилятор не знает, как интерпретировать код.

Хочется инструмент: скормить грамматику, получить ответ "однозначна" или "нет". Такого инструмента нет и быть не может. Задача неразрешима - и доказывается это через PCP.

Каждый компилятор живёт с этим знанием. GCC, Clang, rustc - все используют только те классы грамматик, для которых однозначность гарантирована синтаксически: LR(1), LL(1), PEG. Это не произвол - это математическая необходимость.

**Что разрешимо:** пересечение двух регулярных языков пусто? Разрешимо. КС-язык пуст? Разрешимо. КС-грамматика неоднозначна? Неразрешимо. Разница - в мощности модели.

Есть разрешимые частные случаи. Грамматики в нормальной форме Гreibach однозначны по построению. ANTLR проверяет LL(*) грамматики на конфликты, которые он умеет обнаруживать. Но общий случай - закрыт. Теорема Поста 1946 это запечатала.

Ключевые идеи

• **PCP** - задача о соответствии Поста: дан набор пар строк $(u_i, v_i)$, найти последовательность индексов $i_1, i_2, \ldots, i_k$ такую что $u_{i_1} u_{i_2} \cdots u_{i_k} = v_{i_1} v_{i_2} \cdots v_{i_k}$
• **Неразрешимость PCP** доказывается редукцией от Halting Problem: для любой МТ $M$ и входа $w$ строится экземпляр PCP, имеющий решение тогда и только тогда, когда $M$ останавливается на $w$
• **Неоднозначность КС-грамматик** - прямое следствие: нет алгоритма, который по произвольной КС-грамматике определит, является ли она неоднозначной
• **Мощность инструмента** - PCP используется как промежуточное звено для десятков других доказательств неразрешимости в формальных языках и теории грамматик

Связанные темы

PCP - мост между Halting Problem и неразрешимостью в теории формальных языков

• Halting Problem — PCP доказывается редукцией от задачи остановки
• Контекстно-свободные грамматики — Неоднозначность КС-грамматик неразрешима через PCP
• Mapping Reductions — PCP - классический пример использования редукций для переноса неразрешимости

Вопросы для размышления

• Если для конкретного небольшого набора карточек решение есть - это не противоречит неразрешимости? Что именно неразрешимо в PCP?
• Компиляторы успешно парсят код годами - как они живут с тем, что неоднозначность КС-грамматик неразрешима?
• Редукция HP -> PCP идёт через кодирование вычисления МТ в виде доминошной игры. Насколько плотно такое кодирование - можно ли из PCP восстановить любое вычисление?

Связанные уроки

• comp-04 — PCP доказывается редукцией от Halting Problem
• comp-05 — Теорема Райса - предыдущий шаг в цепочке неразрешимостей
• comp-07 — Mapping reductions используют PCP как промежуточное звено
• fl-12-cfg — Неоднозначность КС-грамматик доказывается через PCP
• cplx-05 — NP-полнота и неразрешимость - два разных предела сложности
• fl-01-intro