Лемма о накачке для КС-языков

Как доказать что язык НЕ является контекстно-свободным? Это похоже на задачу доказательства отсутствия: нельзя просто показать что грамматика не работает. Нужен универсальный инструмент - и это лемма о накачке.

• **Теория компиляторов**: доказательство что C не является КС (из-за scope rules) объясняет почему C компиляторы имеют отдельную фазу symbol table lookup вместо чистого parsing
• **Трансформеры и формальные языки**: работы Hahn et al. (2020), Bhattamishra et al. (2020) показывают что attention механизм теоретически превосходит КС - это частично объясняет способность GPT к синтаксическому анализу
• **Биоинформатика**: RNA структурирование (вторичная структура) описывается КС-грамматиками, третичная структура - уже за пределами КС. Лемма о накачке применялась для доказательства этих границ

Лемма о накачке: структура длинных строк

Язык $\{a^n b^n c^n | n \geq 0\}$ не является контекстно-свободным. Как это доказать? Не существует алгоритма, который проверяет три счётчика одновременно без памяти. Но это интуиция, не доказательство. Лемма о накачке даёт формальный инструмент.

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

Откуда берётся разбиение uvwxy? Из parse tree! Для длинной строки дерево разбора должно быть высоким. По лемме о пути в дереве: если высота > |V| (число нетерминалов), какой-то нетерминал повторяется на пути от корня до листьев. Это повторение и создаёт 'накачиваемый' цикл. Точно как в регулярных автоматах - повторяющееся состояние.

Лемма Огдена: более сильный инструмент

Лемма Огдена (1968) - усиление pumping lemma. Можно 'пометить' позиции в строке и гарантировать, что накачиваемые части v и x содержат хотя бы одну помеченную позицию. Это делает некоторые доказательства значительно проще - там, где pumping lemma даёт слишком свободный выбор разбиения.

Пример: язык $\{a^i b^j c^k | i = j$ или $j = k\}$. Доказать не-КС обычной леммой сложно из-за двух условий (disjunction). Огден позволяет сосредоточиться на b-позициях, которые должны участвовать в накачке, и получить противоречие с одним из условий.

Примеры не-КС языков

Три канонических языка, которые не являются КС: $\{a^n b^n c^n\}$ (три счётчика), $\{ww | w \in \Sigma^*\}$ (удвоение строки), $\{a^{n^2}\}$ (квадраты). Все они требуют одновременного отслеживания зависимостей, которые КС-грамматика не может выразить.

Связь с ML: attention mechanism в трансформерах теоретически моделирует языки класса выше КС. В 2019-2022 годах появились работы доказывающие, что одно-слойные трансформеры с одной head эквивалентны Star-Free regular languages. Multi-head attention достигает класса выше КС - это частично объясняет почему трансформеры распознают синтаксические зависимости через произвольные дистанции.

Свойства замкнутости КС-языков

КС-языки замкнуты относительно: объединения (L1 U L2), конкатенации (L1 L2), итерации Клини (L*), гомоморфизма, обращения. Не замкнуты относительно: пересечения (L1 ∩ L2), дополнения. Это принципиально важно для построения парсеров - нельзя 'пересекать' грамматики произвольно.

Практическое следствие: многие реальные языки программирования не являются контекстно-свободными. Переменные должны быть объявлены до использования - это пересечение двух условий. Решение: разделить на KS-синтаксис (парсинг) и semantic analysis (type checking, scope resolution). Rust ownership rules вообще требуют более выразительных формализмов.

Пересечение КС-языка с регулярным языком - КС. Это важно: можно использовать регулярные выражения для 'фильтрации' КС-языка без выхода за класс. Например, подмножество Python с только простыми выражениями (без циклов) остаётся КС. В компиляторах - lexer (регулярный) + parser (КС) работают совместно именно на этом основании.

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

Лемма о накачке завершает теорию КС-языков:

• Pumping Lemma для регулярных языков — Более простая версия - предшественник КС леммы
• CYK алгоритм — Parse tree структура, используемая в доказательстве леммы
• Разрешимость — Понимание границ КС ведёт к вопросам что вообще разрешимо

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

• **Pumping Lemma для CFG**: для бесконечного КС-языка любая длинная строка s=uvwxy накачивается (uv^i wx^i y in L). |vwx|<=p, |vx|>=1.
• **Источник разбиения**: повторяющийся нетерминал в parse tree (по принципу Дирихле на длинном пути). Аналог повторяющегося состояния в регулярном автомате.
• **Лемма Огдена**: усиление - позволяет 'помечать' позиции и гарантировать их попадание в накачиваемые части. Полезна для сложных дизъюнктивных условий.
• **Замкнутость**: КС замкнуты по объединению, конкатенации, Клини. НЕ замкнуты по пересечению и дополнению. Следствие: синтаксис != семантика в компиляторах.

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

• Язык {a^n b^n} - КС. {a^n b^n c^n} - не КС. Где именно проходит граница? Что определяет 'мощность' грамматики?
• Attention в трансформерах теоретически превосходит КС. Означает ли это что GPT 'понимает' синтаксис лучше традиционных парсеров?
• Языки программирования намеренно проектируются КС-парсируемыми. Какие синтаксические ограничения существуют именно из-за этого требования?

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

• fl-11-pumping-lemma — Регулярная лемма о накачке - более простой аналог для регулярных языков
• fl-22-decidability — Понимание границ КС-языков ведёт к вопросам разрешимости
• alg-22-backtracking — Доказательство через лемму о накачке - это структурированный backtracking на противнике
• fl-15-cyk — CYK и parse trees необходимы для понимания pumping lemma для CFG
• ml-02