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

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

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

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

С

Кузнецов Степан Львович

Категориальные грамматики, основанные на вариантах исчисления Ламбека

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

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

1 о

Москва 2012

005016792

005016792

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

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

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

Официальные оппоненты: Лысёнок Игорь Геронтьевич,

Ведущая организация: Тверской государственный университет.

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

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

Автореферат разослан 27 апреля 2012 года.

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

доктор физико-математических наук (Математический институт имени В. А. Стеклова РАН, ведущий научный сотрудник);

Кудинов Андрей Валерьевич, кандидат физико-математических наук (Институт проблем передачи информации им. A.A. Харкевича РАН, старший научный сотрудник).

профессор

А. О. Иванов

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

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

Актуальность темы. Исчисление Ламбека L введено И. Ламбеком1 для описания синтаксиса естественных языков с помощью основанных на нём категориальных грамматик1 2 3. В исчислении Ламбека используются синтаксические типы, построенные из примитивных типов с помощью трёх двуместных связок — умножения, левого и правого делений.

Хомский4 предложил другое семейство грамматик, среди которых наиболее известны контекстно-свободные грамматики. Они широко применяются для анализа искусственных языков (например, языков программирования5), однако для естественных языков категориальные грамматики обладают рядом преимуществ, прежде всего — свойством лек-сикализации: вся синтаксическая информация хранится в категориальном словаре, и при анализе нужно рассматривать не всю грамматику, а только часть словаря, относящуюся к словам, встречающимся в данном фрагменте текста. Категориальные грамматики позволяют, параллельно с синтаксическим разбором, вести разбор семантический, используя, например, семантику Монтегю6.

Отдельным вопросом является сравнение самих классов языков, по-

1 J. Lambek. The mathematics of sentence structure. American Mathematical Monthly. 65, No. 3, 1958, 154-170. Русский перевод: И. Ламбек. Математической исследование структуры предложений. Математическая лингвистика: сборник переводов, под ред. Ю. А. Шрейдера и др. — М.: Мир, 1964. — С. 47—68.

2G. Morrill. Categorial grammar: logical syntax, semantics and processing. Oxford: Oxford University Press, 2011.

3M. Moortgat. Categorial type logic. Handbook of Logic and, Language, ed. by J. van Benthem and A. ter Meulen. Elsevier, 1997.

4N. Chomsky. Three models for the description of language. IRE Transactions on Information Theory. I T-2, No. 3, 1956, 113-124. Русский перевод: H. Хомский. Три модели описания языка. Кибернетический сборник, вып. 2. — М.: ИЛ, 1961. — С. 237—266.

®А. V. Aho, R. Sethi, J. D. Ullman. Compilers: principles, techniques and tools. — Reading, Mass.: Addison-Wesley, 1985. Русский перевод: А. В. Ахо, P. Сети, Дж. Д. Ульман. Компиляторы: принципы, технологии, инструменты. — М.: «Вильяме», 2003.

6В. Carpenter. Type-logical semantics. — Cambridge, Mass.: The MIT Press, 1997.

рождаемых разными типами грамматик, без учёта синтаксических и семантических структур. В этом (так называемом слабом) смысле, оказывается, грамматики Ламбека не богаче контекстно-свободных: класс языков, порождаемых грамматиками, основанными на исчислении L, совпадает с классом контекстно-свободных языков без пустого слова7. Естественный интерес представляют аналогичные вопросы для вариантов исчисления Ламбека (его расширений и фрагментов). Известно8, что для порождения всех контекстно-свободных языков достаточно фрагмента исчисления Ламбека, содержащего только одно деление — L(\). Кана-зава9 исследовал языки, порождаемые грамматиками, основанными на исчислении Ламбека с добавлением аддитивных конъюнкции и дизъюнкции: этот класс строго содержит класс конечных пересечений контекстно-свободных языков и содержится в классе контекстно-зависимых языков; вопрос о точном описании этого класса открыт. Мортгат10 ввёл исчисление Ламбека, обогащённое двумя модальностями; Егер11 показал, что все языки, порождаемые основанными на этом исчислении грамматиками, являются контекстно-свободными. Диковским и Дехтярём12 рассматривались категориальные грамматики зависимостей (CDG), в основе которых лежит обогащённый дополнительными связками для нелокальных зависимостей фрагмент исчисления Ламбека без умножения, с ограничением: у каждой операции деления в знаменателе стоит примитивный тип; языки, порождаемые такими грамматиками, образуют особый класс, строго содержащий класс контекстно-свободных языков и замкнутый относительно операции объединения, пересечений с регулярными языками, а также взятия образа и прообраза при неукорачивающих гомоморфизмах. Бушковский13 доказал, что грамматикой, основанной на расширении исчисления Ламбека конечным набором дополнительных аксиом, можно

