Алгоритмическая сложность фрагментов исчисления Ламбека

• Автор: Саватеев, Юрий Вячеславович
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2009
• Место защиты: Москва
• Количество страниц: 75 с. : ил.

Оглавление
Введение
1 Исчисление Ламбека L
1.1 Аксиомы и правила исчисления Ламбека
1.2 Фрагменты исчисления Ламбека
1.3 Грамматики на основе исчисления Ламбека
1.4 Структурно эквивалентые секвенции
2 Построение сетей доказательства
2.1 Представление секвенций
2.2 Критерий выводимости
3 Левосторонний фрагмент исчисления Ламбека
3.1 Сведение задачи SAT к задаче выводимости для L(-, )
3.2 Доказательство корректности сведения
4 Фрагмент исчисления Ламбека без умножения
4.1 Сведение задачи SAT к задаче выводимости для L(, /)
4.2 Доказательство корректности сведения
5 Фрагмент исчисления Ламбека с одним делением
5.1 Критерий выводимости
5.2 Алгоритм распознавания принадлежности
Литература

Введение
Общая характеристика работы
Актуальность темы.
Диссертация посвящена исследованию алгоритмической сложности фрагментов исчисления Ламбека.
Исчисление Ламбека Ь было введено в [5]. Оно активно используется в качестве основы для создания категориальных грамматик, описывающих синтаксические структуры естественных языков (см. например [9] и [Ю]). Категориальные грамматики имеют ряд преимуществ перед другими способами, такими как контекстно-свободные грамматики, ввиду лексикализации — вся необходимая информация хранится в лексиконе, поэтому нет необходимости использовать всю имеющуюся информацию — достаточно только той, что относится к данному случаю. Также это позволяет параллельно с анализом синтаксической структуры вести семантический анализ, используя, например, грамматику Монтегю.
Класс языков, порождаемых категориальными грамматиками, основанными на исчислении Ламбека, в точности совпадает с классом контекстно-свободных языков (см. [13]). Исчисление Ламбека также тесно связано с линейной логикой Жирара (см. [3]) — оно эквивалентно интуиционистскому некоммутативному фрагменту мультипликативной линейной логики.
В исчислении Ламбека используются синтаксические типы, построенные из примитивных с помощью трех бинарных связок — умножения, левого деления и правого деления. Естественно рассматривать

фрагменты исчисления Ламбека с ограниченным набором связок. В настоящей работе будут рассмотрены так называемый левосторонний фрагмент L(-,), фрагмент без умножения L(,/), который является особенно важным для лингвистических приложений (большинство грамматик, описывающих естественные языки, основаны именно на этом фрагменте), и фрагмент исчисления Ламбека с одним делением L(). Также рассматриваются их варианты — фрагменты исчисления Ламбека с разрешенными пустыми антецедентами L*(-, ), L*(, /), и L*().
В категориальных грамматиках синтаксический разбор предложения сводится к поиску вывода в исчислении, лежащем в их основе. Поэтому вопрос об алгоритмической сложности задачи распознавания выводимости особенно важен для лингвистических приложений, так как напрямую связан с эффективностью работы ситаксических анализаторов, основанных на категориальных грамматиках.
Для неассоциативного варианта исчисления Ламбека было показано, что задача распознавания выводимости может быть решена за полиномиальное время (см. [4], для фрагмента неассоциативного исчисления без умножения это было доказано раньше — в [1]). Для самого исчисления Ламбека (где умножение является ассоциативным), а также для его варианта L*, разрешающего пустые антецеденты, была доказана NP-лолнота задачи распознавания выводимости (см. [12]).
Мы докажем, что классическая NP-полная задача SAT (о выполнимости булевых формул в конъюнктивной нормальной форме) за полиномиальное время может быть сведена к задачам распознавания выводимости в L(-, ), L(, /), L*(-, ) и L*(, /), и тем самым покажем, что задача распознавания выводимости для этих фрагментов NP-полна. Все конструкции и доказательства, которые мы используем при рассмотрении L(-,) и L*(-,), могут быть явно переписаны для правостороннего фрагмента L(-,/). Таким образом задача распознавания выводимости для L(-, /) и L*(-, /) также является NP-полной.

Глава
Левосторонний фрагмент исчисления Ламбека
В левостороннем фрагменте исчисления Ламбека L(-,) для создания сложных типов используются только две операции — и •. Соответственно из правил остаются (—» ), ( —»), (—» •), и (• —>). Полное исчисление Ламбека является консервативным расширением левостороннего фрагмента. Аналогично можно рассматривать исчисление L*(-,). Как и в полном исчислении правило сечения является устранимым.
Мы докажем, что задачи распознавания выводимости в L(-,) и L*(-,) являются NP-полными. Для этого мы сведем к ним известную NP-полную задачу выполнимости булевых формул в конъюнктивной нормальной форме SAT.
Предложенные конструкции можно явно переписать для правостороннего фрагмента. Поэтому будет выполнена следующая теорема.
Теорема 2. Задача распознавания выводим,ости секвенций в L(-,), L(-, /), L*(-,) и L*(-, /) NP-полна.
Следствие 1. Задача распознавания принадлежности данного слова языку, порожденномоу данной грамматикой, основанной на L(-, ), L(-,/); L*(-,) или L*(•,/), NP-полна.