Свойства замкнутости общих грамматик -- Формально верифицированные

Основная информация

• ID статьи: 2302.06420
• Название: Closure Properties of General Grammars -- Formally Verified
• Авторы: Martin Dvorak (Institute of Science and Technology Austria), Jasmin Blanchette (Ludwig-Maximilians-Universität München)
• Классификация: cs.FL (Формальные языки и теория автоматов)
• Конференция: 14-я Международная конференция по интерактивному доказательству теорем (ITP 2023)
• Ссылка на статью: https://arxiv.org/abs/2302.06420

Аннотация

В данной работе авторы формализовали общие грамматики (грамматики типа 0) с использованием помощника доказательств Lean 3. Авторы определили фундаментальные концепции правил переписывания и слов, выводимых из грамматики, и доказали замкнутость класса языков типа 0 относительно четырёх операций: объединения, обращения, конкатенации и звезды Клини. Литература в основном сосредоточена на аргументах машин Тьюринга, которые могут быть сложнее для формализации. Для звезды Клини авторы не смогли следовать литературным подходам и предложили собственную конструкцию на основе грамматик.

Исследовательский контекст и мотивация

Проблемный фон

1. Значимость теории формальных языков: Концепции формальных языков являются ядром информатики и могут быть распознаны различными формализмами, включая машины Тьюринга и формальные грамматики
2. Эквивалентность грамматик типа 0 и машин Тьюринга: Машины Тьюринга и общие грамматики характеризуют один и тот же класс рекурсивно перечислимых языков или языков типа 0
3. Ограничения существующих формализаций: Хотя существует значительный объём работ по формализации машин Тьюринга в помощниках доказательств, формализация общих грамматик остаётся относительно недостаточной

Исследовательская мотивация

1. Преимущества грамматик: Общие грамматики проще определить, чем машины Тьюринга, и некоторые доказательства свойств грамматик значительно проще, чем аналогичные доказательства для машин Тьюринга
2. Важность свойств замкнутости: Свойства замкнутости языков типа 0 являются фундаментальными результатами теории формальных языков
3. Потребность в формальной верификации: Требуются проверяемые машиной строгие доказательства для обеспечения корректности этих фундаментальных результатов

Основные вклады

1. Первая формализация общих грамматик: Полное определение фундаментальных концепций и операций грамматик типа 0 в Lean 3
2. Формальные доказательства четырёх свойств замкнутости:
   • Замкнутость относительно объединения
   • Замкнутость относительно обращения
   • Замкнутость относительно конкатенации
   • Замкнутость относительно звезды Клини
3. Инновационная конструкция звезды Клини: Поскольку в литературе отсутствует конструкция на основе грамматик, авторы разработали собственный метод
4. Переиспользуемая абстрактная структура: Разработана структура lifted_grammar для уменьшения дублирования кода и предоставления универсальных схем доказательств
5. Библиотека открытого кода на Lean объёмом ~12 500 строк: Полная формализованная реализация, доступная для сообщества

Детальное описание методологии

Структура базовых определений

Система символов

inductive symbol (T : Type) (N : Type)
| terminal : T → symbol  
| nonterminal : N → symbol

Представление правил грамматики

structure grule (T : Type) (N : Type) :=
( input_L : list (symbol T N))
( input_N : N)  
( input_R : list (symbol T N))
( output_string : list (symbol T N))

Определение грамматики

structure grammar (T : Type) :=
(nt : Type)
(initial : nt)
(rules : list (grule T nt))

Определение основных операций

Отношение трансформации грамматики

def grammar_transforms (g : grammar T) (w1 w2 : list (symbol T g.nt)) : Prop :=
∃ r : grule T g.nt,
  r ∈ g.rules ∧
  ∃ u v : list (symbol T g.nt),
    w1 = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v ∧
    w2 = u ++ r.output_string ++ v

Отношение выводимости

def grammar_derives (g : grammar T) : 
  list (symbol T g.nt) → list (symbol T g.nt) → Prop :=
relation.refl_trans_gen (grammar_transforms g)

Технические инновации

1. Абстрактная структура lifted_grammar

Для уменьшения дублирования кода авторы разработали абстрактную структуру:

• Содержит меньшую грамматику g0 и большую грамматику g
• Предоставляет функции lift_nt и sink_nt для преобразования между различными типами нетерминалов
• Обеспечивает инъективность и корректность соответствующих правил

2. Инновационная обработка операции конкатенации

Традиционная конструкция конкатенации для контекстно-свободных грамматик не работает для общих грамматик. Решение авторов:

• Создание прокси-нетерминалов для каждого терминального символа
• Полное разделение нетерминалов, используемых в g1 и g2
• Избежание проблем сопоставления строк через границы конкатенации

3. Оригинальная конструкция звезды Клини

Поскольку в литературе отсутствует конструкция на основе грамматик, авторы изобрели новый метод:

