Формальные языки

Контекстно-зависимые языки и LBA

Rust borrow checker отвергает ваш код. Парсер его принял - синтаксис правильный. Но семантика нарушена: время жизни ссылки не согласовано. Это КЗ-проверка поверх КС-разбора. Всё, что 'знает' контекст - типы, области видимости, времена жизни - живёт в типе 1 иерархии Хомского.

  • **Rust borrow checker:** проверка времён жизни ссылок - семантический анализ КЗ-класса. Полиморфизм времён жизни ('a: 'b) задаёт ограничения согласования, не выразимые КС-грамматикой
  • **C++ шаблоны:** рекурсивные инстанциации шаблонов образуют систему вычислений, эквивалентную LBA. Компилятор GCC тратит O(n²) времени на разбор сложных template-иерархий именно из-за КЗ-природы
  • **Согласование в естественных языках:** немецкие придаточные предложения, перекрёстные зависимости в швейцарском немецком - формально КЗ-структуры. NLP-парсеры используют CYK и Earley алгоритмы, работающие за O(n³)
  • **XML Schema (XSD):** валидация XML с XSD - КЗ-задача. Согласование типов по всему документу требует прохода с памятью O(n), реализуя LBA

Контекстно-зависимые грамматики

Напомним иерархию Хомского: тип 3 (регулярные), тип 2 (КС), тип 1 (КЗ), тип 0 (рекурсивно перечислимые). Тип 1 - **контекстно-зависимые (КЗ) грамматики**: правило αAβ → αγβ означает замену A на γ только в контексте α...β. Порождение не сокращает строку: |αγβ| ≥ |αAβ|. КЗ-языки закрыты относительно пересечения - КС-языки нет.

**КЗ-грамматика (тип 1):** все правила имеют вид αAβ → αγβ, где A ∈ N (нетерминал), α, β ∈ (N∪T)*, γ ∈ (N∪T)⁺. Ключевое: γ непустое - строки не сокращаются. Классический пример КЗ-языка, не являющегося КС: L = {a^n b^n c^n : n ≥ 1}. КС не может выразить тройное согласование.

КЗ-языки замечательны тем, что они **разрешимы** - в отличие от языков типа 0. Это следует из монотонности правил: вывод не сокращает строку, значит цепочки вывода ограничены и конечны. Разрешающий алгоритм: перечислить все выводы длины ≤ |w| и проверить принадлежность.

Почему язык {a^n b^n c^n} является КЗ, но не КС?

Линейно ограниченный автомат (LBA)

**Линейно ограниченный автомат (LBA)** - недетерминированная МТ, которой запрещено выходить за пределы входной строки на ленте. Головка движется только в диапазоне [1, |w|]. Это существенное ограничение: LBA работает в памяти O(n), тогда как общая МТ имеет неограниченную ленту.

**Теорема (Мясник-Ландвебер-Хеневич, 1963):** язык L является КЗ тогда и только тогда, когда L распознаётся LBA. Это аналог теоремы для КС (КС ↔ стековый автомат). КЗ ↔ LBA. Детерминированный LBA распознаёт строго меньший класс языков - открытый вопрос, равен ли он недетерминированному LBA.

Чем LBA отличается от общей МТ?

Свойства КЗ-языков

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

СвойствоРег. (тип 3)КС (тип 2)КЗ (тип 1)РП (тип 0)
ОбъединениеДаДаДаДа
ПересечениеДаНет!ДаДа
ДополнениеДаНет!Да (открыто?)Нет
КонкатенацияДаДаДаДа
РазрешимостьДаДаДаНет
РаспознаваемостьДаДаДаДа

Открытый вопрос (нерешённый с 1963): равен ли детерминированный LBA недетерминированному? Т.е. Det(LBA) = NonDet(LBA)? Это аналог вопроса P vs NP для пространственной сложности. Если решится - даст новые инструменты для понимания P vs PSPACE.

Два КЗ-языка L1 и L2. Является ли L1 ∩ L2 КЗ-языком?

КЗ-языки на практике

Где встречаются КЗ-языки в реальной разработке? **Согласование в естественных языках** (subject-verb-object agreement) - это тип 1 по Хомскому. Немецкий с вложенными придаточными предложениями формально требует КЗ-грамматику. **Шаблоны C++** с рекурсивными инстанциациями вычислительно эквивалентны LBA.

Интересный факт: большинство ограничений в языках программирования, которые **не проверяются парсером**, а проверяются в фазе семантического анализа - это потенциально КЗ-свойства. Правила области видимости, согласование типов, линейная система типов Rust - всё это выходит за рамки КС и требует отдельных алгоритмов проверки.

Компиляторы разбирают язык программирования одной КС-грамматикой

Компиляторы разбирают синтаксис КС-грамматикой (парсер), но семантические ограничения (типы, области видимости, согласование) проверяют отдельными алгоритмами, часто реализующими КЗ-проверки

Rust borrow checker, TypeScript type inference, Java generics erasure - всё это алгоритмы семантического анализа поверх КС-дерева разбора. Они реализуют проверки КЗ-класса (или выше), что объясняет почему эти фазы компиляции сложнее и медленнее самого парсинга.

Почему согласование XML-тегов не проверяется КС-парсером?

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

  • **КЗ-грамматика (тип 1):** правила αAβ → αγβ - замена нетерминала в контексте. Строки не сокращаются. Классический язык: {a^n b^n c^n}
  • **LBA:** МТ, ограниченная лентой длиной O(|w|). КЗ ↔ LBA - теорема (аналог КС ↔ стековый автомат)
  • **КЗ замкнуты:** по объединению, пересечению, конкатенации - в отличие от КС. КЗ-языки разрешимы
  • **На практике:** семантические проверки компиляторов (типы, времена жизни, области видимости) реализуют КЗ-проверки поверх КС-парсера

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

КЗ-языки - промежуточный уровень между КС и полными МТ:

  • Иерархия Хомского — КЗ (тип 1) - между КС (тип 2) и рекурсивно перечислимыми (тип 0)
  • Пространственная сложность — NLSPACE соответствует классу КЗ-языков через сохранение пространства O(n)
  • Машина Тьюринга — LBA - МТ с ограничением на размер ленты O(n); общая МТ без ограничений

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

  • Rust borrow checker отвергает правильный код ('false positives'). Является ли это принципиальным ограничением или недостатком реализации?
  • Детерминированный LBA = недетерминированный LBA? Чем этот вопрос похож на P vs NP и в чём отличие?
  • Зачем XML-парсеры используют отдельную фазу для проверки согласования тегов, а не включают это в КС-грамматику?

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

  • comp-02
Контекстно-зависимые языки и LBA

0

1

Войти