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

ФГБОУ ВПО «Московский государственный университет имени М. В. Ломоносова»

На правах рукописи

Сорокин Алексей Андреевич

Об отношении совместимости в исчислении Ламбека

и в его варианте с операциями замещения

01.01.06 — математическая логика, алгебра и теория чисел

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

0 4 СЕН 2014

Москва — 2014

005552108

Работа выполнена на кафедре математической логики и теории алгоритмов механико-математического факультета ФГБОУ ВПО «Московский государственный университет имени М. В. Ломоносова».

Научный руководитель:

Официальные оппоненты:

Ведущая организация:

Пентус Мати Рейнович,

доктор физико-математических наук, профессор.

Любецкий Василий Александрович,

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

Карлов Борис Николаевич,

кандидат физико-математических наук, доцент кафедры информатики (ФГБОУ ВПО «Тверской государственный университет»).

ФГАОУ ВПО «Уральский федеральный университет имени первого Президента России Б.Н.Ельцина».

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

Учёный секретарь диссертационного совета Д 501.001.84, созданного на базе ФГБОУ ВПО МГУ имени М. В. Ломоносова, доктор физико-математических наук, профессор Иванов Александр Олегович

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

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

Актуальность темы. Исчисление Ламбека L было введено И. Лам-беком в работе1 для формального описания синтаксиса естественных языков. Типы исчисления Ламбека строятся из счётного множества примитивных типов с помощью двуместных связок: умножения, а также левого и правого деления. Два типа А и В исчисления Ламбека называются совместимыми, если существует такой тип С, что обе секвенции А -» С и В —¥ С являются выводимыми. В этом случае тип С называется совмещающим для типов А и В. Отношение совместимости было впервые введено Ламбеком1, им было доказано, что оно является отношением эквивалентности.

М. Р. Пентусом2 был доказан критерий совместимости типов в исчислении Ламбека и коммутативном исчислении Ламбека, сформулированный в терминах интерпретаций типов исчисления Ламбека в свободной группе, порождённой примитивными типами. Позднее были получены критерии совместимости, для неассоциативного исчисления Ламбека NL3 и исчисления Ламбека-Гришина LG4. С лингвистической точки зрения совместимость типов означает возможность соединить соответствующие им языковые выражения с помощью сочинительного союза5.

XJ. Lambek. The mathematics of sentence structure // American Mathematical Monthly. — 1958 - Vol. 65, No. 3. — P. 154-170.

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

2М. Pentus. Equivalent types in Lambek calculus and linear logic // Серия математическая логика и теоретическая информатика, № 2 (препринт). — Математический институт им. В. А. Стеклова РАН, отдел математической логики. М., 1992. — 21 с.

3А. Foret. On the computation of joins for non-associative Lambek categorial grammars // 17th intemational workshop on unification, UNIF 2003, Proceedings / Editora J. Levy, M. Kohlhase, J. Niehren and M. Villaret. — Valencia: Universidad Politéchnica de Valencia, 2003. — Vol. 3. - P. 25-38.

4M. Moortgat, M. Pentus. Туре similarity for the Lambek-Grishin calculus // Proceedings of lítth Conference on Formal Grammar, Dublin, 2007. — P. 75-85.

5J. van Benthem. Language in Action: Categories, Lambdas and Dynamic Logic. —

В работах А. Форэ3'6 рассматривалось применение отношения совместимости для унификации и автоматического построения категориальных грамматик, основанных на исчислении Ламбека. Также построение совмещающего типа для заданных совместимых типов исчисления Ламбека является одним из этапов алгоритма приведения грамматики, основанной на исчислении Ламбека, к эквивалентной однозначной грамматике Ламбека7.

В работе показано, что для любых совместимых типов исчисления Ламбека найдётся совмещающий тип, чья длина ограничена квадратичным многочленом от длин исходных типов, и предложен алгоритм построения соответствующего типа. Кроме того, доказано, что данная квадратичная оценка является неулучшаемой с точностью до постоянного множителя: предъявлено семейство пар совместимых типов, содержащее пары типов сколь угодно большой длины, такое что для каждой из пар длина совмещающего типа ограничена снизу некоторым другим квадратичным многочленом. Также в диссертации исследуется отношение совместимости для исчисления Ламбека с операциями замещения8,9. Показано, что типы данного исчисления совместимы в том и только том случае, когда совпадают их интерпретации в свободной абелевой группе, порождённой примитивными типами.

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

Amsterdam: North-Holland,1991. — 350 p. — (Studies in Logic and the Foundations of

Mathematics; vol. 130).

eA. Foret. Conjoinability and unification in Lambek categorial grammars // New

Perspectives in Logic and Formal Lingusitics, Vth Roma Workshop, 2001, Proceedings / Editors V.M. Abrusci and C. Casadio. — Roma: Bulzoni, 2002.

7A. H. Сафиуллин. Выводимость допустимых правил с простыми посылками в исчислении Ламбека // Вестник Московского университета. Серия 1. Математика, механика. — 2007. — № 4. — С. 73-77.

®G. Morrill, J. М. Merenciano. Generalizing discontinuity // Traitement automatique des langues. — 1996. — Vol. 37, No. 2. — P. 119-143.