7М. Р. Пентус. Исчисление Ламбека и формальные грамматики. Фундаментальная и прикладная математика. Том 1, № 3, 1995, 729—751.

8W. Buszkowski. The equivalence of unidirectional Lambek categorial grammars and context-free grammars. Zeitschrift für mathematische Logik und Grundlagen der Mathematik. 31, 1985, 369-384.

9M. Kanazawa. The Lambek calculus enriched with additional connectives. Journal of Logic, Language and Information, 1, 1992, 141-171.

10M. Moortgat. Multimodal linguistic inference. Journal of Logic, Language and Information, 5, No. 3-4, 1996, 349-385.

nG. Jäger. On the generative capacity of multi-modal categorial grammars. Research on Language and Computation, 1, No. 1-2, 2003, 105-125.

12M. Dekhtyar, A. Dikovsky. Generalized categorial dependency grammars. TYakhtenbrot/Festschrifl, ed. by A. Avron et al. Lecture Notes in Computer Science, Vol. 4S00. Berlin etc.: Springer, 2008, 230-255.

13 W. Buszkowski. Some decision problems in the theory of syntactic categories. Zeitschrift für mathematische Logik und Grundlagen der Mathematik. 28, 1982, 539-548.

породить любой рекурсивно перечислимый язык.

Автором диссертации доказано, что для порождения всех контекстно-свободных языков без пустого слова достаточно фрагмента L(\;pi) — исчисления Ламбека с одним делением и одним примитивным типом; также в работе доказано, что все языки, порождаемые грамматиками, основанными на исчислениях Li (исчисление Ламбека с единицей) и LR (исчислении Ламбека с операцией обращения; см. ниже), контекстно-свободны.

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

Алгоритмические проблемы выводимости (и, следовательно, задачи проверки принадлежности слова к языку, порождаемому категориальной грамматикой) для исчисления Ламбека L и его фрагментов L(\,/) и L(-,\) являются NP-полными (для L NP-полнота доказана Пентусом15, для L(\,/) и L(-,\) — Саватеевым16); однако Пентусом17 и Фаулером18 были независимо предложены полиномиальные (время работы порядка 0(п5)) алгоритмы для практически важного частного случая, когда сложность типов ограничена константой; Фаулер19 успешно применял такие алгоритмы для разбора предложений на английском языке. Сходное явление наблюдается и для CDG: общая задача проверки принадлежности слова языку, порождаемому такой грамматикой, NP-полна, однако, если сложность типов ограничена, существует полиномиальный алгоритм. Для фрагмента с одним делением L(\) Саватеевым предложен полиномиальный (время работы порядка 0(п3)) алгоритм проверки при-

14М. Р. Пентус. Полнота синтаксического исчисления Ламбека. Фундаментальная и прикладная математика. Том 5, № 1, 1999, 193—219.

15М. Pentus. Lambek calculus is NP-complete. Theoretical Computer Science, 357, No. 1-3, 2006, 186-201

18Ю. В. Саватеев. Алгоритмическая сложность фрагментов исчисления Ламбека. Дисс. ... канд. физ.-мат. наук, специальность 01.01.06, защищена 11.12.2009. М., 2009. 75 с.

17М. Pentus. A polynomial-time algorithm for Lambek grammars of bounded order. Linguistic Analysis. 36, No. 1-4, 2010, 441-471.

