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

Саватеев, Юрий Вячеславович

Алгоритмическая сложность фрагментов исчисления Ламбека тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

Саватеев, Юрий Вячеславович АВТОР

кандидата физико-математических наук УЧЕНАЯ СТЕПЕНЬ

Москва МЕСТО ЗАЩИТЫ

2009 ГОД ЗАЩИТЫ

01.01.06 КОД ВАК РФ

Диссертация по математике на тему «Алгоритмическая сложность фрагментов исчисления Ламбека»

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

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ им. М. В. ЛОМОНОСОВА

Механико-математический факультет

На правах рукописи УДК 510.662

ои-зчи—

Саватеев Юрий Вячеславович

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

Специальность 01.01.06 — математическая логика, алгебра и теория чисел

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Москва 2009 - 3 ДЕН

003486565

Работа выполнена на кафедре математической логики и теории алгоритмов Механико-математического факультета Московского государственного университета имени М. В. Ломоносова

Научный руководитель: доктор физико-математических наук,

профессор Пентус Мати Рейнович

Официальные оппоненты: доктор физико-математических наук

Лысенок Игорь Геронтьевич

кандидат физико-математических наук Кудинов Андрей Валерьевич

Ведущая организация: Институт математики имени С. Л. Соболева Сибирского отделения РАН

Защита диссертации состоится 11 декабря 2009 года в 16 часов 45 минут на заседании диссертационного совета Д.501.001.84 при Московском государственном университете имени М. В. Ломоносова по адресу: Российская Федерация, 119991, Москва, ГСП-1, Ленинские горы, д. 1, МГУ имени М. В. Ломоносова, Механико-математический факультет, аудитория 14-08.

С диссертацией можно ознакомиться в библиотеке Механико-математического факультета МГУ (Главное здание, 14 этаж).

Автореферат разослан 11 ноября 2009 года.

Ученый секретарь диссертационного совета Д.501.001.84 при МГУ, доктор физико-математических наук, профессор

А. О. Иванов

Общая характеристика работы

Актуальность темы. Диссертация посвящена исследованию алгоритмической сложности фрагментов исчисления Ламбека.

Исчисление Ламбека L было введено в 1958 году1. Оно активно используется в качестве основы для создания категориальных грамматик, описывающих синтаксические структуры естественных языков2 3. Категориальные грамматики имеют ряд преимуществ перед другими способами, такими как контекстно-свободные грамматики, ввиду лексикали-зации — вся необходимая информация хранится в лексиконе, поэтому нет необходимости использовать всю имеющуюся информацию — достаточно только той, что относится к данному случаю. Также это позволяет параллельно с анализом синтаксической структуры вести семантический анализ, используя, например, грамматику Монтегю4.

Класс языков, порождаемых категориальными грамматиками, основанными на исчислении Ламбека, в точности совпадает с классом контекстно-свободных языков5. Исчисление Ламбека также тесно связано с линейной логикой Жирара6 — оно эквивалентно интуиционистскому некоммутативному фрагменту мультипликативной линейной логики.

В исчислении Ламбека используются синтаксические типы, построенные из примитивных с помощью трех бинарных связок — умножения, левого деления и правого деления. Естественно рассматривать фрагменты исчисления Ламбека с ограниченным набором связок. В настоящей работе будут рассмотрены так называемый левосторонний фрагмент L(-, \), фрагмент без умножения L(\, /), который является особенно важным для лингвистических приложений (большинство грамматик, описывающих естественные языки, основаны именно на этом фрагменте), и фрагмент исчисления Ламбека с одним делением L(\). Также рассматриваются их варианты — фрагменты исчисления Ламбека с разрешенными пустыми антецедентами L*(-,\), L*(\,/), и L*(\).

В категориальных грамматиках синтаксический разбор предложения

1 Lainbek J. The mathematics of sentence structure // American Mathematical Monthly. — 1958. —

Vol. 65, № 3. — P. 154—170. — Русский перевод: Ламбек И. Математическое исследование структуры предложений // Математическая лингвистика: Сборник переводов / Под ред. Ю. А. Шрейдера и др. - М.: Мир, 1964. — С. 47-68.