9G. Morrill, O. Valentin. On calculus of displacement // Proceedings of the 10th International Workshop on Tree Adjoining Grammars and Related Formalisms, New Haven, 2010. — P. 45-52.

Morrill. Categorial grammar: logical syntax, semantics and processing. — Oxford: Oxford University Press, 2011. nG. Morrill, O. Valentin,

M. Fadda. The displacement calculus // Journal of Logic, Language and Information. — 2011. — Vol. 20, No. 1. — P. 1-48.

позволяет хранить всю необходимую синтаксическую информацию в словаре, а также естественным образом комбинировать синтаксический и семантический анализ10,12. Кроме того, для синтаксического описания естественных языков традиционно используются порождающие грамматики, введённые Н. Хомским13. Наиболее важным классом порождающих грамматик являются контекстно-свободные грамматики, активно применяемые для задания синтаксиса языков программирования14.

Если рассматривать грамматики Ламбека только с точки зрения порождаемых ими языков, то как доказано М. Р. Пентусом15, всякий такой язык является контекстно-свободным. Из теоремы Пентуса и результатов Н. Гайфмана16 вытекает, что класс языков, порождаемых грамматиками, основанными на исчислении L, совпадает с классом контекстно-свободных языков без пустого слова. Хорошо известно, что контекстно-свободных грамматик недостаточно для полноценного анализа естественных языков12. Поскольку грамматики Ламбека порождают тот же класс языков, что и контекстно-свободные грамматики, рассматривались различные варианты их модификации. В частности, М. Канадзава17 предложил расширить исчисление Ламбека за счёт аддитивных связок для пересечения и объединения. В категориальных грамматиках зависимостей (categorial dependency grammars) А. Диковского и М. Дехтяря18 фрагмент исчисления Ламбека обогащается за счёт введения структуры зависимостей. Г. Моррилл и Х.-М. Меренсиано8 добавили к стандартным связкам исчисления Ламбека операции замещения, опускания и поднятия Полученное исчисление DL позволяет моделировать большинство известных непроективных синтаксических конструкций11. В диссертации доказано, что класс языков, задаваемых грамматиками, основанными на исчислении DL, является замкнутым относительно пересечения с автоматными

12М. Kracht. The Mathematics of Language. — Berlin: Mouton de Gruyter, 2003.

13N. Chomsky. Three models for the description of language // IRE Transactions on Information Theory. — 1956. — Vol. I T-2, No. 3. — P. 113-124.

Русский перевод: H. Хомский. Три модели описания языка // Кибернетический сборник, вып. 2. — М.: ИЛ, 1961. — С. 237-266.

14А. В. Ахо, Р. Сети, Дж. Д. Ульман. Компиляторы: принципы, технологии и инструменты. — М.: «Вильяме», 2001. — 768 с.

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

16Y. Bar-Hillel, С. Gaifman, Е. Shamir. On the categorial and phrase-structure grammars // Bulletin of the Research Council of Israel, Section F. — 1960. — Vol. 9F. — P. 1-16.

17M. Kanazawa. The Lambek calculus enriched with additional connectives // Journal of Logic, Language and Information. — 1992. — Vol. 1. — P. 141-171.

1SM. Dekhtyar, A. Dikovsky. Generalized categorial dependency grammars // Trakhtenbrot/Festschrift, Proceedings / Editors A. Avron et al. — Berlin etc.: Springer, 2008. — P. 230-255. — (Lecture Notes in Computer Science, Vol. 4800).

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

Цель работы.

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

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

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

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

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

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

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

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

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

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

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

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

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

Апробация диссертации.

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

• на семинаре «Алгоритмические вопросы алгебры и логики» под руководством академика РАН С. И. Адяна, Москва, Россия, 18 декабря 2012 года и 25 марта 2014 года;

• на Московских чтениях по конструктивной логике и представлению знаний, Москва, Россия, 30—31 мая 2012 года;

• на международной конференции «Мальцевские чтения», Новосибирск, Россия, 12—16 ноября 2012 года;

• на международной конференции «Теоретическая информатика в России» (Computer Science in Russia 2013), Екатеринбург, Россия, 24—29 июня 2013 года;

в на международной конференции «Формальные грамматики» (Formal Grammar 2013), Дюссельдорф, Германия, 10—11 августа 2013 года.

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

Структура диссертации. Работа состоит из введения, 6 глав, содержащих 23 раздела, предметного указателя и списка литературы. Библиография содержит 41 наименование. Текст диссертации изложен на 120 страницах.

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

Глава 1 имеет вспомогательный характер. В ней вводятся основные понятия, необходимые для дальнейшего изложения, а также формулируются известные ранее результаты. В разделе 1.1 приводится аксиоматика исчисления Ламбека Ь и простейшие свойства выводимости в данном исчислении. Счётное множество Рг = {рг,р2, ■ ■ •} называется множеством примитивных типов. Типы исчисления Ламбека строятся из примитивных типов с помощью бинарных связок \, / и •. Формально, множество типов Тр есть наименьшее множество, удовлетворяющее следующим условиям:

1. Рг с Тр;

2. если А,В е Тр, то (А\В), (В/А), (А-В)е Тр.

Примитивные типы обозначаются малыми латинскими буквами р, <7, г,..., возможно с нижними индексами. Для типов исчисления Ламбека используются большие латинские буквы А, В, С,____Конечные последовательности типов обозначаются греческими буквами Г, Д, П,____Выводимыми объектами исчисления Ь являются секвенции вида Г —> А, где Г является непустой последовательностью типов, а А является типом; Г именуется антецедентом, А — сукцедентом секвенции. Исчисление Ламбека Ь задаётся схемой аксиом А —> А, А е Тр и следующими правилами вывода:

ПА-» В ГВА-+С

П В/А" Г(В/А)ПД -> С ^

АП^В ГВА-+С П-> А

ГП(Л\В)Д->С Г-»Л Д->5 ТАВА-+С

ТА^А-В Г (А-В)Д->£Г

В разделе 1.2 определяется исчисление Ламбека Ь*, допускающее пустые антецеденты. В отличие от исчисления Ь, в исчислении Ь* антецедент может быть пустой последовательностью. Аксиомы и правила вывода исчислений Ь и Ь* совпадают.

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

через £*, элементы данного множества называются словами. Формальный язык есть произвольное множество слов Ь с Е*. На множестве формальных языков вводятся операции конкатенации: ■ Ь2 = {иь | и ~ 1<1,у £ Ь2}, и сопряжённые к ней операции левого и правого деления: Ьг/Ь2 = {и | {и} • Ь2 С Ьг} и Ь2\Ьг = {и | Ь2 • {и} С

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

Глава 2 посвящена доказательству верхней оценки на длину совмещающего типа в исчислении Ламбека Ь. Длиной типа А называется количество вхождений примитивных типов в Л, данная величина обозначается через 1(А). В разделе 2.1 вводится отношение совместимости в исчислении Ламбека, определяется понятие совмещающего типа и приводится критерий совместимости в исчислении Ламбека. Тип С € Тр называется совмещающим для типов А и В, если ЬЬА-4Си1Ь5-> С. В этом случае типы А и В называются совместимыми. Тип е Тр называется соединяющим для типов А и В, если В этом

случае типы А и В называются соединимыми. Как доказано И. Ламбе-ком1, типы исчисления Ламбека являются совместимыми тогда и только тогда, когда они являются соединимыми. Из этого следует, что отношение совместимости является эквивалентностью и более того, конгруэнцией на множестве Тр.

Через 0 обозначается свободная группа, порождённая примитивными типами, операция умножения в группе 0 обозначается через о. Интерпретацией типа А в группе 0 называется элемент [Л! е С?, определяемый правилами И = р, где р € Рг, [А-В} = Щ о ¡В], ¡А/В} = ¡А} о [В]"1,

Теорема 1 (М. Р. Пентус, 1992). 19 Следующие утверждения равносильны:

1. Типы А и В совместимы в исчислении Ь.

2. Типы А и В совместимы в исчислении Ь*.

3. И1 = щ.

В разделе 2.2 описывается алгоритм построения совмещающего типа. Вводится вспомогательный алфавит V = Рги{р | р е Рг]. Для каждого слова и) € V* вводится двойственное ему слово ги-1: р~1 = р, р-1 = р, (й1 ... ап) = а~1... а^1. После этого для каждого типа Л € Тр определяется его представление (Л) е V, задаваемое равенствами (р) = р, где р е Рг, {А - В) = (А)(В), (А/В) = (А)(В)-\ (В\А) = (В)~1(А). Также определяется обратное отображение ф: V* —> Тр по правилу ф{е) = д/д, где д — новый примитивный тип, ф(р) = р, ф(р) = (р\р/р), если р е

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

Рг, ф(аи) 1) = ф(а) • ф(и> 1), если а е 1 ф е,. При естественном отождествлении элементов р~1 и р данное отображение также определено и на группе 0.

Лемма 2.6. Типы А,ф((А)) и ф(\А\) являются совместимыми в исчислении Ь для любого А £ Тр.

На рисунке 1 приведена общая схема построения совмещающего типа С для заданных совместимых типов А и В. Здесь каждая стрелка обозначает выводимую секвенцию, через Ао и Во обозначены типы специального вида, такие что секвенции А —> Ао и В —Во являются выводимыми, а также верны равенства 1(Ао) = 1(А) и 1(В0) = 1(В).

А В

I I