18T. A. D. Fowler. A polynomial time algorithm for parsing with the bounded order Lambek grammars. The Mathematics of Language: proceedings of the 10-th and 11-th Biennial Conference, MOL 2010 and MOL 2011, ed. by Ch. Ebert, G. Jager and J. Michaelis. Lecture Notes in Computer Science, Vol. 6149. Berlin etc.: Springer, 2009, 36-43.

19T. A. D. Fowler. Parsing CCGBank with the Lambek calculus. Parsing with Categorial Grammar Workshop, ESSLLI 2009. Bordeaux, 2009, 38-42.

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

В качестве следствий из предлагаемых конструкций автором диссертации получены теоремы об NP-пoлнoтe для исчислений ЬР*(\), Ь(-, \;рх) и Ь(\,/;рх) (и их консервативных расширений, содержащихся в Ьп), а также полиномиальный алгоритм для проверки принадлежности слова к языку, порождаемому Ьх(\)-грамматикой.

Цель работы. Выявление места в иерархии Хомского классов языков, порождаемых категориальными грамматиками, основанными на исчислениях Ц\;р1), Ь*(\;р1) (а также их консервативных расширениях, являющихся фрагментами Ь и Ьх соответственно) и на исчислении Ьх. Построение расширения исчисления Ламбека одноместной связкой к, полного относительно интерпретации на подмножествах свободной полугруппы, где к интерпретируется как обращение языка; выявление места в иерархии Хомского класса языков, порождаемых грамматиками, основанными на полученном исчислении. В качестве дополнительных следствий из доказанных теорем также установлены оценки алгоритмической сложности проблем выводимости для некоторых вариантов исчисления Ламбека.

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

1. класс языков, порождаемых Ьх-грамматиками, совпадает с классом контекстно-свободных языков;

2. проблема выводимости в Ьх(\) разрешима за полиномиальное время;

3. класс языков, порождаемых Ц\; рх)-грамматиками, совпадает с классом контекстно-свободных языков, не содержащих пустого слова;

4. проблема выводимости в Ц-,\;рх) ОТ-полна;

5. построено исчисление Ь11 для унарной операции обращения и доказана его полнота относительно моделей на подмножествах свободной полугруппы; класс языков, порождаемых Ьк-грамматиками, совпадает с классом контекстно-свободных языков, не содержащих пустого слова.

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

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

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

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

• на международном коллоквиуме «Структуры и вывод» (Structures and Déduction 2009) в составе 21-й Европейской летней школы по логике, лингвистике и информатике (ESSLLI-2009), Бордо, Франция, 20—31 июля 2009 года;

• на 15-й и 16-й Эстонских зимних школах по компьютерным наукам (EWSCS-2010 и 2011), Палмсе, Эстония, 28 февраля — 5 марта 2010 года и 27 февраля — 4 марта 2011 года;

• на семинаре «Алгоритмические вопросы алгебры и логики» под руководством академика РАН С. И. Адяна, Москва, Россия, 16 марта 2010 года, 15 марта 2011 года и 21 февраля 2012 года;

• на международной конференции «Формальные грамматики» (Formai Grammar 2011), Любляна, Словения, 6 августа 2011 года;

• на международной конференции «Логические методы доказательств и вычислений» (LMRC-2012), Москва, Россия, 1—3 февраля 2012 года;

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

Публикации. Основные результаты диссертации опубликованы в работах [1]—[4], из них первые три — в журналах из перечня ВАК.

Структура диссертации. Работа состоит из введения, четырёх глав, содержащих 21 раздел, и списка литературы. Библиография содержит 37 наименований. Текст диссертации изложен на 70 страницах.

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

Глава 1 является вспомогательной. В ней вводятся необходимые для дальнейшего изложения понятия и формулируются ранее известные результаты.

В разделе 1.1 определено исчисление Ламбека Ь. Счётное множество Рг = {р\,Р2^Рз, • • • } называется множеством примитивных типов; р\ будем обозначать также просто р. Множество Тр типов исчисления Ламбе-ка определяется как наименьшее в смысле включения множество, удовлетворяющее следующим двум условиям: (1) Рг С Тр; (2) если А, В 6 Тр, то (А\В), (В / А), (А • В) е Тр. Типы обозначаются большими латинскими буквами, их конечные последовательности — заглавными греческими; пустая последовательность обозначается буквой Л. Выводимыми объектами в исчислении Ламбека являются секвенции — выражения вида П —> С.