3Moortgat M. Categorial type logic, // Handbook of Lope and Language / Editors J. van Benthem, A. ter Meulen. — Elsevier. — 1997. — P. 93—177.

'Morrill G. Type Logical Grammar: Categorial logic of Signs // Berlin: Springer. — 1994. — 328 p.

4Montague R. English as a Formal Language // Linguaggi nella societa e nella técnica. — / Editor Bruno Visentini. — Milan: Edizioni di Comuniti, 1970. — P. 189—223.

5Pentus M. Lambek grammars are context free // Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science: June 19—23, 1993. Montreal, Canada. — Los Alamitos, California: IEEE Computer Society Press, 1993. — P. 429—433.

«Girard J.-Y. Linear logic // Theoretical Computer Science. — 1987. — Vol. 50, N> 1. — P. 1—102.

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

Для неассоциативного варианта исчисления Ламбека де Гроотом было показано, что задача распознавания выводимости может быть решена за полиномиальное время7. Для фрагмента неассоциативного исчисления без умножения это было доказано ранее Аартсом и Траутвейном8. Для самого исчисления Ламбека (где умножение является ассоциативным), а также для его варианта L*, разрешающего пустые антецеденты, была доказана NP-полнота задачи распознавания выводимости?.

Мы докажем, что классическая NP-полная задача SAT (о выполнимости булевых формул в конъюнктивной нормальной форме) за полиномиальное время может быть сведена к задачам распознавания выводимости в L(-, \), L(\, /), L*(-, \) и L*(\, /), и тем самым покажем, что задача распознавания выводимости для этих фрагментов NP-полна. Все конструкции и доказательства, которые мы используем при рассмотрении L(-, \) и L*(-, \), могут быть явно переписаны для правостороннего фрагмента L(-,/). Таким образом задача распознавания выводимости для L(-, /) и L*(-, /) также является NP-полной.

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

Таким образом, теперь для всех фрагментов исчисления Ламбека, заданных ограничениями набора связок, установлены точные оценки алгоритмической сложности задачи распознавания выводимости.

7 de Groote Ph. The non-associative Lambek calculus with product in polynomial time / / Automated Reasoning with Analytic Tableaux and Related Methods / Editer N. V. Murray. — Berlin: Springer, 1999. — P. 128-139. — (Lecture Notes in Computer Science; vol. 1617).

8Aarts E., Trautwein K. Non-associative Lambek categorial grammar in polynomial time // Mathematical logic Quartérly. - 1995. — Vol. 41, № 4. — P. 476-484.

"Pentus M. Lambek calculus is NP-complete // Theoretical Computer Science. — 2006. — Vol. 357, № 1/3. - P. 186-201.

редавая его принципиальную структуру10 п. В 2005 году Пенном была предпринята попытка применить данный метод для исследования выводимости во фрагменте исчисления Ламбека без умножения, однако там не было получено никаких результатов, связанных с алгоритмической сложностью12. Еще один критерий (близкий к критерию, предложенному автором13, однако формально неверный) для этого фрагмента был предложен Леконтом в 1993 году14.

Открытый вопрос об NP-полноте задачи распознавания выводимости во фрагменте исчисления Ламбека без умножения упоминается в статьях многих математиков и лингвистов, изучающих исчисление Ламбека7 8 9 12.

Цель работы. Получение оценок алгоритмической сложности задач распознавания выводимости и распознавания принадлежности данного слова языку, порождаемому данной категориальной грамматикой, для различных фрагментов исчисления Ламбека.

Научная новизна. Результаты диссертации являются новыми, среди них:

1. Задачи распознавания выводимости в исчислении NP-полны для Ц-, \), L(\, /), L(-, /), L*(-, \), L*(\, /), L*(-, /).

2. Задачи распознавания принадлежности данного слова языку, порождаемому данной категориальной грамматикой, NP-полны для L(-, \), L(\, /), L(-, /), L*(-, \), L*(\, /), L*(-, /).