Л0 ф({А)) 0([А1) ф((В)) В0 X У V Ч У х/

Л1 А2 В2 Вх

X ^ X ^

Аз ^ ^.Вз

с-

Рис. 1: Схема построения совмещающего типа С для заданных совместимых типов А и В.

Раздел 2.3 посвящён доказательству верхней оценки на длину совмещающего типа С. Для этого вначале строятся типы Ао,А\, А2,В0,В1 и В2, указанные на рисунке 1, и проводится непосредственная оценка их длины. После этого на основе соотношений на длину совмещающего и соединяющего типа доказывается искомая оценка на длину типа С. Теорема 2. Для любых совместимых в исчислении Ь типов А, В е Тр найдётся совмещающий тип С, такой что 1{С) ^ \{12{А) + 12(В)) + ^ (1(А) + 1(В)).

Доказанная оценка справедлива также для исчисления I/.

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

В разделе 3.1 вводится исчисление МСЬЬ, называемое мультипликативной циклической линейной логикой. Пусть Уаг = {р, д,...} — счётное множество переменных, в данном случае оно совпадает с множеством примитивных типов Рг. Атомами называются элементы множества А1 = Уаг и {р | р 6 Уаг}. Формулы линейной логики строятся из атомов

с помощью бинарных связок >5> (пар) и 0 (тензор), множество формул обозначается через Рт. Длиной формулы называется число вхождений атомов в неё, длина формулы Л обозначается через 1{А).

Для каждой формулы А е Рт определяется внешним образом её отрицание Лх: рх = р, (р)х = р, где р е Уаг, (В >9 С)х = Сх ®ВХ, (В®С)Х = Сх *3 В-1. Секвенции исчисления МСЬЬ имеют вид Г, где Г есть непустая последовательность формул. Исчисление задаётся аксиомами вида РР, V 6 Уаг и приведёнными ниже правилами вывода.

->Г АВА ->ГЛ

о тл И®)

-^Г(Л>$?В)Д^ °> ->Г(Л®В)Д

~»гд, ->г Л -»• ЛХД, г

^ДГ(го1^е) -=Ггд-М)

Понятие внешнего отрицания позволяет рассматривать в МСЬЬ и двусторонние секвенции, понимая запись Лх... Лт В1... Вп как другое обозначение секвенции Лх ... ... Вп. Выводимость секвенции ГчДв исчислении МСЬЬ обозначается МСЬЬ Ь Г -» Д. Переводом типа Л € Тр называется формула Л б Рт, задаваемая соотношениями р = р, если р е Рг, Л~В = А® В, А/В = А^В±, В\Л = Вх >9 А. Стандартным переводом секвенции Ах...Ап -» Выявляется секвенция Лх... Ап -»■ В, то есть односторонняя секвенция Лх... А^В. Теорема 4 (М. Р. Пентус, 1992). Исчисление МСЬЬ является консервативным расширением исчисления I/, то есть верна равносильность:

п Ь*оНоЛ1'''В ** МСЬЬ Ь Л! ... Л„ В.

а разделе 3.2 вводится отношение совместимости для исчисления

МСЬЬ. Формулы Л и В называются совместимыми, если существует формула С, такая что МСЬЬ 1- Л ->• С и МСЬЬ Ь В —► С. В этом случае формула С называется совмещающей для Л и В. Пусть д — свободная группа, порождённая множеством Уаг, тогда интерпретация формулы Л есть элемент [Л] е Я, задаваемый соотношениями |[р] = р, |р| = р-1, [Л® В! = [Л В] = [Л] о [¡В]]. Балансом ¿(А) формулы Л называется разность между числом вхождений паров и тензоров в Л.

Теорема 5. Формулы А, В е Рт совместимы в исчислении МСЬЬ тогда и только тогда, когда выполняются условия [Л1 = [В| и (¿(Л) = с1(В).

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

В разделе 3.3 вводится необходимое условие выводимости в исчислении MCLL, так называемые упрощённые сети доказательства. Если А

— формула, то её представляющее слово [Л] получается удалением из записи А всех скобок. Если Г = А\... Ап, то [Г] = o|\Ai] о... о \Ап], где о — новый символ, называемый ромбом. Элементами множества Пг являются пары {Sk,k), называемые вхождениями, где через Sf¡ обозначен к-й слева символ в записи [Т].

Отношение порядка ^г осуществляет сравнение таких пар по второму элементу, соответствующее отношение строгого порядка обозначается через <г- Если a,ß € fir, то 1п(а,/3) = {77 е fir | а < 77 < ß} U {77 € fir I ß < V < а}> a через 5r(a,ß) обозначается разность между суммарным числом паров и ромбов и числом тензоров в множестве ln(a,ß). Через 5г(а) обозначается соответствующая разность для множества вхождений связок в последовательность Г слева от вхождения а. Также используются обозначения Г2р4 — {(ir, к) \ (ir, к) € fir, ir е At}, = {<*,*) е fir}, Of = {(®,fc) € fir}, fi£ = {(o,fc)€fir}, а также =

Неориентированный граф G = (fir,£), где £ С fir х fir — симметричное бинарное отношение, называется <г-планарным, если для любых рёбер (ai,a2),(ßi,ß2) £ £ либо 1п(аьа2) Q In(/?i,/32), либо ln(ßi,ß2) С In(ai,a2), либо 1п(а1,аг) П In(/3i, /?г) = 0. Упрощённой сетью доказательства называется пара А/" = (fir,£), где £ — симметричное бинарное отношение, удовлетворяющая следующим условиям:

1. |fi^|-|fi®| =2,

2. £ задаёт разбиение множества fifi1 на пары, при этом в каждую пару входят элементы вида (р, к) и (р, I) для некоторой переменной р е Var.

3. V(a,/3) G £ (5r(ot,ß) = 1).

4. Ai является <г-планарным графом.

Следующая теорема следует из теоремы 7.12 работы20.

Теорема 6. Для всякой выводимой в MCLL секвенции Г существует упрощённая сеть доказательства, то есть можно найти отношение £ е fir4 х fir4» такое что граф J\f = {ПГ,£) будет упрощённой сетью доказательства.

Раздел 3.4 посвящён доказательству нижней оценки на длину совмещающей формулы С для совместимых формул А и В специального вида.

20М. Pentus. Free monoid completeness of the Lambek calculus allowing empty premises // Proceedings of Logic Colloquium '96, / Editors J. M. Larrazabal, D. Lascar and G. Mints.

— Berlin etc.: Springer, 1998. — P. 171-209. — (Lecture Notes in Logic, Vol. 12).

Через \А\п обозначается число вхождений атома 7г в формулу А. А называется тонкой, если для всех р £ Var верно, что |Л|Р ^ 1 и |Л|р ^ 1. Переменная р называется нейтральной для А, если \А\р = \А\? = 1. Если переменная р не является нейтральной для тонкой формулы А, но А содержит один из атомов р и р, то данный атом называется одиночным. Вхождение атома я- в тонкую формулу А обозначается через 7л (тг). Через D(A)

обозначается сумма £(|£а(7аОО>7а(р))| + 1), где суммирование ведётся р

по всем нейтральным для А переменным, таким что ¿д(7а(р), 7а(Р)) Ф 1. Если А и В образуют тонкую пару, через Е(А, В) обозначается сумма £(|5а(7а(тг)) - ¿в(7в(тг))| + 1), где суммирование ведётся по всем оди-

7Г

ночным атомам. Следующая лемма доказывается с использованием упрощённых сетей доказательства.

Лемма 3.11. Для любой тонкой пары совместимых формул А и В и любой формулы С, которая является совмещающей для А и В, выполняется неравенство 1(C) > D(A) + D(B) + Е(А, В).

Раздел 3.5 посвящён доказательству нижней оценки на длину совмещающей формулы в исчислении MCLL. Для этого для всех натуральных к строятся формулы Tfc, E/fc, являющиеся переводами некоторых типов исчисления Ламбека, такие что при любых к и I одинаковой чётности формулы Tfc и Щ являются совместимыми, а также удовлетворяют соотношению D(Tfc) ^ Щ- +1 - 5, D(U{) ^ ^ +1 - 5. Из существования тага« формул выводятся основные теоремы данной главы. Теорема 8. Для любых к и I одинаковой чётности найдутся такие совместимые формулы А и В исчисления MCLL длины к и I соответственно, что для всякой формулы С, которая является совмещающей для А и В, выполняется неравенство 1(C) > k + ^ — 9. Теорема 9. Для любых к и I одинаковой чётности найдутся такие совместимые типы Т и U исчисления L* (исчисления L) длины к и I соответственно, что для всякого типа С, который является совмещающим для Т и U, выполняется неравенство 1(C) > + ^ — 9.

Глава 4 содержит известные теоретические факты, касающиеся разрывных операций над языками и исчисления Ламбека с операциями замещения. В разделе 4.1 вводится исчисление Li, называемое исчислением Ламбека с единицей21, а также его несеквенциальная версия HLi. Типы данного исчисления строятся из элементов множества PrU {/}, где I Рг, с помощью бинарных связок •, \ и /. Исчисление HLi задаётся аксиомами

21 J. Lambek. Deductive systems and categories II: Standard constructions and closed categories // Category Theory, Homology Theory and Their Applications I / Editor P. Hilton. — Berlin: Springer, 1969. — P. 76-122. — (Lecture Notes in Mathematics, Vol. 86).

вида А А, и приведёнными ниже правилами вывода:

АС/В А - В -л С

А- В С А С/В

В А\С А - В —ь С

А - В С В А\С,

аксиомами для константы I:

A-I ■н- A, A<r* I ■ А, где запись В С означает, что обе секвенции В ->• С и С 5 являются аксиомами исчисления HLi, а также правилом транзитивности:

А-> Д В -» С А-+ С

Исчисление HLi является консервативным расширением исчисления L*, а именно, секвенция Aj.... Аг в, где г > 0, выводима в исчислении L* тогда и только тогда, когда секвенция А\ ■... • Аг -> В выводима, в исчислении HLi, а секвенция -4- В выводима в исчислении L* тогда и только тогда, когда секвенция / В выводима в исчислении HLi. В разделе 4.2 вводятся так называемые разрывные операции над языками. Обозначим Ei = Е U {1}, где 1 ^ Е — выделенный разделитель. Для каждого слова w е EJ его сорт s(w) равен |u>|i, то есть числу вхождений разделителя в w. На множестве Ei для всякого целого положительного j вводится частичная бинарная операция j-замещения Qj, состоящая в замене j-го слева разделителя в первом аргументе данной операции на её второй аргумент. В случае если первый аргумент операции ©¿ содержит менее j разделителей, результат её применения не определён. Также определяются бинарные операции 4-,,, Li ^ Ь2 = {w е EJ | Vwi G Li (wi Qj w £ L2)}, Li tj L2 = {w € EJ I Viü2 € L2 (w Qj W2 6 Li)}. Таким образом, операции Qj, tj и ij для всякого j представляют собой разрывный аналог операций

В разделе 4.3 определяется исчисление HDL, называемое исчислением Ламбека с операциями замещения, введённое О. Валентином в 2012 году22. Оно эквивалентно введённому в 1996 году исчислению DL8. Пусть Рг£> — счётное множество примитивных типов, на котором задана функция сорта s: Ргд —¡> N, где через N обозначено множество натуральных чисел. Кроме того, пусть выделены два элемента I, J £ Ргр, тогда множество Base = Ргр U {I, J} называется множеством базовых типов; функция s доопределяется на всём множество Base с помощью равенств s(I) = 0 и s(J) = 1. Множество TpD типов исчисления Ламбека с операциями

220. Valentin. Theory of discontinuous Lambek calculus: PhD Thesis. — Universität Autónoma de Barcelona, Barcelona, 2012.

замещения строится из базовых типов с помощью связок а также

счётного семейства бинарных связок |fc, 4*, где к £ N, к ^ 1 и задаётся следующим определением:

1. Если ДВе Трд и s(A) ^ s(B), то (А/В),{В\А) € Трс, причём s{A/B) = s(B\A) = s{A) - s(B).

2. Если A, Be Трд, то (А - В) € Трв, причём s(A ■ В) = s(A) + s(B).

3. Если A,Be TpD и s(B) ^ 1, в(Л) ^ s(B) - 1, к ^ s(B), то BUAe Tp^, причём s{B U А) = s(A) - s(B) + 1.

4. Если A, Be TpD и s(A) > s(B), к ^ s(A) - s(B) + 1, то (A tk В) е TpD, причём s(A tк В) = s(A) - s(B) + 1.

5. Если А, В € Трр и s(A) ^ 1, к < в(Л), то (Л 0fc В) е TpD, причём s(A Qk В) = а(А) + а(В) - 1.

Секвенциями исчисления HDL являются выражения вида А—> В, такие что А, В е TpD и s(A) — s(B), выводимость секвенции А -¥ В обозначаются через HDL I- А —> В. Аксиомы исчисления HDL имеют вид А —> А, А 6 TpD, ниже приведены правила вывода для связок: Л —» С/В А-В^С

А - В С А -> С/В

В-+А\С А - В С

А-В-+С В А\С

A^CtjB A ©j В С

A Oj В С ~А~ТС\~В

В AС AQjB-^C

AQjB С В AljC

структурные постулаты, включающие в себя аксиомы для констант: А • I А, А ++ I • А, J ©1 А -н- А, А <-> A Qj J, если j ^ з(Л), аксиомы ассоциативности для мультипликативных связок: [А-В)-С ++ А-(В-С), (A ©i В) Qj С (Л ©j С) ©i+i(B)-i если j < г, (Л ©j В) Qj С -н- AQj (B©j_i+i С), если г ^ j < i + s(B), (A Qi В) Qj С (Л ©л-+1_в(в) С) ©i В, если г + s(B) ^ j, аксиомы взаимодействия между «непрерывными» и «разрывными» связками:

А-В (Л • J) 0,(Л)+1 В, А ■ В о (J ■ В) Qi Л

и правило транзитивности:

Исчисление HDL является консервативным расширением исчисления HLi- Через Tpfc обозначается множество типов, получающееся при ограничении максимального сорта подтипов числом к. Исчисление, получаемое из HDL запретом типов не из ТрА, обозначается через HDLfc. Все такие исчисления являются консервативными расширениями исчисления HLj.

В разделе 4.4 вводятся языковые модели для исчисления Ламбека с операциями замещения.

В главе 5 доказывается критерий совместимости для исчисления Ламбека с операциями замещения. В разделе 5.1 вводится отношение совместимости для исчисления HDL и понятие интерпретации в свободной абелевой группе для типов данного исчисления. Понятия совместимости и совмещающего типа аналогичны соответствующим понятиям для исчисления L. Как и ранее, отношение совместимости является конгруэнцией на множестве типов.

Пусть а £ Ргд — новый элемент, a F — свободная абелева группа, порождённая множеством Pro U {а}, тогда для каждого типа Л € TpD определяется его интерпретация [Л]:

1- И =Р, если р € Prfc,

2- 1П = е,

3. [JJ = а,

4. [Л • В] = [ЛJ о Щ,

5. [А/В1 = [В\А1 = [Л1о1В1-1,

6. [Л ©J BJ = [Л] о а-1 о IB] для любого j < к,

7. {В ij Л] = |Л Т,- В} = Щ о а о Щ -1 для любого j ^ к.

Также в данном разделе доказывается, что равенство [Л] = [В| является необходимым условием совместимости типов А и В.

В разделе 5.2 доказывается, что равенство интерпретаций является достаточным условием и, следовательно, критерием совместимости в исчислении HDL, а также в его фрагментах HDLfc. Для этого доказывается несколько вспомогательных утверждений о совместимости конкретных типов, после чего исследуемая проблема сводится к соответствующей проблеме для типов специального вида, содержащих только примитивные типы сорта 0 и связки ■ и /. Для доказательства критерия совместимости строится гомоморфизм из свободной абелевой группы, порождённой примитивными типами, в группу классов эквивалентности по отношению совместимости, данный метод впервые применялся в 2. Теорема 11. Типы А, В € Трк совместимы в исчислении HDLfc тогда и только тогда, когда ([Л] = [В].

Теорема 12. Типы А, В £ Tpfc совместимы в исчислении HDL тогда и только тогда, когда [Л] = [В].

Глава 6 посвящена грамматикам, основанным на исчислении Ламбе-ка с операциями замещения. В ней доказывается, что порождаемый ими класс языков замкнут относительно пересечения с автоматными языками, не содержащими пустого слова. В разделе 6.1 вводится секвенциальная версия исчисления HDL, обозначаемая через DL8'9. Пусть через Tp'D обозначено множество типов, имеющих сорт г, а [] — новый символ, называемый разделителем. Множество атомарных конфигураций есть наименьшее множество слов в алфавите TpD U {0, {, }.;}, удовлетворяющее условиям:

1. [] является атомарной конфигурацией.

2. Любой тип Л 6 Тр^ является атомарной конфигурацией.

3. Для любого г > 0, любого типа А е Тр^ и любого конечного набора слов Гх,... ,Г,, каждое из которых является конкатенацией конечного числа атомарных конфигураций, выражение Л{Гх;... ;Г*} является атомарной конфигурацией.

Конфигурациями называются конечные слова, составленные из атомарных конфигураций. Конфигурации обозначаются большими греческими буквами Г,Д,..., возможно с нижними индексами, а всё множество конфигураций — через О. Пустая конфигурация обозначается через Л. На конфигурации естественным образом продолжается функция сорта s, определяемая следующим образом:

1. 5 (Л) = О,

2- *([]) = 1,

3. s(A) = 0, если А е Тр%,

4. в(Л{Г1;...;Г<}) = в(Г1) + ... + в(Г1),

5. в(Гх... Гг) = в(Гх) +... + «(Гг), где Гь..., Гг — атомарные конфигурации.

Для каждой конфигурации определяется её представляющий тип т(Г), при этом s(r) = s(r(r)).

1- т(0) = J,

2. т(А) = А, если А е Тр£,,

3. т(Л{Г1;... = (... (Л 04 т(Г<))... ©2 т(Г2)) ©i r(Ti).

4. т(Гх... Г;) = г(Гх) •... ■ т(Г*), если Г1;..., Г^ — атомарные конфигурации.

Выводимыми объектами исчисления DL являются секвенции вида Г —> А, где Г G О, А е TpD, s(r) = в(Л). При этом данное исчисление эквивалентно исчислению HDL, то есть DL I- Г —> А HDL Н т(Г) Л. В дальнейшем в данной главе рассматривается именно исчисление DL.

В разделе 6.2 вводится понятие категориальной грамматики, основанной на исчислении Ламбека. Грамматикой Ламбека или L-грамма-тикой называется тройка Q = (£, >,#), где Е — конечный алфавит, >

— конечное подмножество декартова произведения Е х Тр, а Я е Тр — целевой тип. Язык L(Q), задаваемый грамматикой Q, равен

L{G) = {ai... Or | ЗЛЬ. ..Ar((\/j{aj > Aj)) Л L h Л1... Лг Я)}, где запись aj > Aj означает (a,j,Aj) € >. Если заменить в данном определении исчисление L на L*, получится определение Ь*-грамматики. L-грамматиками порождаются в точности все контекстно-свободные языки без пустого слова15'16, а L'-грамматиками — все контекстно-свободные языки15,23.

В дальнейшем рассматриваются грамматики, основанные на исчислении DL9'11. Разрывной грамматикой Ламбека или DL-грамматикой называется тройка Q = {£,[>,Я), где Е — конечный алфавит, о — конечное подмножество декартова произведения £ х Трд, а Я € Tp°D — целевой тип. Язык L(Q) определяется аналогично случаю L-грамматики.

При замене исчисления DL на его фрагмент DLfc получается определение DLfc-грамматики. Известно9, что уже DL:-грамматиками порождаются некоторые языки, не являющиеся контекстно-свободными, в частности, все языки, представимые в виде замыкания автоматного языка относительно перестановки букв в словах.

В разделе 6.3 вводятся понятия конечного автомата и автоматного языка. Конечным автоматом называется кортеж М — (Е, Q, A, qs,F), где Е — конечный алфавит, Q — конечное множество состояний, Д С Q х £* х Q — конечное множество переходов вида (qi,w) —> q2, где w называется меткой перехода, qs е Q — стартовое состояние, a F С Q

— множество завершающих состояний. Конфигурацией конечного автомата называется пара (д, го), q 6 Q,w € £*. Множество конфигураций автомата М обозначается через См■ Отношением достижимости в автомате М называется наименьшее рефлексивное транзитивное отношение -»•мё См х См, такое что для каждого перехода {(q\,u) q2) € А и произвольного слова в£Е выполняется соотношение (qi,uv) —>м (Q2,v). Язык L(M), задаваемый автоматом, состоит из всех слов w, таких что существует завершающее состояние q е F, удовлетворяющее соотношению (qs,w) ->м (q, е). В случае если автоматный язык не содержит пустого слова, его можно задать конечным автоматом с однобуквенными метками перехода и одним завершающим состоянием.

В разделе 6.4 описывается алгоритм построения DL-грамматики для пересечения языка, задаваемого DL-грамматикой, с автоматным языком. Пусть язык L задан DL-грамматикой Q = <£, >,Я), a LR — автоматный язык, не содержащий пустого слова. Можно считать, что LR задаётся

23S. Kuznetsov. Lambek grammars with one division and one primitive type // Logic

Journal of the IGPL. — 2012 — Vol. 20, No. 1 — P. 207-221.

конечным автоматом М = (Е, Q, Д, qs, {qf}} с одним завершающим состоянием. Будем считать, что все элементы множества Q принадлежат множеству Рг и имеют сорт 0, при этом они не используются при построении типов грамматики д. Через Q' — (£, >',Я') обозначается новая DL-грамматика, где Я' = (qs \ Н) • qf, а словарь >' определяется как >' = {(a,(Qi\A)-q2) I а>А, ({qua) q2) £ Д}.

В разделе 6.5 доказывается, что введённая грамматика действительно задаёт язык LDLr. Пусть Т — множество типов, не содержащих примитивных типов из множества Q = {qx,..., qn}. Если Т € Т, то через T-j обозначается тип (qt \Т) • qj, также используется обозначение Tii0 = дг \Т. Через 0(Т') обозначается множество конфигураций, содержащих только типы из множества Т' = {Titj \ г > 0, j ^ 0} U Т U О. Секвенция Г -> А называется Т'-секвенцией, если Г е 0(Т') и А еТ'.

Для каждой атомарной конфигурации Г е 0(Т') вводится слово (Г)т в алфавите Q U {g7 | gj 6 Q}, называемое её д-образом:

1. (А), = (Q), = е,

2- (qi)q = дь_если g* € Q,

3. (Tij)q = QiQj, если s(Tid) = 0,

4. (ЗДГ^.. ;ГР}), = ©¿(ГО, ... (rr),eif

где Qj = qj,Qj = q} при j > 0 и ©0 = — Л (Л обозначает пустую последовательность), g-образ (Г), конфигурации Г равен конкатенации q-образов входящих в неё атомарных конфигураций. Определение д-образа продолжается на Т'-секвенции по правилу (Г Т, j)q = ©¿(Г)90,-, (Г

Qi), = (г),е4.

Пусть фиксированы п букв bi,...,bn, именуемые открывающими скобками, а также п соответствующих им закрывающих скобок Ь1,... ,Ьп и В = {£>1, i>i,..., bn,bn}. Правильной скобочной последовательностью ранга п называется всякое слово w 6 В*, которое может быть сокращено до пустого последовательным вычёркиванием подслов вида bjbi, где i ^ п.

В данном разделе доказывается, что g-образ выводимой секвенции является правильной скобочной последовательностью. Отсюда следует, что выводимость секвенции A\uh .. .ATir ^r ->■ HMiin для неотрицательных io,jo,...,ir,jr равносильна одновременному выполнению условий DL h А1 ...Ат —> Я и j0 = ¿1,... ,jr-i = ir, jr = i0. Следовательно, грамматика Q' действительно порождает язык L(Q) П Ьц и верна следующая теорема:

Теорема 15. Множество языков, распознаваемых T)L-грамматиками, замкнуто относительно пересечения с автоматными языками, не содержащими пустого слова.

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

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

[1] А. А. Сорокин. О длине совмещающего типа в исчислении Ламбе-ка // Вестник Московского университета. Серия 1. Математика, механика. — 2011. — № 3. — С. 10-14.

[2] A. Sorokin. Lower and upper bounds for the length of joins in the Lambek calculus // Proceedings of 8th Computer Science Symposium in Russia, CSR 2013 / Editors A. Bulatov and A. Shur. — Berlin: Springer, 2013. — P. 150-161. - (Lecture Notes in Computer Science, Vol. 7913).

[3] A. Sorokin. On the generative power of discontinuous Lambek calculus // Proceedings of 17th and 18th International Conferences, FG 2012, FG 2013 / Editors G. Morrill and M.-J. Nederhof. - Berlin: Springer, 2013. - P. 250-262. - (Lecture Notes in Computer Science, Vol. 8036).

[4] A. Sorokin. Conjoinability relation in 1-discontinuous Lambek calculus // Categories and Types in Logic, Language, and Physics / Editors C. Casadio, B. Coecke, M. Moortgat and P. Scott. — Berlin: Springer, 2013. — P. 392-401. - (Lecture Notes in Computer Science, Vol. 8222).

Отпечатано в отделе оперативной печати Геологического ф-та МГУ Подписано в печать «2 О» [¿ЮНА^ 2014 г. Тираж¡СОэкз. Заказ №