Исчисление Ь задаётся аксиомами вида р, —Рг (акс.) и правилами вывода

АП-ч-В / .и ггтг гт / л. П -»■ А Г В А -> С п

В , п и , . П.-* А ГВА-+С ,,

Г -> А Д В , ч ГЛДА-»С ,

^ 'Я ^ / /1 т А гя I"

ГД->А-£ ^ Г (Л • В) Д -> С

(сг^).

П-»А ГЛД-+С ГПД -»С

Обозначим через Тр(\) множество типов, не содержащих ни •, ни /. Исчисление, заданное аксиомами (акс.) и правилами (\ ->) и (—> \), обозначается Ь(\). (Вместо \ можно взять /, при этом получится симметричная теория; мы будем везде рассматривать \.) Аналогично определяются исчисления Ц-,\) и Ь(\,/).

Через Тр(рх,... ,рдг) обозначим множество типов, содержащих только примитивные типы из множества {рг, ■.. ,рлг}- Если в исчислении Ламбека ограничиться такими типами, получится исчисление

Ь(р1,... ,рдг); его фрагменты с ограниченными наборами связок обозначаются Ь(\;рх,... ,рм), Ь(-,\;р1,... ,рлг), Ц\>/;рх, .. -,рм)-

В разделе 1.2 вводится исчисление Ламбека, допускающее пустые левые части секвенций (Ь*), и исчисление Ламбека с единицей (Ьх), а также фрагменты этих исчислений. Исчисление II получается из Ь отбрасыванием ограничения П ф Л на правила (-> \) и (-> /). Через Трг обозначается множество всех типов, построенных из примитивных типов и константы 1 с помощью связок •, \ и /. Исчисление Ьх получается из Ь* добавлением аксиомы —> 1 (обозначается (—> 1)) и правила вывода

Г1А-+А К

при этом в качестве множества типов вместо Тр используется Трх.

В разделе 1.3 определяется понятие консервативного расширения (фрагмента), доказывается допустимость в исчислении Ламбека и его вариантах правила подстановки, определяется отношение эквивалентности типов. Подстановка типа А вместо г (г 6 Рги{1}) в обозначается •б/[л := А]. Здесь л/ может быть любым синтаксическим объектом: типом, последовательностью типов, секвенцией или (см. далее) грамматикой. Запись := А\, Х2 Аг,...] (или, сокращённо, := Л*]) означает, что все подстановки осуществляются одновременно.

Раздел 1.4 содержит определение категориальной грамматики и формулировки результатов Гайфмана — Бушковского и Пентуса об эквивалентности (в слабом смысле) Ь-грамматик и контекстно-свободных грамматик.

Определение. Пусть — один из вариантов исчисления Ламбека (Ь, Ьх, (определяется ниже), или фрагмент одного из этих исчислений), Тр с£ — соответствующее множество типов. Грамматикой, основанной на исчислении -грамматикой) называется тройка Я = (Е, Н, >}, где