3. Задачи распознавания выводимости в исчислении разрешимы за полиномиальное время для L(\),L*(\),L(/),L*(/).

4. Задачи распознавания принадлежности данного слова языку, порождаемому данной категориальной грамматикой, разрешимы за полиномиальное время для L(\),L*(\),L(/),L*(/).

Методы исследования. В работе применяются методы теории доказательств. Основным инструментом исследования выводимости является

l0Roorda D. Resource Logics: Proof-theoretical Investigations: Ph.D. thesis. — Amsterdam, 1991. — 138 p.

11 Metayer F. Polynomial equivalence among systems LLNC, LLNC„ and LLNCo // Theoretical Computer Science. — 1999. — Vol. 227, № 1. — P. 221—229.

15Penn G. A Graph-Theoretic Approach to Polynomial-Time Recognition with the Lambek Calculus / / Electronic Notes in Theoretical Computer Science. — Elsevier. — 2005. — Vol. 53.

"Savateev Y. Product-free Lambek calculus is NP-complete // Logical Foundations of Computer Science, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3-6, 2009. Proceedings / Editors S. N. Artemov and A. Nerode. — Berlin: Springer, 2009. — P. 380-394. — (Lecture Notes in Computer Science; vol. 5407).

uLecomte A. Towards efficient parsing with proof-nets // EACL 1993,6th Conference of the European Chapter of the Association for Computational Linguistics, April 21-23,1993. — Utrecht: OTS — Research Institute for Language and Speech, Utrecht University, 1993. — P. 269—276.

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

Теоретическая и практическая ценность. Работа носит теоретический характер. Результаты, полученные в диссертационной работе, могут найти применение в математической логики и лингвистике.

Апробация диссертации. Результаты диссертации докладывались на следующих семинарах и конференциях:

• На международном семинаре "Вычислительные интерпретации доказательств" (Computational Interpretations of Proofs), Париж, Франция, 29-30 ноября 2007 года.

• На международной конференции "Логические модели доказательств и вычислений" (LMRC-2008) Москва, Россия, 5-8 мая 2008 года.

• На международной конференции "Компьютерные науки в России" (CSR-2008), Москва, Россия, 7-12 июня 2008 года.

• На семинаре "Алгоритмические вопросы алгебры и логики"под руководством академика РАН С.И. Адяна (2008, 2009).

• На международной конференции "Логические основы компьютерных наук" (LFCS-2009), Дирфилд Бич, США, 3-6 января 2009 года.

• На Европейской летней школе по логике, лингвистике и информатике (ESSLLI-2009), Бордо, Франция, 20-31 июля 2009 года.

• На научно-исследовательском семинаре кафедры математической логики и теории алгоритмов под руководством академика РАН С. И. Адяна, члена-корреспондента РАН Л. Д. Беклемишева и профессора В. А. Успенского (2009).

Публикации. Основные результаты диссертации опубликованы в работах [1]-[3].

Структура диссертации. Работа состоит из введения, 5 глав, содержащих 12 разделов, и списка литературы. Библиография содержит 17 наименований. Текст диссертации изложен на 75 страницах.

Содержание работы

В главе 1 вводятся нужные нам понятия и обозначения.

В разделе 1.1 формулируются аксиомы и правила исчисления Лам-бека.

Ассоциативное исчисление Ламбека можно построить следующим образом. Пусть задано счетное множество примитивных типов Р = {Po,Pi, ■ ■ •}• Определим множество Тр L-типов (также называемых L-термами): (1) Р С Тр; (2) если А, В € Тр, то (А/В), (А\В), (А - В) & Тр.

Примитивные типы будем обозначать строчными латинскими буквами (р, д,г,...), L-типы — заглавными латинскими буквами (А, В, С...). Заглавными греческими буквами (П, Г, Д,...) будем обозначать последовательности (возможно пустые) L-типов. Выражения вида П —► А, где П непусто, называются L-формулами или секвенциями. Конечную последовательность L-типов Ai,..., Ап условимся обозначать Ai... Ап.