• Введение разделителя # для построения изолированных "отсеков" слов
• Использование очистителя R для прохода от начала к концу и удаления разделителей
• Новый набор правил: P* = P ∪ {Z → ZS#, Z → R#, R# → R, R# → ε} ∪ {Rt → tR | t ∈ T}

Экспериментальная установка

Среда формализации

• Помощник доказательств: Lean 3
• Математическая библиотека: mathlib
• Объём кода: Примерно 12 500 строк хорошо отформатированного кода на Lean
• Метапрограммирование: Использование метапрограммирования Lean для разработки небольших автоматизаций

Методы верификации

• Структурная индукция: Использование структурной индукции для доказательств отношения выводимости
• Анализ случаев: Исчерпывающий анализ различных случаев применения правил
• Поддержание инвариантов: Сохранение ключевых инвариантов в сложных доказательствах

Результаты экспериментов

Основные теоремы

1. Замкнутость относительно объединения: theorem T0_of_T0_u_T0 (L1 L2 : language T) : is_T0 L1 ∧ is_T0 L2 → is_T0 (L1 + L2)
2. Замкнутость относительно обращения: theorem T0_of_reverse_T0 (L : language T) : is_T0 L → is_T0 (reverse_lang L)
3. Замкнутость относительно конкатенации: theorem T0_of_T0_c_T0 (L1 L2 : language T) : is_T0 L1 ∧ is_T0 L2 → is_T0 (L1 * L2)
4. Замкнутость относительно звезды Клини: theorem T0_of_star_T0 (L : language T) : is_T0 L → is_T0 L.star

Анализ сложности доказательств

• Объединение и обращение: Относительно простые, используют стандартные конструкции
• Конкатенация: Средняя сложность, требует обработки проблем сопоставления границ
• Звезда Клини: Наиболее сложная, только лемма star_induction содержит более 3000 строк кода

Побочные результаты

• Контекстно-свободные грамматики: Доказательства могут быть переиспользованы для установления замкнутости контекстно-свободных языков
• Леммы конкатенации: theorem CF_of_CF_u_CF и подобные могут быть непосредственно применены к контекстно-свободным языкам

Связанные работы

Формализация грамматик

• Контекстно-свободные грамматики: Carlson и др. (Mizar), Minamide (Isabelle/HOL), Barthwal и Norrish (HOL4), Firsov и Uustalu (Agda), Ramos (Coq)
• Общие грамматики: Данная работа является первой полной формализацией

Другие вычислительные модели

• Конечные автоматы: Thompson и Dillies (Lean), формализация регулярных выражений
• Машины Тьюринга: Реализации в нескольких помощниках доказательств, последние работы Balbach даже доказывают теорему Кука-Левина
• λ-исчисление: Norrish (HOL4), Forster и др. (Coq)
• Частично рекурсивные функции: Norrish (HOL4), Carneiro (Lean)

Заключение и обсуждение

Основные выводы

1. Грамматики превосходят машины Тьюринга: Для доказательства свойств замкнутости грамматики могут быть удобнее, чем машины Тьюринга
2. Осуществимость формализации: Сложные результаты теории языков могут быть успешно формализованы в современных помощниках доказательств
3. Значимость абстракций: Хорошие абстракции (такие как lifted_grammar) критически важны для крупномасштабной формализации

Ограничения

1. Классы сложности: Грамматики не могут определить важные классы сложности (такие как класс P), для этого всё ещё требуются модели вроде машин Тьюринга
2. Конструктивность: Авторы не пытались сделать разработку конструктивной
3. Замкнутость относительно пересечения: Замкнутость относительно пересечения не формализована, так как авторы не знают элегантной конструкции, основанной исключительно на грамматиках

Направления будущих исследований

1. Полная иерархия Хомского: Включение контекстно-чувствительных, контекстно-свободных и регулярных грамматик в библиотеку
2. Доказательства эквивалентности: Попытка доказать эквивалентность общих грамматик и машин Тьюринга
3. Интеграция с mathlib: Связь результатов mathlib для регулярных языков с данной библиотекой

Глубокая оценка

Преимущества

1. Пионерская работа: Первая полная формализация общих грамматик, заполняющая важный пробел
2. Технические инновации: Оригинальная конструкция звезды Клини демонстрирует глубокие теоретические знания
3. Качество инженерии: 12 500 строк высокого качества кода с хорошо продуманной архитектурой
4. Теоретический вклад: Доказывает, что методы на основе грамматик в некоторых случаях превосходят подходы с машинами Тьюринга
5. Переиспользуемость: Абстракции вроде lifted_grammar обеспечивают основу для последующих работ

Недостатки

1. Ограничения выразительности: Невозможно обработать важные концепции теории сложности
2. Отсутствие конструктивности: Не рассмотрены требования конструктивной математики
3. Неполнота: Отсутствует обработка важных операций, таких как пересечение
4. Документация: Некоторые технические детали могли бы быть объяснены более подробно

Влияние

1. Теоретическое значение: Закладывает основу для машинной верификации теории формальных языков
2. Методологическая ценность: Демонстрирует лучшие практики крупномасштабных проектов формализации
3. Вклад в сообщество: Библиотека открытого кода будет способствовать связанным исследованиям
4. Образовательная ценность: Может служить отличным примером для изучения методов формализации

Области применения

1. Теоретическая информатика: Исследования теории языков и теории автоматов
2. Формальная математика: Математические исследования, требующие строгих доказательств
3. Верификация компиляторов: Гарантии корректности синтаксического анализа и обработки языков
4. Обучение: Вспомогательные материалы для курсов по формальным языкам

Библиография

Статья цитирует 26 важных работ, охватывающих:

• Классические учебники: теория синтаксического анализа Aho & Ullman, теория автоматов Hopcroft и др.
• Формализованные работы: реализации вычислительных моделей в различных помощниках доказательств
• Документация инструментов: соответствующие материалы Lean 3 и mathlib

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