£ — некоторое непустое конечное множество (алфавит), Н е а > С Тр_£> хЕ - произвольное конечное бинарное соответствие. Язык, порождаемый грамматикой (?, есть Я(0) = {ах... ак е £* | 3_Оь ... ,Вк- Bi > а* и «£? Ь В\... В к Н}. Такие языки называются Л?-языками. Теорема 2—3 20 (X. Гайфман, 1960; В. Бушковский, 1985; М. Р. Пен-тус, 1993). Класс Ъ-языков совпадает с классом контекстно-свободных языков без пустого слова.

20Мы сохраняем нумерацию теорем, используемую в диссертации (поэтому нумерация здесь не сплошная). Теоремы 2 и 3 для краткости сформулированы в виде одной теоремы.

В разделе 1.5 даётся краткая сводка известных результатов об алгоритмической сложности фрагментов исчисления Ламбека для дальнейших ссылок.

В разделах 1.6 и 1.7 формулируются исчисления MCLL', MCLL и MCLLi(x (фрагменты линейной логики), устанавливается их связь с L, L* и Li соответственно и доказываются теоретико-графовые критерии выводимости в этих исчислениях.

Множество Var = {pi,P2,P3, • • • } называется множеством переменных-, At = Var U {g | q S Var} U {1, J.} — множество атомов. Формулы строятся из атомов с помощью двуместных связок и <8>. Секвенции MCLLi.j. имеют вид —> Г, где Г — конечная последовательность формул. Линейное отрицание формулы определяется рекурсивно: = pi, р^ = p¿, Iх = -L, Х-1 = 1, (АЪВ)1- = (А^В)1- = ВХЪА±. Аксиомы MCLLi,x

имеют вид —> pipi и —1. Правила вывода таковы:

И*);

^ (цикл.).

Стандартный перевод А типа А € Тр: определяется рекурсивно: р1 = Р1 {Рг е Рг), 1 = 1, А~В = А® В, А\В = А-Ь-ЪВ, В / А — ВЪА-1. Если Въ...,Вт,С £ Трх, то Ъ1 I- Вг... Вт С МСЬЬх,х Ь

В^ ... В±С. Фрагмент МСЬЬх,± без 1и1 обозначается МСЬЬ и соответствует Ь*; исчислению Ь соответствует исчисление МСЬЬ', получающееся из МСЬЬ добавлением ограничения ГД ^Лк правилу (—>1?).

Для исследования выводимости в МСЬЬ и МСЬЬ' (а, следовательно, и в Ь* и Ь) применяются сети доказательства. Мы используем их вариант, предложенный Пентусом. Пусть Г = А\... Ат. Запишем Г так: <>А\0.. .оАт. Занумеруем здесь все символы, кроме скобок (атом считается одним символом); множество пар (символ, номер), называемых вхождениями, обозначим С1г. Для а, /3 6 О г считаем, что а <г /?, если номер а меньше номера /3; отношение -¡г есть транзитивное замыкание деревьев синтаксического разбора формул А\, ..., Ат (если а лежит в поддереве с корнем /3, то а -<г Р)- Вхождение X подформулы есть соответствующее подмножество Г2р; 1(^0 есть вхождение связки непосредственно слева, а г(Х) — непосредственно справа от X (если такового нет, то г (Л') = (о, 1)). Множество вхождений обозначим Пр, о — Г2р, ® — П®, атомов вида pi , атомов вида pi — Пр1

'■) положим — ^р* ип?..