Аксиомы и правила вывода в L таковы:

Ф -*■ В ТВ А -» А /ртт Л-А ГФД —¥ A (0Ui)'

НА —> В , л Ф -» А ТВ А -» С ,, \

П {В/А) К /h Т(В/А)ФА —► С

АП В , х х Ф -> А ТВ А С /\ ч

П (А\В) К ГФ(А\В)Д С U h П —» Л Ф-+ В (. \ TABA -» С , Л ПФ -+{А-В) У 'h T{A-B)A^CV h

В посылках и выводах правил стоят L-формулы, Г и Д могут быть пустыми.

Запись L I- П —> А означает, что секвенция П —► А выводима в исчислении L.

Исчисление L* отличается от L тем, что в нем разрешены пустые антецеденты, то есть выражения вида —> А, где А — некоторый тип, также считаются формулами. Правило сечения (CUT) является устранимым в обоих этих исчислениях.

В разделе 1.2 описываются интересующие нас фрагменты исчисления Ламбека.

• Левосторонний фрагмент исчисления Ламбека. В этом фрагменте для образования сложных типов используются только две операции — умножение и левое деление. Все секвенции, выводимые в этом фрагменте, не содержат знака /, поэтому правила (—» /) и (/ —>) отсутствуют в этом фрагменте.

• Фрагмент исчисления Ламбека без умножения. То же самое, только здесь отсутсвует умножение.

• Фрагмент исчисления Ламбека с одним делением. Здесь для образования сложных типов используется только одна операция — левое деление.

Так же мы рассматриваем варианты этих фрагментов, допускающие пустые антецеденты.

В разделе 1.3 показывается как строятся грамматики на основе исчисления Ламбека и какие языки они порождают.

Грамматика Ламбека это четверка (Е, Р, Я, В), где X это алфавит, Р — набор примитивных типов, Л: Е —> 2Тр — отображение, сопоставляющее каждой букве алфавита конечное множество Ь-типов, построенных из Р, В — выделенный Ь-тип. Слово хх,..., хп & Е* принадлежит языку, порождаемому данной грамматикой, если существуют А{ 6 такие, что секвенция А\... А„ —* В выводится в исчислении Ламбека.

В разделе 1.4 вводится понятие структурно эквивалентных секвенций, которое потребуется нам при доказательстве критерия выводимости.

В главе 2 вводится понятие сети доказательства.

В разделе 2.1 описывается представление секвенций исчисления Ламбека как множества начал некоторого слова и доказываем свойства этого представления. В этом же разделе вводится понятие сети доказательства и формулируются так называемые доказательные условия — свойства сетей доказательства, которые будут использоваться для определения выводимости исходной секвенции.

Пусть даны р 6 Тр, г € N и ] € 2. Тогда назовем атомом символ

. Определим множество А1 как множество всех атомов.

Определим РБ как множество всех конечных слов в алфавите А<;.

Элементы РБ будем обозначать буквами А, В, С и так далее, символом е будем обозначать пустую строку.

Определим три отображения 4 : ГЭ —► Р, : РБ N и д : РЭ —> й следующим образом:

¿(Ар|ф=р; ¿(АрЩ)=г, д(АрЩ) = «.

На пустом слове значение этих функций не определено.

Пусть А С В обозначает, что А является собственным началом В, то есть существует С ф е, такое что В = АС. Выражение А С В значит, что либо А С В, либо А = В.

Пусть Va ~ {В | е С В С А} — множество всех непустых начал А. На множестве Vs. отношение [I является строгим линейным порядком. Тем самым, определены понятия mine, maxc и [В, С]с. Последнее означает множество {В е Ра | В С Ю> С С}. Полуинтервал (В,С]с определяется аналогично.

Если 7 — бинарное отношение на некотором множестве X, то 7+ означает его транзитивное замыкание, а 7* — его транзитивно-рефлексивное замыкание.

Пусть (-){п)(п € Z) — семейство функций на FS, заданное следующими соотношениями:

(p$)(n>=p^lj, ДЛЯ^О, W

Определим следующую функцию И : Тр —► К:

Л(р) = 1; Н(А/В) = к(В\А) — Н(А); к{А ■ В) = к{А) + Н{В).

Перевод Ь-типов в элементы ЕЭ осуществляется с помощью следующего отображения [•]:

Ы = р[о{;

[(А/В)]] =

кл-

Пусть Л/"а = {® 6 Ра I «¿(®) нечетно}.

Определим бинарное отношение (р на множестве Ра следующим образом:

В^с <

(В С С) Л (d(C) = d(B) - 1)Л

Л(|{Ю> | В С Ю С C,d(D) = d(C)}| < ¡ff(B)l), если д{В) > 0; (С С В) Л (d{С) = d(В) - 1)Л

Л(|{Ю | С с D с В,¿(D) = d(C)}| < |э(В)|), если 5(В) < 0.

Пусть Ф(В) = {С | ВуэС}.

Рассмотрим секвенцию А\... Ап —► В. Пусть

На множестве определены отношение </?, функция Ф, а также множество Л/\у-

Множество 0 с Ту/ называется (/^-замкнутым, если изАб^иВузА следует, что В € Я.

Определим отношение /3 С Ту/ х Ту/ следующим образом:

Для А 6 Ту/ определим следующее множество:

= {В | ЭС(В^СЛА/?'С)ЛУВ((Ву>*ЮлА/?В) -+А/3'Щ}.

Пусть 7г функция из ЛЯу в Ту/. Пусть ф бинарное отношение на Ту/, определяемое следующим соотношением:

Определение 2.1.1. Тройку (7г, у, гр) будем называть сетью доказательства для слова Ш. Определим

Назовем доказательными условиями следующие ограничения на сеть доказательства.

1. Функция 7г является биекцией между Л/уу и Ту/ \ А/уу-

2. Для любого А € Л/\у верно, что Ь(тг(А)) — ¿(А).

4. Отношение (<р и ~ф)+ иррефлексивно.

5. Для любого А е Му/, такого что д(А) ф 0, для любого В 6 Ту/\Яу/, такого что А</>+В, верно, что АфЧУС(к<рС -V Сф+Ш)УШ'{ШфШ' ЭС(А^С А Ш'ф+С))

6. Для любого А 6 Ту/ \ Му/ существуют В € -7>(А) и С ^ ^(А), такие что С^*В.

В разделе 2.2 формулируется и доказывается критерий выводимости секвенций на основе доказательных условий.

А/ЗВ-» (А = 1) УЗС(Су>АЛСузВ). Определим отношение /3' С Ту/ х "Р\у следующим образом: А/З'В (А/ЭВ) Л УС(Су> А С(^В).

В = 7г(А), если А 6 ЛГ\у;

Ау?В, если А ^ Му/ и с?(А) ф 0.

=пип{А;тг(А)}; /4(А) = тах{А;7г(А)}.

3. /х-(А) с //-(В) д+(А) С /1~(В) У/4(®) С /х+(А).

Теорема 1.1/ Ь А\... Ап —* В, если и только если для слова = [Лх]^)... существует сеть доказательства (гг, (р, ф), удо-

влетворяющая доказательным условиям (1)-(5).

Ь I- А\... Ап —» В, если и только если для слова Щ = [Лх!^ ... существует сеть доказательства (ж, ф), удо-

влетворяющая доказательным условиям (1)-(6).

В главе 3 доказывается NP-пoлнoтa задач распознавания выводимости для лево- и правостороннего фрагментов исчисления Ламбека и их вариантов, допускающих пустые антецеденты.

Теорема 2. Задача распознавания выводимости секвенций в Ь(-,\), Ь(-,Д 1/(-,\) иЬ*(-,/) ЫР-полна.

Следствие 1. Задача распознавания принадлежности данного слова языку, порожденному данной грамматикой, основанной на Ь(-, \), Ь(-,/), 1/(-,\) или Ь*(■,/), ИР-полна.

В разделе 3.1 приводится конструкция, с помощью которой сводится известная №-полная задача БАТ к задаче распознавания выводимости в данном фрагменте. Для правостороннего фрагмента работает конструкция, симметричная построенной.

Для каждой булевой переменной Xi пусть обозначает лите-

рал -nxi, а -112)1 обозначает литерал ж*.

Пусть р?, Г{, где 0<г<п+1,0<:/<ш — различные примитивные типы из Р.

Определим следующие семейства типов:

- (Ро\Рп+г);

сР = {(УоХ^-1)-^!); С = Я? = <р1Ш

Щ = Щ = Щ1;

Е^ь) = (р?_ДР°);

= | ((р1-ЛЕГ1(1)) ■ Ю> если ^г присутствует в Су,

* \ • р!))> если ^¡Хг не присутствует в су,

= (Ех(0) • ((^(0)^(1)) • (ЯДп)));

Л = (((^_1(0)\П_1)\^(0)) • (№(0)\Д(1)) • (Н{\п))), для 1 < г < п + 1;

Ян-! = ((£„(0)\г„)\Яп+1).

Лемма 3.1.1. Следующие утверждения эквивалентны: 1. сх А ... A Cm выполнима.

Раздел 3.2 посвящен доказательству леммы 3.1.1.

В главе 4 доказывается NP-лолнота задачи распознавания выводимости для фрагмента исчисления Ламбека без умножения и его варианта, допускающего пустые антецеденты.

Теорема 3. Задача распознавания выводимости секвенций в L(\, /) и L*(\,/) NP-полна.

Следствие 2. Задача распознавания принадлежности данного слова языку, порожденному данной грамматикой, основанной на L(\, /) или L*(\,/), NP-полна.

Эта теорема доказывается также с помощью сведения задачи SAT к задаче распознавания выводимости в этих фрагментах.

В разделе 4.1 приводится конструкция, необходимая для такого сведения.

Пусть р?, qj, al, Ь-, где 0<i<n,0<j'<m — различные примитивные типы из Р.

Определим следующие семейства типов:

G0 = (рЖ)

G = Gm

= kV?)

А, = А™

яйШ-г/Щ WM-iM'1), если есть в Cj

(^/(¿/(ЩЛШ'^Ш-х, если нет в Cj

S. L*(-, \)\- F\... Fn+\ —» G

F№ = (£/(f)W) W) = Fnt)

Bi = вГ\рГ-1

3-1

Пусть П* обозначает следующие последовательности типов:

(ЪФШВЛА)) ВД (Ъ(0)\т))-

Лемма 4.1.1. Следующие утверждения эквивалентны:

С1 А ... А Ст выполнима Ц\,/)ЬП1...ПП->С Ь*(\,/)НП1...ПП->С?

Раздел 4.2 посвящен доказательству леммы 4.1.1.

В главе 5 рассматривается фрагмент исчисления Ламбека с одним делением.

В разделе 5.1 доказывается новый критерий выводимости для этого фрагмента с использованием другого представления секвенций и других доказательных условий.

Рассмотрим отображение [•]': Тр(\) —> ГЭ:

1Р1' = Р\1\; 1(А\в)у = 1ВПИГ)<0);

Секвенции А\... Ап —► В мы поставим в соответствие строку W =

Функция я* будет определена на всем множестве Ту/- Сетью доказательства мы будем называть саму функцию п. Доказательные условия:

Г. Для всех А 6 Руу верно, что 7Г2(А) = А.

2'. Для всех А 6 7\у верно, что Ь(тг(А)) ■— £(Л).

3'. /х~(А) с /х-(В) =» М+(А) С М-(В) V <(В) С м+(А).

4'. «(А)) = + 1.

5'. Если с1(/1^(А)) — для некоторого ] > 0, то существует такое

В 6 (/1-(А),/£(А))С, что (¿(В) < 2з.

6'. Если А)) = 2] для некоторого ] > 0, то либо существует такое В 6 (/^(А),/4(А))С, что (¿(В) < 2.7, либо

тг(А) = тах{В | УС € (А, В]сй(С) > ¿(А)}.

Теорема 4. L(\) b A\... An —► В, если и только если п > 0 и для

существует сеть доказательства тг, удовлетворяющая доказательным условиям (1 ')-(б').

Теорема 5. L*(\) b Ai... Ап —» В, если и только если для

W = [a1]'...[A.№]')<0)

существует сеть доказательства -к, удовлетворяющая доказательным условиям (1 ')-(4') и (6').

В разделе 5.2 строится полиномиальный алгоритм, позволяющий определять принадлежность слова языку, порожденному данной грамматикой, за полиномиальное время, и доказывается его корректность.

Пусть (£,Р,Д, В) — грамматика Ламбека, основанная на L(\) или

L*(\)-

Размером грамматики назовем число ЦВ}'\ + Soei: 2лея(а) IM'I-

Теорема 6. Существует алгоритм, который по данному слову и данной грамматике, основанной на L(\) или L*(\), распознает принадлежность этого слова языку, порожденному данной грамматикой, за время, ограниченное полиномом от длины слова и размера грамматики.

Автор благодарит своего научного руководителя профессора М. Р. Пентуса за постановку задачи, поддержку и внимание к работе.

Работы автора по теме диссертации

[1] Саватеев Ю. В. Распознавание выводимости для исчисления Ламбека с одним делением // Вестник Московского университета. Серия 1, Математика. Механика. - 2009. — № 2. — С. 59-62.

[2] Savateev Y. Lambek grammars with one division are decidable in polynomial time // Computer Science — Theory and Applications / Editors E.A. Hirsch et al.. - Berlin: Springer, 2008. — P. 273-282. -(Lecture Notes in Computer Science; vol. 5010).

[3] Savateev Y. Product-free Lambek calculus is NP-complete // Logical Foundations of Computer Science, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3-6, 2009. Proceedings / Editors S. N. Artemov and A. Nerode. — Berlin: Springer, 2009. — P. 380—394. — (Lecture Notes in Computer Science; vol. 5407).

Подписано в печать 27. /0.09 Формат 60x90 1/16. Усл. печ. л. 0,75 Тираж /00 экз. Заказ

Отпечатано с оригинал-макета на типографском оборудовании механико-математического факультета МГУ имени М. В. Ломоносова

Содержание диссертации автор исследовательской работы: кандидата физико-математических наук, Саватеев, Юрий Вячеславович

Введение

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 Алгоритм распознавания принадлежности

Введение диссертация по математике, на тему "Алгоритмическая сложность фрагментов исчисления Ламбека"

Общая характеристика работы

Актуальность темы.

Диссертация посвящена исследованию алгоритмической сложности фрагментов исчисления Ламбека.

Исчисление Ламбека L было введено в [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(-,/) и !/(-,/) также является NP-полной.

Таким образом, теперь для всех фрагментов исчисления Ламбе-ка, заданных ограничениями набора связок, установлены точные оценки алгоритмической сложности задачи распознавания выводимости.

В качестве основной техники для исследования выводимости во фрагментах ассоциативного исчисления Ламбека мы используем так называемые сети доказательства — метод, позволяющий наглядно и компактно представлять вывод формулы в данном исчислении, полностью передавая его принципиальную структуру (аналоги использовались в [14], [7]). Этот метод успешно применялся в [12], [15] и [16]. Также в 2005 году в [11] была попытка применить данный метод для исследования выводимости во фрагменте исчисления Ламбека без умножения, однако там не было получено никаких результатов, связанных с алгоритмической сложностью. Еще один критерий (близкий к критерию из [16], однако формально неверный) для этого фрагмента был предложен в [6].

Цель работы.

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

Методы исследования.

В работе применяются методы теории доказательств. Основным инструментом исследования выводимости является построение так называемых сетей доказательства с различными свойствами, отвечающими конкретному фрагменту исчисления Ламбека.

Научная новизна.

Результаты диссертации являются новыми, среди них:

1. Задачи распознавания выводимости в исчислении NP-полны для L(, \), L(\, /), Ц-, /), L*(-,\), L*(\, /), L*(-, /)•

2. Задачи распознавания принадлежности данного слова языку, порождаемому данной категориальной грамматикой, NP-полны для L(-,\), L(\, /), L(-, /), L*(, \), L*(\, /), L*(, /).

3. Задачи распознавания выводимости в исчислении разрешимы за полиномиальное время для L(\), L*(\), L(/), L*(/).

Теоретическая и практическая ценность.

Работа носит теоретический характер. Результаты, полученные в диссертационной работе, представляют интерес для математической лингвистики. Полученные результаты могут быть полезны специалистам, работающим в МГУ им. М. В. Ломоносова, МИ РАН им. В. А. Стеклова, ПОМИ РАН им. В. А. Стеклова, Институте математики им. С. Л. Соболева СО РАН, ИППИ РАН и др.

Апробация работы.

Результаты диссертации докладывались на следующих семинарах и конференциях:

• На международной конференции "Компьютерные науки в России" (CSR-2008), Москва, Россия, 7-12 июня 2008 года.

• На семинаре "Алгоритмические вопросы алгебры и логики" под руководством академика РАН С.И. Адяна (2008, 2009).

• На Европейской летней школе по логике, лингвистике и информатике (ESSLLI-2009), Бордо, Франция, 20-31 июля 2009 года.

Публикации.

Основные результаты диссертации опубликованы в работах [15]

17].

Структура работы.

Работа состоит из введения, 5 глав, содержащих 12 разделов, и списка литературы. Библиография содержит 17 наименований. Текст диссертации изложен на 75 страницах.

Список источников диссертации и автореферата по математике, кандидата физико-математических наук, Саватеев, Юрий Вячеславович, Москва

1. Aarts Е., Trautwein К. Non-associative Lambek categorial grammar in polynomial time 1.j Mathematical logic Quarterly. — 1995. — Vol. 41, № 4. - P. 476-484.

2. Buszkowski W. The equivalence of unidirectional Lambek categorial grammars and context-free grammars // Zeitschrift fur mathematische Logik und Grundlagen der Mathematik. — 1985. — Vol. 31. — P. 369— 384.

3. Metayer F. Polynomial equivalence among systems LLNC, LLNCa and LLNCo // Theoretical Computer Science. — 1999. Vol. 227, №1,-P. 221-229.

4. Montague R. English as a Formal Language // Linguaggi nella societa e nella tecnica. — / Editor Bruno Visentini. — Milan: Edizioni di Comunita, 1970. P. 189-223.

5. Moortgat M. Categorial type logic, // Handbook of Logic and Language / Editors J. van Benthem, A. ter Meulen. — Elsevier. — 1997. — P. 93— 177.

6. Morrill G. Type Logical Grammar: Categorial Logic of Signs // Berlin: Springer. 1994. - 328 p.

7. Penn G. A Graph-Theoretic Approach to Polynomial-Time Recognition with the Lambek Calculus // Electronic Notes in Theoretical Computer Science. Elsevier. - 2005. - Vol. 53.

8. Pentus M. Lambek calculus is NP-complete // Theoretical Computer Science. 2006. - Vol. 357, № 1/3. - P. 186-201.

9. Pentus M. Lambek grammars are context free // Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science: June 19—23, 1993. Montreal, Canada. — Los Alamitos, California: IEEE Computer Society Press, 1993. P. 429-433.

10. Roorda D. Resource Logics: Proof-theoretical Investigations: Ph.D. thesis. Amsterdam, 1991. - 138 p.Работы автора по теме диссертации

11. Savateev Y. Lambek grammars with one division are decidable in polynomial time // Computer Science — Theory and Applications /Editors E.A. Hirsch et al. — Berlin: Springer, 2008. — P. 273—282. — (Lecture Notes in Computer Science; vol. 5010).

12. Саватеев Ю. В. Распознавание выводимости для исчисления Ламбе-ка с одним делением // Вестник Московского университета. Серия 1, Математика. Механика. — 2009. — № 2. — С. 59—62.