Определение. Сетью доказательства называется структура ОТ = ({Г2г> <г, -<г)) Л, £), где Л,£ С Пг хГ2р, удовлетворяющая следующим аксиомам: (1) - = 2; (2) Л — всюду определённая функция из в (3) £ — биективная функция из Г2р'+ в Ир' , и если а — вхождение Ри то £{а) — вхождение (4) граф (Г2г, Л и £) может быть изображён без пересечений в одной полуплоскости, если его вершины расположены на её границе в порядке <г; (5) граф (Ог, Л и -<г> ациклический.

Определение. Сильной сетью доказательства называется сеть доказательства, удовлетворяющая дополнительной аксиоме: (6) для любого вхождения ХсПг подформулы -4(1(Х)) ф Л(г(Аг)). где Л(а) есть А(а), если а € О®, и а, если а 6

Теорема 13 (М. Р. Пентус, 1996). Секвенция -» Г выводима в исчислении МСЬЬ тогда и только тогда, когда существует сеть доказательства для Г.

Теорема 14. Секвенция ->• Г выводима в исчислении МСЬЬ' тогда и только тогда, когда существует сильная сеть доказательства для Г.

В разделе 1.8 изложен способ построения Ь*-грамматики для контекстно-свободного языка М, содержащего пустое слово. Рассмотрим язык М — {е}. Для него в силу теоремы 2-3 существует Ь-грамматика 9 — {£, с>,#). Конструкция этой грамматики такова, что тип Н примитивный (можно считать, что Н = р{), а все типы, встречающиеся в категориальном словаре о, имеют вид р^, pj\pi или рк \рг), причём к,э Ф 1. Если рассмотреть Я как Ь*-грамматику, порождаемый ей язык не изменится. Осуществим в грамматике 0 подстановку типа Б = ((г\г) \((в \ в) \ д)) \<7 вместо рь Получится грамматика, порождающая язык Я(<?) и {е} = М (это доказывается с помощью сетей доказательства). Тем самым устанавливается, что класс контекстно-свободных языков совпадает с классом Ь*-языков. Несмотря на естественность такого утверждения, случай языка с пустым словом ранее разобран не был.

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

В разделе 2.1 приведена технически более удобная формулировка исчисления Ь1. В разделе 2.2 описана подстановка, сводящая выводимость в Ь1 к выводимости в Ь*:

Теорема 16. Если П С — секвенция с типами из Трг иц — примитивный тип, не встречающегося в этой секвенции, то верна равносильность

Ь*н (П->С)Ь*:= (1-Й) ■!][!:=

Из этой теоремы получается следствие, характеризующее класс Ь].-языков:

Теорема 17. Всякий Ъх-язык контекстно-свободен.

В разделе 2.3 описана подстановка, сводящая выводимость в 1а(\) к выводимости в Ь*(\):

Теорема 18. Если П -> С — секвенция с типами из Трг(\) ид — примитивный тип, не встречающийся в этой секвенции, то верна равносильность

М\)Ы1^С <!=> Ъ*(\)Ь(П ->С)[1:=д\д, й := (д.\?)\(рЛд)].

Отсюда следует полиномиальная разрешимость проблемы выводимости в 1а(\):

Теорема 19. Существует алгоритм, проверяющий выводимость секвенции в исчислении Ьх(\) за время 0(п3), где п — длина секвенции (количество вхождений связок, примитивных типов и константы 1).

Глава 3 посвящена исчислению Ламбека (Ь(р)) с одним примитивным типом и его фрагментам (Ь(\;р) и др.). В разделах 3.1 и 3.2 предъявляется конструкция (подстановка типов), сводящая выводимость в Ь(\) к выводимости в Ь(\;р), и при помощи сетей доказательства обосновывается её корректность:

Теорема 20. Для любой секвенции П -> С, где П = В±... Вт, т ^ 1, и В1,..., Вт, С € Тр(\;р1,... имеет место равносильность

Ь(\;р)Н(П-»С)[рг -.= Аи...,рм

где Ак = (/+1 • (((р • р) \р)\р) -р»-^) \р, к = 1,..., N.

Выражение вида {Бх ■ ... ■ Бт) \ С здесь понимается как сокращение для Бт \(£>т_1 \(1)т_2 \ •.. \(£>1 \ С)...)); рт означает р..... р (тп раз).

Та же конструкция работает для соответствующих фрагментов Ь*. Применяемая подстановка зависит от множества примитивных типов, встречающихся в данной секвенции; в разделе 3.5 построена единая равномерная подстановка. Разделы 3.3 и 3.4 содержат приложения предложенной конструкции:

Теорема 24. Класс Ь (\;р) -языков совпадает с классом контекстно-свободных языков без пустого слова, а класс Ь*(\;р)-языков — с классом всех контекстно-свободных языков.

Теорема 25. Проблемы выводимости в исчислениях Ь(-,\;р) и Ь*(-,\;р) ЫР-полны.

Глава 4 посвящена исчислению Ламбека с операцией обращения (Ь11). В разделе 4.1 вводится понятие модели на подмножествах свободной полугруппы (Ь-модели, языковой модели) и формулируется теорема Пен-туса о полноте исчисления Ь относительно Ь-моделей. В разделах 4.1—4.4 алфавит £ считается произвольным непустым конечным или счётным множеством. Формальные языки без пустого слова над £ образуют множество 7-'(£+). На нём заданы три операции (умножение, левое и правое деление): М ■ N = {ии \ и € М,у <Е ЛГ}; М\М = {и 6 £+ | (Уи еМ)га£ ЛГ}; Ы/М = {и е £+ | (Уи е М)ии е Л^}.

Определение. Ь-моделъю называется структура Л4 — (£, и>), где ю — такое отображение из Тр в £+, что ш(А • В) = ъи{А) • и>{В), ги(А\В) = ю(А)\ги(В), ги(В/А) = ю(В) / ги(А) для любых А,В е Тр. Секвенция • • • ->• <? истинна в модели М, если го^) •... • ги(Рт) С ги(С).

Теорема 27 (М. Р. Пентус, 1995). Секвенция выводима в исчислении Ь тогда и только тогда, когда она истинна во всех Ь-моделях.

В разделе 4.2 предъявляется исчисление ЬЕ. Типы ЬЕ строятся из примитивных типов с помощью двуместных связок \, /, • (как и в случае Ь), а также одноместной связки 11 (пишется в постфиксной форме, Лн). Помимо аксиом и правил исчисления Ь, в Ьн имеются следующие правила:

_л¿±С_ нд ГАА^С (КК , Г С , щц

Понятие Ь-модели естественным образом обобщается на Ьа: теперь ю: Тра —>• 7?(£+), а к условиям на ю добавляется ш(Ап) = ги(Л)к.

Теорема 28. Секвенция с типами из Тря выводима в исчислении Ьа тогда и только тогда, когда она истинна во всех Ь-моделях.

Теорема о полноте показывает, что расширение выбрано правильно. В разделе 4.3 доказывается, что каждый тип из Тра эквивалентен типу в нормальной форме — типу, в котором связка я встречается только непосредственно около примитивных типов.

В разделе 4.4 доказывается теорема 28. Пусть некоторая секвенция (можно считать, что она состоит из типов в нормальной форме) невы-водима в Ьп. Тогда она тем более невыводима без применения правил для к, поэтому по теореме 27 существует опровергающая её модель М. Построим по ней модель М2, опровергающую данную секвенцию и удовлетворяющую условию (\М е Трп)ад(Ан) = (в модели М оно может нарушаться).

Пусть Ф — множество подтипов данной секвенции. Определим рекурсивно счётчик /(А), А 6 Ф: /(р,) = /(р^) = 1, ¡{А-В) = /(А)+ /(£) +10,

f(A\B) = f(B/A) = /(В); положим К = max{f(A) \ A e Ф}, N — 2К + 25. Рассмотрим алфавит Si = S x {1,..., N} и гомоморфизм h: S+ —»■ E+, a ^ (a, 1)... (a, N). Пусть T = {и £ Ef | и не является под-словом слова вида h(v) или h(v)R (v 6 Е+) или и начинается или оканчивается символом вида (а, 2к)}. Положим 11)2(pi) = h(w(pi))Uh(w(pf/))KL)T и продолжим отображение W2 на все типы из Тр по определению L-модели для Полученная модель М2 = (Ei,1112) будет искомой.

В разделе 4.5 изложены основные свойства исчисления LR и его фрагментов:

Теорема 29. Класс Т^-языков совпадает с классом контекстно-свободных языков без пустого слова.

Теорема 30. Проблемы выводимости в исчислениях LR(\), LR и всех промежуточных фрагментах NP-полны.

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

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

[1] С. JI. Кузнецов. Об исчислении Ламбека с одним делением и одним примитивным типом, допускающем пустые антецеденты. Вестник Московского университета. Серия 1. Математика, механика. № 2, 2009. - С. 62-65.

[2] S. Kuznetsov. Lambek grammars with one division and one primitive type. Logic Journal of the IGPL. 20, No. 1, 2011. — P. 207-221.

[3] С. Л. Кузнецов. Об исчислении Ламбека с единицей и одним делением. Вестник Московского университета. Серия 1. Математика, механика. № 4, 2011. — С. 58—61.

[4] С. Л. Кузнецов. Исчисление Ламбека с операцией обращения. Деп. в ВИНИТИ 17.04.2012, № 152-В2012. - 17 с.

Отпечатано в отделе оперативной печати Геологического ф-та МГУ Тираж ¡00 экз. Заказ № ¡9