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

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

МЕХАНИКО-МАТЕМАТИЧЕСКИЙ ФАКУЛЬТЕТ

pre оя

1 г & Г,Г;

На правах рукописи УДК 510.64+519.766.2

ПЕНТУС МАТИ РЕЙНОВИЧ ПОЛНОТА ИСЧИСЛЕНИЯ ЛАМБЕКА

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

Автореферат

диссертации на соискание учёной степени доктора физико-математических наук

Москва — 2000

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

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

профессор А. В. Михалёв

— доктор физико-математических наук, В. П. Оревков

— доктор физико-математических наук, профессор А. Л. Семёнов

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

Защита диссертации состоится 2000 г. в

16 ч. 15 мин. на заседании диссертационного совета Д.053.05.05 при Московском государственном университете им. М. В. Ломоносова по адресу: 119899, ГСП, Москва, Воробьёвы горы, МГУ, механико-математический факультет, аудитория 14-08.

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

Автореферат разослан «

Учёный секретарь диссертационного совета

Д.053.05.05 при МГУ

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

профессор

¿1/1 а ее, о

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Категориальная грамматика — раздел математической лингвистики, описывающий формальные законы синтаксических категорий в естественных и искусственных языках. Одно из центральных мест в нём занимает исчисление Ламбека, которое было введено в статье [1] для изучения свойств формальных языков. Формальным языком называется произвольное множество непустых слов (конечных последовательностей символов) над некоторым конечным алфавитом. В лингвистических приложениях при описании синтаксиса естественного языка алфавитом (в математическом смысле) является множество всех словоформ рассматриваемого фрагмента естественного языка. При этом множество всех грамматически правильных предложений образует формальный язык. Другие важные примеры формальных языков над тем же алфавитом — множество всех именных групп, множество всех групп сказуемого и т. д.

Исчисление Ламбека описывает свойства трёх бинарных операций над формальными языками: операции умножения, операции правого деления и операции левого деления (эти операции обозначаются соответственно • , / и \). Произведение языков состоит из всевозможных попарных конкатенации их элементов. Результат правого деления языка А на В (обозначается А/В) определяется как множество всех таких непустых слов у, что {-у}*В С А. Результат левого деления языка А на В (обозначается В\А) определяется как множество всех таких непустых слов 7, что В*{7} С А.

Исчисление Ламбека описывает утверждения вида А С В, где А п В — термы, составленные из переменных по формальным язы-

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

кам с помощью операций \ и /. Аксиомы и правила этого исчисления утверждают, что

1) отношение С рефлексивно и транзитивно,

2) умножение ассоциативно,

3) С С А/В тогда и только тогда, когда С* В С А,

4) С С В\А тогда и только тогда, когда В*С С А.

Для описания синтаксиса естественных языков Бар-Хиллел в 1950-х годах ввёл понятие базовой категориальной грамматики (см. [2]). Каждая базовая категориальная грамматика приписывает словоформам рассматриваемого фрагмента естественного языка термы, составленные с помощью операций \ и "/•' Содержательно каждый такой терм служит обозначением для Некоторой синтаксической категории, т. е. некоторого класса словоформ и словосочетаний с одинаковой синтаксической сочетаемостью. В грамматике выделен один терм (обычно он обозначает класс всех грамматически правильных предложений). Последовательность словоформ допускается данной грамматикой, если соответствующую последовательность термов можно сократить так, что останется только выделенный терм. При этом разрешается сократить соседние термы А/В и В (получается А), а также В и В\А (тоже получается А).

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

В конце 50-х — начале 60-х годов возник вопрос о связи категориальных грамматик (в том числе грамматик Ламбека) с

[2] Bar-Hillel Y. A quasi-arithmetical notation for syntactic description // Langugage. — 1953. — Vol. 29. — P. 47-58.

иерархией порождающих грамматик Хомского, включающей четыре вложенных друг в друга класса: порождающие грамматики (самый большой класс), грамматики непосредственно составляющих, контекстно-свободные грамматики и автоматные грамматики. В 1960 году Бар-Хиллел, Гайфман и Шамир доказали, что формальный язык может быть задан некоторой базовой категориальной грамматикой тогда и только тогда, когда он является контекстно-свободным, т. е. может быть задан некоторой контекстно-свободной грамматикой (см. [3]). Они высказали гипотезу, что то же самое имеет место для грамматик Ламбека (см., например, [4]). Доказательство одной половины этой гипотезы (а именно того, что любой контекстно-свободный язык задаётся некоторой грамматикой Ламбека) фактически совпадает с соответствующим доказательством для базовых категориальных грамматик. Вопрос об обратном включении оставался открытым в течение многих лет. В. Бушковским были получены частичные результаты, относящиеся к фрагменту без правого деления и умножения и к фрагменту без умножения с некоторым ограничением на вложенность разносторонних делений (см. [5, 6]). Положительный ответ для

[3] Bar-Hillel Y., Gaifman C., and Shamir E. On categorial and phrase-structure grammars // Bull. Res. Council Israel Sect. F. — 1960. — Vol. 9F. — P. 1-16.

[4] Chomsky N. Formal properties of grammars // Handbook of Mathematical Psychology / Editors R. D. Luce et al. — New York: Wiley, 1963. —• Vol. 2. — P. 323-418.

[5] Buszkowski W. The equivalence of unidirectional Lambek categorial grammars and context-free grammars // Zeitschrift für mathematische Logik -und Grundlagen der Mathematik. — 1985. — Vol. 31. — P. 369-384.

[6] Buszkowski W. On generative capacity of the Lambek calculus // Logics in AI: European Workshop JELIA '90. Amsterdam, The Netherlands, September 1990. Proceedings / Editor J. van Eijck. — Berlin etc.: Springer-Verlag, 1991. — P. 139-152. — (Lecture Notes in Computer Science; Vol. 478. Lecture Notes in Artificaial Intelligence).

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

Некоторые современные приложения исчисления Ламбека к изучению естественных языков приводятся в книгах [8, 9, 10].

С исчислением Ламбека связаны и другие нетривиальные математические проблемы. Ряд вопросов касается интерпретации исчисления Ламбека на различных математических структурах (см. обзорные статьи [11, 12]).

Наиболее широкий класс интерпретаций исчисления Ламбека образуют полугруппы с делением. Полугруппой с делением называется полугруппа (Н, ♦), рассматриваемое вместе с частичным порядком причём для любых элементов а,Ь £ Н существует такой элемент а/Ь 6 Н (правое частное элемента а по 6), что условия х а/6 и х»Ь ^ а эквивалентны, и существует такой элемент Ь\а £ Н (левое частное элемента а по Ь), что условия х ^ Ь\а и Ь»х ^ а эквивалентны

[7] Пентус М. Р. Исчисление Ламбека и формальные грамматики,-. Дис. ... канд. физ.-мат. наук: 01.01.06. —■ Защищена 01.03.1996; Утв. 14.06.1996; 01910048811. — М., 1996. — 69 с. — Би-блиогр.: с. 67-69.

[8] Categorial Grammars and Natural Language Structures / Editors R. T. Oehrle, E. Bach, and D. Wheeler. — Dordrecht: Reidel, 1988.

[9] Moortgat M. Categorial Investigations. Logical and Linguistic Aspects of the Larnbek Calculus: Ph.D. thesis. — Dordrecht: Foris, 1988. — XVII, 270 p.

[10] Carpenter B. Type-Logical Semantics. — Cambridge etc.: The MIT Press, 1997. — XXI, 575 p. — (Language, Speech, and Communication) .

[11] Dosen К. A brief survey of frames for the Larnbek calculus // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. — 1992. — Vol. 38, no. 2. — P. 179-187.

[12] Ono H. Semantics for substructural logics // Substructural Logics / Editors К. Dosen and P. Schroeder-Heister. — Oxford: Clarendon Press, 1993. — P. 259-291. — (Studies in Logic and Computation; 2).

(см. [13]). В некоторых работах вместо а/Ь пишут а:Ь, а вместо Ь\а пишут а::Ь.

Интерпретация исчисления Ламбека в полугруппе с делением Н задаётся произвольной функцией V, ставящей в соответствие примитивным типам элементы Н. Интерпретирующая функция V продолжается естественным образом па все типы. Утверждение А —► В является истинным при данной интерпретации, если *(А) ^ v{B). ^

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

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

К. Дошен рассмотрел следующую конструкцию. Частично упорядоченной полугруппой называется такая полугруппа с частичным порядком, где полугрупповая операция монотонна. Множество всех таких подмножеств Л частично упорядоченной полугруппы <7, что из а ^ Ь и 6 £ А следует а £ А, является полугруппой с делением относительно порядка С и операции

А*В {с £ С | с аЬ для некоторых а £ А, Ь £ В}.

В 1985 году К. Дошен [14] доказал полноту исчисления Ламбека относительно моделей на таких полугруппах с делением.

[13] Fuchs L. Partially Ordered Algebraic Systems. — Oxford: Perg-amon Press, 1963. — Русский перевод: Фукс Л. Частично упорядоченные алгебраические системы / Пер. с англ. И. В. Стеллецкого. — М.: Мир, 1965. — 342 с.

[14] Dosen К. A Completeness Theorem for the Lambek Calculus of Syntactic Categories // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. — 1985. — Vol. 31. — P. 235-241.

В 1986 году В. Бушковский [15] опубликовал доказательство полноты относительно ещё более узкого класса моделей исчисления Ламбека. Он рассматривал в качестве полугруппы с делением множество всех подмножеств произвольной полугруппы С. При этом в качестве, порядка снова использовалось отношение С, а в качестве операции умножения — операция «, определяемая так:

А»В ^ {аЬ | а € Л, Ь € В}.

Такие полугруппы с делением представляют частный случай полугрупп С'делением, рассмотренных Дошеном (достаточно на С в качестве отношения частичного порядка ввести отношение равенства). Таким образом, результат Вушковского сильнее результата Дошена.

Особый интерес представляют модели исчисления Ламбека на множестве подмножеств свободной полугруппы (частный случай моделей, рассмотренных Бушковским). Эти модели обычно называются языковыми моделями исчисления Ламбека или Ь-моделями, так как в них •, \ и / обозначают умножение, левое деление и правое деление формальных языков, определённые на стр. 1. Именно эта интерпретация рассматривалась в 1958 г. при формулировке исчисления Ламбека. Корректность исчисления Ламбека относительно Ь-моделей следует непосредственно из корректности относительно интерпретаций в полугруппах с делением. Вопрос о полноте относительно Ь-моделей долгое время оставался открытым (см., например, [6, 11, 15, 16, 17]). Конструкция Бушковского непригодна для доказательства полноты относительно Ь-моделей, так как согласно этой конструкции по невыводимой секвенции строится контрмодель

[15] Buszkowski W. Completeness Results for Lambek Syntactic Calculus // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. — 1986. — Vol. 32. — P. 13-28.

[16] Zielonka W. Axiomatizability of Ajdukiewicz-Lambek calculus by means of cancellation schemes // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. — 1981. — Vol. 27, no. 3. — P. 215-224.

[17] ßenthem J. van. Language in Action: Categories, Lambdas and Dynamic Logic. — Amsterdam etc.: North-Holland, 1991. — X, 350 p. — (Studies in Logic and the Foundations of Mathematics; Vol. 130).

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

В данной диссертации дан положительный ответ на вопрос о полноте исчисления Ламбека относительно Ъ-моделей. Более того, доказано, что исчисление Ламбека полно относительно класса всех Ь-моделей на двухбуквенном алфавите, т. е. для каждого невыводимого утверждения А В, где А а В — типы исчисления Ламбека, найдётся некоторая интерпретирующая функция и, ставящая в соответствие примитивным типам множества слов в двухбуквенном алфавите, такая что у(А) % у(В).

Во многих работах изучается также другой частный случай моделей исчисления Ламбека на полугруппах с делением — реляционные модели (см. [18, 19]). Мы рассматриваем бинарные отношения как множества упорядоченных пар. Композицией (или произведением) бинарных отношений А и В называется бинарное отношение {{г, ^ | (г,э) £ А и € В для некоторого $}. Пусть 5 — строгий частичный порядок на некотором множестве. Множество всех подмножеств 5 с определёнными на нём операцией композиции и отношением С образует полугруппу с делением. Интерпретация исчисления Ламбека в любой такой полугруппе называется реляционной моделью исчисления Ламбека или И-моделью.

С. Микулаш доказал в 1992 году (см. [20]), что исчисление Ламбека полно относительно реляционных моделей. Возник вопрос

[18] Benthem J. van. Semantic parallels in natural language and computation. — Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1988. — 45 p. — (ILLC Prepublication Series; LP-88-06),

[19] Orlowska E. Relational interpretation of modal logics // Polish Acad. Sci. Inst. Philos. Sociol. Bull. Sect. Logic. — 1988. — Vol. 17, no. 1. — P. 2-14.

[20] Mikulas Sz. The Completeness of the Lambek Calculus with respect to Relational Semantics. — Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1992. — 21 p. — (ILLC Prepublication Series; LP-92-03).

об усилении этого результата путём указания какого-нибудь конкретного простого отношения строгого частичного порядка, относительно R-моделей на котором исчисление Ламбека было бы полно. В данной диссертации доказано, что в качестве такого отношения подходит обычный строгий линейный порядок на целых числах.

Операции умножения и делений, обладающие свойствами, описываемыми исчислением Ламбека, встречаются в различных областях алгебры. Например, на множестве всех двусторонних идеалов произвольного ассоциативного кольца R можно рассмотреть операции ♦ , \ и / (обычно вместо \ и / пишут ' . и . '), определённые следующим образом (см. [21]):

п

А»В состоит из всех конечных сумм где а; £ Л и 6; £ В;

>'=1

А\В =± {г £ R | Ar С 5}; А/В ^ {г € R | rB Ç А}.

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

Аналогичные операции на различных решётках с делением рассматриваются в монографии [22], где Г. Биркгоф приводит ряд утверждений, фактически являющихся теоремами исчисления Ламбека.

[21] Lambek J. Lectures on Rings and Modules. — Waltham, Massachusetts, etc.: Blaisdell, 1966. — Русский перевод: Ламбек И. Кольца и модули / Пер. с англ. А. В. Михалёва. — М.: Мир, 1971. — 280 с.

[22] Birkhoff G. Lattice Theory. — Providence, Rhode Island, 1967. — Русский перевод: Биркгоф Г. Теория решёток / Пер. с англ. В. Н. Салия. — М.: Наука, 1984. — 568 с.

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

Методы исследования. В диссертации использованы теоретико-доказательственные методы (устранение сечения в секвенциальных исчислениях) и комбинаторные методы.

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

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

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

Работа носит теоретический характер. Её методы и результаты могут быть полезны специалистам Московского, государственного университета им. М. В. Ломоносова, Санкт-Петербургского государственного университета, Новосибирского государственного университета, Красноярского государственного университета, Тверского государственного университета, Математического института им. В. А. Стеклова РАН, Санкт-Петербургского отделения Математического института им. В. А. Стеклова РАН.

Апробация работы. Основные результаты, полученные в диссертации, докладывались на общемосковском научно-исследовательском семинаре по математической логике (руководители семинара — чл.-корр. РАН С. й. Адян, проф. В. А. Успенский), на семинаре («Логические проблемы информатики» (руководитель семинара — проф. С. Н. Артёмов), на заседании Московского математического общества и на международных конференциях в России, Швейцарии, Франции, Израиле и Испании.

Публикации. Результаты диссертации опубликованы в 11 работах, перечисленных в конце автореферата.

Структура и объем работы. Диссертация состоит из введения и 10 глав. Текст диссертации изложен на 165 страницах. Список литературы содержит 58 наименований.

СОДЕРЖАНИЕ РАБОТЫ

Во введении даётся обзор результатов по исследуемой проблеме и кратко формулируются основные результаты диссертации.

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

Отрезок множества целых чисел где р £ X и } £ 2,

состоит из всех таких целых чисел х £ Ъ, что р ^ х д.

Пусть V — некоторый алфавит. Через V* обозначается множество всех слов в алфавите V, включающее пустое слово. Множество всех непустых слов в алфавите V обозначается через V"*". Длина слова а обозначается |а|.

Под свободной полугруппой будем понимать множество всех непустых слов некоторого алфавита. При этом полугрупповой операцией является операция конкатенации (т. е. склеивания) слов.

Множество всех подмножеств произвольного множества XV обозначим через ^Р(ЛУ).

Типы исчисления Ламбека определяются следующим образом. Предполагаем, что задано счётное множество {р1,р2,рз, ■ ■ •}, элементы которого будем называть примитивными типами. Типы исчисления Ламбека строятся из примитивных типов с помощью трёх бинарных связок /. Обозначим множество всех типов,' построенных таким образом, через Тр. Прописные буквы латинского алфавита будем использовать для обозначения типов исчисления Ламбека, а прописные греческие буквы — для обозначения конечных (не обязательно непустых) последовательностей типов. Символ Л будет всегда обозначать пустую последовательность типов. Иногда будем писать А\* ... *Ап вместо (... (Аг'Аг)*... *АП).

В статье [1] И. Ламбек ввёл два дедуктивно эквивалентных друг другу исчисления (мы будем обозначать их Ьн и Ь). Выводимыми объектами исчисления Ьн являются записи вида А—> В. Аксиомы имеют вид А А, (А.*В)»С -»■ А*(В*С) и А»(В*С) (А*В)*С. Выводы строятся с помощью следующих правил:

А*С —В С А\В

С ->■ А\В А*С-> В

А~> В В-+С А-+ С

С»А-> В С В/А

С В/А С*А В

Рассмотрим теперь исчисление Ь. Выводимыми объектами этого исчисления являются записи вида Аг... Ап —>• В, где п ^ 1 (такие записи называются секвенциями). Интуитивно Ах ... Ап —> В означает то же, что и Ах * ... *Ап —> В.

Аксиомы исчисления Ь имеют вид А —А. Выводы строятся с помощью следующих правил:

АП

П-+ А\В

(-> \), где П^Л,

П->А ГДД->С ГП(А\В)Д С

ПА-» В П В/А

Гч Л А В

ГД А*В

(-> /), где П ф А,

И •),

П А ТВ А С Г(В/А)ПД С

ТАВА ->■ С Г(А*В)Д -)■ а

(/ "в,

П-» В ГДД ->■ А ГПД —► А

(си1;).

В статье [1] доказано, что если В € Тр, п ^ 1 и А,- € Тр для всех » 5$ п, то секвенция Ах ... Ап —> В выводима в исчислении Ъ тогда и только тогда, когда секвенция • ... *Ап —> В выводима в исчислении Ьн-

Будем писать Ь Н Г —> А, если секвенция Г —> А выводима в исчислении Ламбека.

Разрешимость множества всех выводимых в этом исчислении секвенций была доказана Ламбеком в статье [1] путём устранения правила сечения (сЫ) в исчислении Ь.

Грамматика Ламбека есть тройка (Т,Н,>), где 7" —- произвольное конечное множество (алфавит), Н — произвольный тип исчисления Ламбека и > — произвольное конечное бинарное отношение > С Тр х Т.

Язык, порождённый грамматикой Ламбека (Т,Н,>), определяется как множество всех непустых слов ¿1 .. Лп в алфавите Т, для которых существует такая выводимая в исчислении Ламбека секвенция В\ .. .Вп —»■ Н, что для любого г ^ п выполняется В, > Обозначим этот язык через Я, >).

Контекстно-свободная грамматика есть четвёрка (У,УУ,1, И), где V и Н* — два непересекающихся конечных множества, I — элемент множества УУ, а К —- конечное множество контекстно-свободных правил вида К а, где К <Е и а € (V и П>)+.

Слово р' непосредственно выводимо из слова /3 в грамматике (у,УУ,1,И), если Р = 71 А'72, Р' = 71072 для некоторых 7Ь72 € (V и >У)+ и К => а есть правило из К.. Мы говорим, что /3' выводимо из /3 в (V, УУ, /, 72), если существует такая последовательность А), 01, ... что /3,- £ (V и И>)*, /3 = Ро, Р' = /Зп И для каждого г ^ п — 1 слово /3j.fi непосредственно выводимо из слова .

Языком, порождённым грамматикой {V, УУ, 72.) (обозначение: 0{у,УУ,1,И)), называется множество всех слов в алфавите V, выводимых в рассматриваемой грамматике из однобуквен-ного слова /.

Длина типа А определяется как суммарное количество вхождений примитивных типов и обозначается через ||А||. Для последовательности типов полагаем ЦА1 ... Ап|| ;=± ЦЛ1Ц + ... + ||/4п||.

Обозначим через Уаг(А) множество примитивных типов, входящих в тип А. Для любого натурального числа т определим Тр(гтг) как следующее конечное множество типов:

Тр(т) ^ {А € Тр | Уаг(А) С {Р1,Р2,... ,Ргп} и ||А|| «С т}.

Будем говорить, что пара ("У^о) является частичной полугруппой, если ЛУ — произвольное множество и о является такой частичной функцией из \У х ЛУ в что если определено одно из выражений а о (6 о с) или (о о Ь) о с, то второе выражение тоже определено и имеет место равенство а о (6 о с) = (а о Ь) о с. В отличие от обычной практики в алгебре, мы не исключаем случай "\У = 0.

К-фреймом называется такая частичная полугруппа (\У,о), где является строгим частичным порядком на некотором множестве Ю (как обычно, мы рассматриваем частичный порядок как множество упорядоченных пар) и частичная бинарная операция о задаётся на множестве ЛУ следующим образом:

где 51,^1,52,^2 6 О.

Обозначим через И-фрейм, где в качестве ЛУ использу-

ется обычный строгий порядок < на множестве целых чисел. Для произвольных целых чисел р 6 2 и ? 6 2 обозначим через (^^д], о) И-фрейм обычного строгого порядка < на интервале целых чисел [р, д]. Обозначим класс таких конечных И-фреймов через

Для любых множеств V. С и Т С ЛУ положим

72. о Т ^ {7 £ ЛУ | существуют такие а £ 71 и Р £ Т, что а о ¡3 = у}.

Пусть о) — частичная полугруппа. Будем говорить, что (V,-*) является частичной подполугруппой частичной полугруппы о), если V С Уо V С V и операция * является ограничением операции о на множестве V.

Моделью исчисления Ламбека на частичной полугруппе (или, для краткости, просто моделью) называется тройка о, ш), где о) — частичная полугруппа, & ги — отображение, ставящее в соответствие каждому типу исчисления Ламбека некоторое подмножество множества ЛУ (т. е. и>: Тр —* ^р(\У)) и удовлетворяющее следующим трем соотношениям:

Для любых типов А1, ... , Ап и любого отображения и> из Тр в частичную полугруппу будем писать ю(А\ ...Ап) вместо

ю{А\) о ... о \и{Ап).

Секвенция Г —^ В истинна в модели (ЛУ,©, и>) тогда и только тогда, когда Ш(Г) С ю(В). Секвенция ложна в некоторой модели тогда и только тогда, когда она не является истинной в этой модели.

, <г), если =«2>

не определено, если ¿1 ф «2,

(1) ю{А*В) = т{А) о ю{В);

(2) ю{А\В) = {7 € | ш{А) о {т} £ и;(В)};

(3) ьи(В/А) = {у £ | {7} о ю{А) £ *и{В)}.

Пусть о, и>) — модель исчисления Ламбека на частичной полугруппе. Модель (^У, о, и) называется Ь-моделью, если (ЛУ, о) .является свободной полугруппой. Модель (ЛУ, о, ю) называется II-моделью, если (\У, о) является Е-фреймом (см. [18]).

Известно, что исчисление Ламбека корректно относительно моделей на частичных полугруппах. С другой стороны, В. Бушков-ский доказал, что исчисление Ламбека полно относительно класса всех моделей на полугруппах (т. е. в исчислении Ламбека выводимы все секвенции, истинные во всех моделях на полугруппах). Основной результат данной диссертации, теорема о полноте относительно класса всех Ь-моделей, усиливает теорему Бушковского, так как Ь-модели — частный случай моделей на полугруппах.

Полнота относительно класса всех Я-моделей доказана С. Ми-кулашом (см. [20]). В данной диссертации получено усиление результата Микулаша, устанавливающее полноту относительно меньшего класса моделей, а именно, относительно класса Я-моделей, основанных на обычном отношении порядка на множестве целых чисел.

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

В третьей главе приводится доказательство того, что каждый формальный язык, порождаемый некоторой грамматикой Ламбека, также порождается некоторой контекстно-свободной грамматикой (см. [7]). Эта контекстно-свободная грамматика строится конструктивно по грамматике Ламбека. При этом роль вспомогательного алфавита в построенной контекстно-свободной грамматике играет некоторое конечное множество типов исчисления Ламбека, а контекстно-свободные правила считываются с выводимых в исчислении Ламбека секвенций ограниченной длины.

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

предыдущей. Доказывается, что в засвидетельствованных классах Тр(т)-квазимоделей ложность секвенции в некоторой Тр(т)-квази-модели влечёт её ложность в некоторой модели (теорема 4.13). Тем самым задача доказательства полноты сводится к задаче отыскания полных засвидетельствованных классов Тр(т)-квазимоделей.

Определение. Назовем квазимоделъю тройку ьи), где

ш — отображение, ставящее в соответствие каждому типу исчисления Ламбека некоторое множество элементов частичной полугруппы (ЛУ, о) и обладающее следующими двумя свойствами:

(1) и>(А*В) = ги(А) о ю(В) для любых типов А € Тр, В € Тр;

(2) если Ь I- А ->• В, то и>(А) С ю{В).

Замечание. Каждая модель на частичной полугруппе является квазимоделью.

Определение. Назовем Тр(т)-кеаэимоделъю тройку

(ЛУ^о, го), где ги — отображение, ставящее в соответствие каждому типу исчисления Ламбека некоторое множество элементов частичной полугруппы (\У, о) и обладающее следующими двумя свойствами:

(1) если А*В € Тр(т), то и>{А*В) С ии(А) о «>(£);

(2) если Г € Тр(т)+, В & Тр(т) и Ь Н Г В, то Ш(Г) С ы(В).

Определение. Секвенция Г —» А тогда и только тогда истинна в квазимодели (соответственно в Тр(т)-квазимодели) (\У,о, го), когда гй(Т) С и)(Л).

Лемма 4.2. Каждая квазимодель является Тр(т)-квазимоде-лью при любом т.

Определение. Назовем Тр(т)-квазимодель о, ю) консервативным расширением, другой Тр(т)-квазимодели (V,*,«}, если

(1) (V, *) является частичной подполугруппой частичной полу-

группы (ЛУ, о);

(2) т(А) П V = и(А) для любого типа А.

Определение. Последовательность Тр(т)-квазимоделей (\У,-, о, и;;), где г £ Н, называется консервативной, если для любого натурального » Тр(т)-квазимодель (ЛУ,-.^, о, ) является консервативным расширением предыдущей Тр(го)-кваэимодели (\У;, о, и>,-). (Здесь т фиксировано.)

Определение. Назовем пределом консервативной последовательности (Wi,o,wi), где г £ N, Тр(т)-квазимодель (Woo, ">оо), определённую следующим образом:

(i) Woo - U W,-;

igN

(й) госо(А) U Wi(A).

Лемма 4.9. Предел любой консервативной последовательности Тр(m)-кв&зимоделей является консервативным расширением каждого из элементов последовательности.

Определение. Пусть (W, о, w) является Тр(т)-квазимоде-лью. Пусть А, В £ Тр, a £ W, 7 £ W и 7 £ w(A\B). Назовем элемент а свидетелем того, что 7 ^ w(A\B), если произведение а о 7 определено, а £ w(A) и а о 7 0 w(B).

Пусть <W,o, является Тр(т)-квазимоделью. Пусть А, В € Тр, а € W, 7 G W и 7 ^ w(B/A). Назовем элемент а свидетелем того, что 7 £ w(B/A), если произведение у о а определено, а £ ti)(A) и 7 о а ^ w(B).

Определение. Пусть (U, о) является частичной полугруппой. Пусть JC — некоторый класс Тр(пг)-квазимоделей на частичных подполугруппах частичной полугруппы (U, о). Назовем класс К засвидетельствованным, если

(1) для любой Тр(т)-квазимодели (V,o,t;) £ 1С, любого типа вида

А\В из Тр(т) и любого элемента 7 £ V верно следующее: если 7 $ v(A\B), то в /С найдётся Тр(ш)-квазимодель (W, о, w), которая является консервативным расширением Тр(т)-квазимо-дели (V,o, v) и содержит свидетеля того, что 7 $ w(A\B);

(2) для любой Тр(т)-квазимодели (V, o,t>) £ /С, любого типа вида

В/А из Тр(т) и любого элемента 76V верно следующее: если 7 ^ v(B/A), то в /С найдётся Тр(т)-квазимодель (W,o, которая является консервативным расширением Тр(т)-квазимо-дели (V, o,v) и содержит свидетеля того, что 7 £ w(B/A).

Теорема 4.13. Зафиксируем натуральное число т. Пусть К. — засвидетельствованный класс Тр(т)-кваз*шоделей на частичных подполугруппах счётной частичной полугруппы (U,о). Пусть Е £ Тр(ш), F £ Тр(т). Пусть секвенция Е —+ F ложна в некоторой

Тр(т)-квазимодели из класса К. Тогда секвенция Е —► Г ложна в некоторой модели на некоторой частичной подполугруппе частичной полугруппы (и, о).

В пятой главе каждой выводимой секвенции вида Г —► В*С ставится в соответствие некоторое множество положительных целых чисел, называемых «весами» типа В относительно различных выводов секвенции Г —» В*С. Для определения «весов» вводится вспомогательное исчисление Ь^, равносильное исчислению Ламбека.

Секвенции исчисления имеют вид Г —> Д, где

Г и Д — последовательности типов. Интуитивно секвенция А-[ ... Ат —> В\ ... Вп понимается как секвенция А\ *...»Ат В\» ... *ВП.

Аксиомы имеют вид р; —>■ р; и Л —> Л.

Правила исчисления Ь<* следующие:

АП —> В , .. „ П -» А ТВА -> © Л .

(—> \), где П ^ Л, ГП(А\Б)Д -> в

ПА

П -+ В/А

(-> /),гдеП ¿А,

п —» а гвд-*©

Г(Б/Л)ПД -> ©

(/ -о,

ЭАВЕ

Г &(А*В)Н

Ь И •).

ГАВ Д -> © Г(А*В)Д ©

Г © Д 5

гд ©н

(соп).

Будем обозначать выводы в исчислении Ь^ символом 2? (возможно, с индексом, штрихами, тильдой или «крышкой»). Если Т>

V

является Ь''-выводом секвенции Г —> ©, будем писать Ь Г —> ©.

Лемма 5.4. Пусть п ^ 1, Г € Тр*, А,- 6 Тр для всех » ^ п. Секвенция Г -> ... Ап выводима в исчислении тогда и только тогда, когда секвенция Г —» Ах •... *А„ выводима в исчислении Ь.

Определение. Для любой последовательности типов Г £ Тр(т) обозначим через [Г] последовательность примитивных типов, полученную из Г опусканием всех скобок и связок.

V

Каждому Ь^-выводу секвенции Г —> С± ... Сп мы хотим поставить в соответствие разбиение слова [Г] на п непрерывных подслов Съ ■ ■ ■ , Сп (т. е. [Г] = Сх ■ • - Сп)- Весом типа С; (1 ^ г ^ п) относи-V

тельно вывода Г —>■ С\ .. . Сп является длина слова Вес типа Соотносительно вывода Т> будем обозначать через Введём обозначение .. .С^) для

+ в® (С,-+1)+...+ ^(СД

Определение. Веса определяются индукцией по построению Ьм-вывода.

Случай 1: аксиома p¿ —р,-. Положим я^(р,) ||р;|| = 1.

АН -> В , , . _

Случай 2: ^ V. Положим тР(А\В) ^ ||П||.

п Нл\в

КА —» В . #\ _

Случай 3: ^ ^ 'К Положим иР(В/А) IIXII[.

II 4 В/А

„ « . ПчА ТВАНС1...Сп .

Случаи 4: -=-~ Л —»).

Т)

ГП(А\В)Д Сх ...Сп Если ...С,.!) ^ ||Г|| < ... С,), положим

в®(СО ^ + ||П|| + ||А||, иначе ^

- _ П^А ГЯД 5 С1 ...С„ ,, . Случаи 5: -1-— (/ _>.).

Г(В/А)ПД Н С! ...Сп

Если тР (С{+1 ... Сп) < ||Д|| < ^(С, ...Сп), положим

^ + ||П|| + ||А||, иначе ^ Я®(С%).

V

Случай 6: Г еЛБ5 (-*• .). Г 5 @(А*В)Е

Положим мР{А»В) ^ -I- *Р(В) и иР{С) ^ \Р(С) для

любого типа С из © или 5.

„ V _ гл^д % © , ,

Случаи 7: —-—- (♦->)•

Г(Л*В)Д % <ё>

Положим и® (С) для любого типа С из ©.

Случай 8: Г^Аг-А. А Зц-В», V

ГА-> А1...АпВ1...Вт _ '

Положим и®(Л,-) ^ и ^ '

В шестой главе доказывается следующее свойство о «сращивании» выводов: если веса типов В\ и Въ относительно некоторых выводов секвенций Г —> Вх'Сх и Г —> В2*Сг совпадают, то секвенции Г —> В\*С2 и Г —► Вг*С\ выводимы.

Лемма 6.1. ЕслиЬ» I- Т'Т" Я Ф'Ф" ичР{Ф') = ||Т'||, то (¡) существует такой вывод Т>' секвенции Т' —> Ф', что для любого

типа С? из Ф' выполняется равенство ((7) = и^(О); (и) существует такой вывод V" секвенции Т" —У Ф", что для любого

<Г*// /ТЛ

типа С из Ф" выполняется равенство ч {О) — ъи{Сг).

Т)

Лемма 6.3. Если Ъ» Ь- Т1СЕ1 -4 Ф1Ф1,

Ь" I- Т2С£2 ^ Ф2Ф2 (ФО-ЦТ1Ц = »^(ФаИМ < ||С||,

то существует такой вывод V секвенции Т1СЕ2 Ф1Ф2, что

»^(б) = и®1 (С) для любого типа из Ф1 ; (и) в2'(С) = я^ (О) для любого типа О из Фг •

В седьмой главе доказывается ещё одно утверждение о весах: в исчислении Ьм допустимо правило сечения определённого вида, причём оно сохраняет веса.

Т) -т>

Лемма 7.3. Если Ь" Ь Т 4 Ф£Ф и Ь^ Н £ П, то существует такой вывод V секвенции Т ФПФ, что = н^1 (С) для любого типа в из Ф или Ф.

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

Определение. Будем писать Ф < П, если найдётся такая последовательность типов Ф, что ФФ = П.

Лемма 8.1. Существуют семейство множеств Юр с выделенными элементами Ир, семейство частичных полугрупп (Чр, о) £ и семейство квазимоделей на них (Чр, о, «г), индексированные последовательностями типов Г £ Тр* и обладающие следующими свойствами:

0) иг С Бг х Бг; (и) ЛгеЮг;

(111) <Лл, кг) £ иг(С) Ь Н Г ->• С для всех Г £ Тр* и С £ Тр; (1у) <ЛГ, Ьгв) € игв{В) для всех Г £ Тр* и В £ Тр; (у) иг П (Бг х Бп) С ип для всех Г £ Тр* и П £ Тр*; (VI) мг(А)П(Бг хВп) С ип(А) для всех Г £ Тр*, П £ Тр* и А £ Тр.

В доказательстве используются упорядоченные пары (Д, з), где А £ Тр* и £ £ М, обозначаемые для удобства . В качестве Ьг берется Искомые квазимодели определяются так:

^ {£д I А < Г и (||Ф|| ^ 5 Ф = Д) для всех Ф < Д}; иГ ^ {(&, 6 X БГ | г < 8}; «г^^^^а^еБгхБг!

©СЕ, »Р(©) = г, и13 (©С) =5, Д2 < П для некоторых П £ Тр+, © £ Тр*, Е £ Тр* и Х>}.

Определение. Для любых натуральных чисел тип обозначим через Ь8Тт,п следующее конечное подмножество множества Тр(т)+:

Ь5Тт,п ^ {А1 ... А1 | 1 ^ / ^ п, А! £ Тр(т), . .. , А, £ Тр(т)}.

Лемма 8.3. Для любых натуральных чисел тип существуют конечное множество Ит,п, частичная полугруппа (Vт,п, °) <Е Тр(т)-квазимодель на ней (Уто,п, о, «т,п), семейство элементов /гг> индексированное последовательностями типов Г £ Ь5Тт1„, и выделенный элемент д 6 Ит,п , обладающие следующими свойствами:

(О С 1Эгп,п X Бт,п

(н) /гг £ От,п для всех Г е Ь8Тт,„;

(ш) (д,/гг) € 1>т,гг(С) <£> Ь I- Г С для всех Г € Ь8Тт,„ я С € Тр(т);

(¿V) 6 ит>п(В) для всех Г € Ь5Тт,п иВ Е Тр(т).

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

лемме 8.1. При этом д ^ Лд, Ст,„ ^ У Юр и ьт,п(А)

ГеЬБТт,п

^ и «г(Л)- В качестве Ут,п берется такой строгий линей-Г6ЬЭТт,п

ный порядок на Т>т,п, что У Ир С Ут,п-

геьэт т,„

Основную часть девятой главы составляет доказательство технической леммы о построении «почти» Тр(т)-квазимодели с некоторыми заданными свойствами (лемма 9.1). На основе этой леммы доказывается, что класс всех реляционных Тр(ш)-квазимо-делей на конечных строгих линейных порядках засвидетельствован. Как следствие устанавливается полнота исчисления Ламбека относительно класса тех И-моделей, где синтаксическим типам ставятся в соответствие подмножества обычного строгого порядка на целых числах (теорема 9.3).

Лемма 9.1. Пусть даны натуральные числа ш,п £ N. Пусть Вт,п = [о, к], а Ут>„ = {<5,«) | 0 ^ я < < < А}. Пусть (У,о,ь) — Тр(т)-квазимодель, (\У,о) — частичная полугруппа, Е £ Тр(т), К С V, Т С \У. Пусть задана функция тт: Ут,п —> W. Введём следующие обозначения для некоторых подмножеств множества \У:

Го = {тг(л, <) | 0 ^ 5 < < < к},

■Рх = {тг(а, к) | 0 ^ 5 < к),

"Р2 = Ту о 11,

Т-Ть иГ1иТ2.

Пусть выполнены следующие условия:

(1) частичная полугруппа (V, о) является частичной подполугруппой частичной полугруппы (ЛУ, о);

(2) То П = 0;

(3) ГоС\7>2 = 0;

(4) Т>\ ПТ>2 = 0;

(5) ?ПУ = 0;

(6) 7>ПТ= 0;

(7) Т П V = 0;

(8) Г о (Я и V) С Т;

(9) (ЯиУ)оТС Т;

(10) 7г(г,з) о^.О =тг(г, С);

(11) если а ф в' и произведение тс(т,з) о 7г(в',<) определено, то 7г(г,5> 6 7";

(12) \~oVCT;

(13) •РооУСГ;

(14) для любого целого числа в < к и элемента р £ V. произведение 7г(я, к) о р определено;

(15) >1 о {/3 € W | /3 £ 7г} С Г;

(16) если в < к, з' < к и тг(з, к) = тг(в', Л), то з = в';

(17) если в < к, я' < к, р £ 11, р' € К и тг{з, к) о р = к{з', к) о р', то г = в' и р — р';

(18) для любых с*1,... , ага € ЛУ имеет место оц о.. .оа„ £ 7?. (здесь п — натуральное число, заданное в начале формулировки этой леммы).

Тогда найдётся функция и: Тр(т) ф(\У), удовлетворяющая следующим условиям:

(I) для любого типа вида А» В из Тр(тп) имеет место включение

и(А*В) С «(А)ои(В);

(II) для любых типов В\,... ,В1,С £ Тр(т), если Ь В\ ... В1 С,

то и(Вх) о ... о «(В;) С и (С) иТ;

(iii) 7г(<7, к) £ и(Е) (напомним, что д — выделенный элемент в Dm,„

и потому О ^ g <С к);

(iv) если F £ Тр(ш) л L \f Е F, то тт{д, к) £ u(F);

(v) если F £ Tp(m), p£ll и р <£ v(E\F), то тг{д, к) о р £ u(F);

(vi) для любого типа A £ Тр(т) верно v(A) С и(А);

(vii) для любого типа А £ Тр(пг) верно и(А) С г>(.А) U V.

В доказательстве определяется более общая функция и, которая ставит подмножества множества W в соответствие не только одиночным типам из Тр(т), но также последовательностям типов из Тр(т):

ио (©) ^ {тг<5, t) | 0 ^ s < t < к и {s, t) £ ü^T(©)}, «i(©) ^ {*{s,k) | 0 ^ s < к и (s,hE) £ t^7(©)}, гхг(©) ^ {"'(•s, А;) о р | 0 ^ s < /г, р £ 72. и найдётся такая

последовательность Д £ LSTm>n_i ,что р £ гГ(Д) и (s,hE д>£й^Г(©)}, м(©) — uo(0) U«i(0) Uu2(9) Uv(©).

Определение. Обозначим через /С™ класс всех Тр(ш)-квази-моделей на R-фреймах из S^.

Лемма 9.2. Пусть (V,o, v) Е , E\F € Tp(m), <5 £ V и 5 £ £ v(E\F). Тогда найдётсяТр(т)-квазимодель (W,o, w) £ /Cg1, являющаяся консервативным расширением Тр(тп)-квазимодели (V, о, v) и содержащая свидетеля того, что S £ w(E\F) (т. е. найдётся такой элемент а £ w(E), что a о 8 $ w[F)).

В доказательстве используется лемма 9.1. По данному конечному R-фрейму (V,o) = <W[jm],o) £ 5z и элементу <5 = (a, b) £ V определяются n^q — a + l,TZ^± {{a, j) | a < j ^ q}, и 7" ^ 0. Множество Dm,n можно отождествить с отрезком целых чисел [0, к] для подходящего натурального числа к. В качестве (W,o) используется о). Функция 7г задаётся следующим образом:

7r(s,k) {р — к + s,a),

ir(s, t) (р — к + s,p — к + t), если t < к.

Найденная по лемме 9.1 функция и является искомым отображением w.

Теорема 9.3. В исчислении Ламбека выводимы те и только те секвенции, которые истинны во всех R-моделях на частичной полугруппе (<z, о).

Десятая глава посвящена доказательству основного результата диссертации — теоремы о полноте исчисления Ламбека относительно L-моделей (теорема 10.6). Доказательство основано на утверждении о засвидетельствованности некоторого класса Тр(т)-квази-моделей на конечно-порождённых свободных полугруппах, которое устанавливается с помощью леммы 9.1.

Определение. Через Spree обозначим класс всех свободных полугрупп (V^jO), где V —■ конечное подмножество фиксированного счётного алфавита {aj | j £ N}. Через обозначим класс тех Тр(т)-квазимоделей (V"*", о, v) на свободных полугруппах из ¿»Free, которые удовлетворяют следующему условию: для любого типа А £ Тр(т) найдётся такое слово а £ v(A), что |а| ij m.

Лемма 10.1. Пусть m £ N, <V+,o,t;) £ 5 £ V* и

Е £ Тр(т). Тогда найдутся Тр(гп)-квазимодель (VV+ , о, ц>) £ )С™гее и такое слово a £ W"*", что

(i) <W+, о, w) является консервативным расширением Тр(т)-квази-

модели <V+, о, v);

(ii) а £ tu(£);

(iii) для любого типа F £ Тр(т), если LI■/ Е —t F, то a fi w(F);

(iv) для любого типа F £ Тр(т), если S £ V+ и i ^ v(E\F), то

а о <5 £ w(F).

Опишем кратко основные конструкции, используемые в доказательстве. Положим V ;=± V+ и п |<5| + 1. Пусть Dmi„ = [0, к]. Пусть х, z, 2/1, t/2, ••• , У к — к + 2 различных элементов алфавита {aj j j £ N}, которые не встречаются в алфавите V. Положим У ^ {x,z,yi,y2,... , у к} и W ;=± W+, где W ^ V U У. Зададим функцию 7г следующим образом:

7Г<5, t) ^ (хто О у5+1 о zm) о (хт о у3+2 о zm) о . . . о {хт о yt о гт).

Здесь и далее хт ^ х о . ..ох. Определим некоторые подмножества т раз

множества И'"*":

72. ^ {р £ У+ | р о а — 6 для некоторого слова а 6 V*},

Го ^ {тг<5, <) I 0 ^ я < г < к),

VI ^{тг(з,А;> <А},

тг,

Т'^Рои-Р! иР2,

Л'!] {а€И'~'~ | а^У"^" и а не подслово слова 7т(0, А;) о 5}, М2 ^ о>У*, Л13 ^ \Л>* о {ж}, М ^ и М.1 и Мз, Т ^ М. о „. о .

7П раз

Применим лемму 9.1 и получим функцию ы: Тр(т) —»■ ф(\У), обладающую свойствами (1)-(уп) из леммы 9.1.

Определим вспомогательную функцию ЗиЬэ^ : —> )

так, что множество (а) состоит из слова а и слов, получен-

ных подстановкой некоторых слов из множества Л4 вместо некоторых вхождений символов в слове а. Определим теперь отображения Тр(т) ф(И>+) и ш: Тр(т) <Р(П>+):

адо(Л)^ У Би^л^Л!),

ю(Л) ^и(А) и то (А).

Можно доказать, что для любого типа А £ Тр(т) выполняются включения ь(А) С и>о(А) С ь(А) и Л4 и Т С и){А). В качестве искомого слова а € И^ возьмем а п{д,к).

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

множество положительных целых чисел:

#(Л\В)^тах(1,#В-#Л), #(Л/В)^тах(1,#Л-#Я).

Положительный счётчик последовательности типов определяется естественным образом: ... А1) ^ #Л1 + ... +

Лемма 10.5. Класс £ргее непуст.

Легко видеть, что искомую Тр(т)-квазимодель (У+,о,г>) можно определить так: V {ао}, v(A) ^ {а* | к ^

Теорема 10.6. В исчислении Ламбека выводимы те и только те секвенции, которые истинны во всех Ь-моделях.

Это теорема сводится легко к предыдущим результатам. Если Ь Е —^ Р, то найдётся такое натуральное число т, что Е (Е Тр(т) и Р £ Тр(т). Применим лемму 10.1, полагая 6 = е и рассматривая Ь-модель, построенную в доказательстве леммы 10.5, в качестве V). Получаем такую Тр(т)-квазимодель (УУ*, о, гоо) £ ^йее' что и)о{Е) 2 гио(-Р') (см. лемму 10.1 (н) и (ш)). Осталось применить теорему 4.13. Засвидетельствованность класса следует из леммы 10.1 (1), (и) и (¡у).

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

ЗАКЛЮЧЕНИЕ

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

Во-первых, доказано, что грамматики Ламбека эквивалентны контекстно-свободным грамматикам Хомского (этот результат получен в кандидатской диссертации автора; до этого было известно

лишь, что каждая контекстно-свободная грамматика эквивалентна некоторой грамматике Ламбека).

Во-вторых, установлена полнота исчисления Ламбека относительно естественного класса моделей для этого исчисления. В этих моделях рассматриваются три бинарные операции *, \ и /, определённые на формальных языках в некотором алфавите V следующим образом:

Л*В^± {aoß | а е А, ß G В}; Л\В^±{уЕ V+ | Л*{7} С В};

B/A^±{yeV+\b}*ACB}.

Доказано, что в исчислении Ламбека выводимы в точности все тождественно истинные соотношения вида X С У, где выражения X и Y составлены с помощью бинарных операций \ и / из переменных по формальным языкам в произвольном алфавите V, содержащем не менее двух букв.

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

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

РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

1. Pentus М. Lambek calculus is L-compiete. — Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1993. — 36 p. — (ILLC Prepublication Series; LP-93-14).

2. Pentus M. Language completeness of the Lambek calculus // Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science: July 4-7, 1994. Paris, France; — Los Alamitos, California: IEEE Computer Society Press, 1994. — P. 487-496.

3. Pentus M. The conjoinability relation in Lambek calculus and linear logic // Journal of Logic, Language and Information. — 1994. — Vol. 3, no. 2. — P. 121-140.

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

5. Pentus М. Models for the Lambek calculus // Annals of Pure and Applied Logic. — 1995. — Vol. 75, no. 1-2. — P. 179-213.

6. Пентус M. P. Синтаксическое исчисление Ламбека и формальные грамматики // YSTM'96: *Молодежь и наука — третье тысячелетие». Труды международного конгресса / Под ред. И. Б. Федорова, К. С. Колесникова и А. О. Карпова. — М.: НТА «Актуальные проблемы фундаментальных наук», 1997. — Т. 1. — С. I-15-I-16.

7. Pentus М. Product-free Lambek calculus and context-free grammars // Journal of Symbolic Logic. — 1997. — Vol. 62, no. 2. — P. 648-660.

8. Pentus M. Lambek calculus and formal languages // Logic Colloquium '95: Proceedings of the Annual European Summer Meeting of the Association of Symbolic Logic, held in Haifa, Israel, August 9-18, 1995 / Editors J. A. Makowsky and E. V. Ravve. — Berlin etc.: Springer, 1998. — P. 269-272. — (Lecture Notes in Logic; 11).

9. Pentus M. Free monoid completeness of the Lambek calculus allowing empty premises // Logic Colloquium '96: Proceedings of the colloquium held in San Sebastian, Spain, July 9-15, 1996 / Editors J. M. Larrazabal, D. Lascar and G. Mints. — Berlin etc.: Springer, 1998. — P. 171-209. — (Lecture Notes in Logic; 12).

10. Pentus M. Lambek calculus and formal grammars // Provability, Complexity, Grammars / L. D. Beklemishev, M. Pentus, N. K. Vereshchagin. — American Mathematical Society, 1999. — P. 57-86. — (American Mathematical Society Translations. Series 2; Vol. 192).

11. Пентус M. P. Полнота синтаксического исчисления Ламбека // Фундаментальная и прикладная математика. — 1999. — Т. 5, № 1. — С. 193-219.

Введение

1 Определения

1.1 Исчисление Ламбека.

1.2 Грамматики Ламбека и контекстно-свободные грамматики.

1.3 Модели на частичных полугруппах

2 Известные свойства исчисления Ламбека

2.1 Устранимость сечения.

2.2 Простые теоретико-доказательственные свойства

2.3 Интерпретация в свободной группе.

2.4 Интерполяционное свойство.

2.5 Корректность исчисления Ламбека.

2.6 Полнота фрагмента исчисления Ламбека.

3 Грамматики Ламбека

3.1 Одно свойство свободных групп.

3.2 Тонкие секвенции.

3.3 Исчисление Ъси^.

3.4 Контекстно-свободность языков, порождаемых грамматиками Ламбека.

4 Квазимодели

4.1 Определение Тр(т)-квазимоделей

4.2 Консервативные расширения.

4.3 Свидетели

5 Веса

5.1 Исчисление I/.

5.2 Эквивалентность исчислений I/ и Ь.

5.3 Определение весов.

5.4 Обратимость правил (—> •) и (• —>•).

6 Сращивание выводов

7 Правило сечения

8 Построение квазимоделей

9 Т1-полнота

9.1 Основная лемма.

9.2 Засвидетельствованность класса конечных линейных И-фреймов

10 Ь-полнота

10.1 Засвидетельствованность класса ^Сргее.

10.2 Непустота класса /Ср£ее.

10.3 Основная теорема.

Актуальность темы. Категориальная грамматика — раздел математической лингвистики, описывающий формальные законы синтаксических категорий в естественных и искусственных языках. Одно из центральных мест в нём занимает исчисление Ламбека. которое было введено в статье [36] для изучения свойств формальных языков. Формальным языком называется произвольное множество непустых слов (конечных последовательностей символов) над некоторым конечным алфавитом. В лингвистических приложениях при описании синтаксиса естественного языка алфавитом (в математическом смысле) является множество всех словоформ рассматриваемого фрагмента естественного языка. При этом множество всех грамматически правильных предложений образует формальный язык. Другие важные примеры формальных языков над тем же алфавитом — множество всех именных групп, множество всех групп сказуемого и т. д.

Исчисление Ламбека описывает свойства трёх бинарных операций над формальными языками: операции умножения, операции правого деления и операции левого деления (эти операции обозначаются соответственно •, / и \). Произведение языков состоит из всевозможных попарных конкатенаций их элементов. Результат правого деления языка А на В (обозначается А/В и читается «А над Б») определяется как множество всех таких непустых слов 7, что {7}•£ С А. Результат левого деления языка А на В (обозначается В\А и читается «В под А») определяется как множество всех таких

- 5 непустых слов 7, что В»{7} С А.

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

1) отношение С рефлексивно и транзитивно,

2) умножение ассоциативно,

3) С С А/В тогда и только тогда, когда С»В С А,

4) С С В\А тогда и только тогда, когда В»С С А.

Для описания синтаксиса естественных языков Бар-Хиллел в 1950-х годах ввёл понятие базовой категориальной грамматики (см. [9]). Каждая базовая категориальная грамматика приписывает словоформам рассматриваемого фрагмента естественного языка термы, составленные с помощью операций \ и /. Содержательно каждый такой терм служит обозначением для некоторой синтаксической категории, т. е. некоторого класса словоформ и словосочетаний с одинаковой синтаксической сочетаемостью. В грамматике выделен один терм (обычно он обозначает класс всех грамматически правильных предложений). Последовательность словоформ допускается данной грамматикой, если соответствующую последовательность термов можно сократить так, что останется только выделенный терм. При этом разрешается сократить соседние термы А/В и В (получается А), а также В и В\А (тоже получается А). Достоинства и недостатки категориальных грамматик перечислены в работе [3, с. 134-135].

- б

Грамматики Ламбека отличаются от базовых категориальных грамматик тем, что в них разрешены более сложные сокращения (которые определяются вышеупомянутым исчислением Ламбека). Согласно терминологии, принятой для базовых категориальных грамматик, термы исчисления Ламбека, составленные с помощью операций \ и /, называются синтаксическими категориями, синтаксическими типами или просто типами, а простейшие термы (переменные) называются примитивными типами. Следуя обозначениям, используемым для базовых категориальных грамматик, вместо А С В в исчислении Ламбека обычно пишут А ч- В.

Некоторые современные приложения исчисления Ламбека к изучению естественных языков приводятся в книгах [23,24,40].

В конце 50-х — начале 60-х годов возник вопрос о связи категориальных грамматик (в том числе грамматик Ламбека) с иерархией порождающих грамматик Хомского, включающей четыре вложенных друг в друга класса: порождающие грамматики (самый большой класс), грамматики непосредственно составляющих, контекстно-свободные грамматики и автоматные грамматики. В 1960 году Бар-Хиллел, Гайфман и Шамир доказали, что формальный язык может быть задан некоторой базовой категориальной грамматикой тогда и только тогда, когда он является контекстно-свободным, т. е. может быть задан некоторой контекстно-свободной грамматикой (см. [1,2,10]). Они высказали гипотезу что то же самое имеет место для грамматик Ламбека (см., например, [25,39]). Доказательство одной половины этой гипотезы (а именно того, что любой контекстно-свободный язык задаётся некоторой грамматикой Ламбека) фактически совпадает с соответствующим доказательством для базовых категориальных грамматик (см. [22,26]). Во

- 7 прос об обратном включении оставался открытым в течение многих лет. В. Бушковским были получены частичные результаты, относящиеся к фрагменту без правого деления и умножения и к фрагменту без умножения с некоторым ограничением на вложенность разносторонних делений (см. [19,21]). Положительный ответ для исчисления Дамбека в целом получен в диссертации [5] (доказано, что формальный язык может быть задан некоторой грамматикой Ламбека тогда и только тогда, когда он является контекстно-свободным).

Некоторые современные приложения исчисления Ламбека к изучению естественных языков приводятся в книгах [23,24,40].

С исчислением связаны и другие нетривиальные математические проблемы (см. [34,57]). Ряд вопросов касается интерпретации исчисления Ламбека на различных математических структурах (см. напр. [11,16] и обзорные статьи [28,29,43]).

Наиболее широкий класс интерпретаций исчисления Ламбека образуют полугруппы с делением. Полугруппой с делением называется полугруппа (Н, •), рассматриваемое вместе с частичным порядком причём для любых элементов а, 6 £ Н существует такой элемент а/Ъ Е Н (правое частное элемента а по 6), что условия х ^ а/Ъ и х*Ъ ^ а эквивалентны, и существует такой элемент Ь\а £ Н (левое частное элемента а по 6), что условия х ^ Ъ\а и Ъ»х ^ а эквивалентны (см. [30]). В некоторых книгах вместо а/Ъ пишут а:6, а вместо Ь\а пишут а::Ъ.

Интерпретация исчисления Ламбека в полугруппе с делением Н задаётся произвольной функцией г>, ставящей в соответствие примитивным типам элементы Н. Интерпретирующая функция V продолжается естественным образом на все типы. Утверждение А —> В является истинным при данной интерпретации, если

-8 у(А) ^ ь(В).

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

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

К. Дошен рассмотрел следующую конструкцию. Частично упорядоченной полугруппой называется такая полугруппа с частичным порядком, где полугрупповая операция монотонна. Множество всех таких подмножеств А частично упорядоченной полугруппы С, что из а ^ Ь и Ь Е А следует а Е А, является полугруппой с делением относительно порядка С и операции

А'В ^ {с Е С | с ^ аЬ для некоторых а Е А, Ь Е В}.

В 1985 году К. Дошен [27] доказал полноту исчисления Ламбека относительно моделей на таких полугруппах с делением.

В 1986 году В. Бушковский [20] опубликовал доказательство полноты относительно ещё более узкого класса моделей исчисления Ламбека. Он рассматривал в качестве полугруппы с делением множество всех подмножеств произвольной полугруппы При этом в

- 9 качестве порядка снова использовалось отношение С, а в качестве операции умножения — операция •, определяемая так:

А*В ^ {аЬ | а 6 Л, Ье В].

Такие полугруппы с делением представляют частный случай полугрупп с делением, рассмотренных Дошеном (достаточно на С в качестве отношения частичного порядка ввести отношение равенства). Таким образом, результат Бушковского сильнее результата Дошена.

Особый интерес представляют модели исчисления Ламбека на множестве подмножеств свободной полугруппы (частный случай моделей, рассмотренных Бушковским). Эти модели обычно называются языковыми моделями исчисления Ламбека или Ь-моделями, так как в них \ и / обозначают умножение, левое деление и правое деление формальных языков, определённые на стр. 4. Именно эта интерпретация рассматривалась в статье [36] при формулировке исчисления Ламбека. Корректность исчисления Ламбека относительно Ь-моделей следует непосредственно из корректности относительно интерпретаций в полугруппах с делением, более широких классов моделей. Вопрос о полноте относительно Ь-моделей долгое время оставался открытым (см., например, [14,20,21,29,58]). Конструкция Бушковского непригодна для доказательства полноты относительно Ь-моделей, так как согласно этой конструкции по невыводимой секвенции строится контрмодель на сложно устроенной частичной полугруппе (в частности, в этой частичной полугруппе любой элемент представим в виде произведения других элементов бесконечным числом способов, в то время как в свободной полугруппе это не так).

В данной диссертации дан положительный ответ на вопрос о полноте исчисления Ламбека относительно Ь-моделей. Более того, доказано, что исчисление Ламбека полно относительно класса всех Ь-моделей на двухбуквенном алфавите, т. е. для каждого невыводимого утверждения А —у В, где А и В — типы исчисления Ламбека, найдётся некоторая интерпретирующая функция V, ставящая в соответствие примитивным типам множества слов в двухбуквенном алфавите, такая что ь(А) у(В).

Во многих работах изучается также другой частный случай моделей исчисления Ламбека на полугруппах с делением — реляционные модели (см. [12,13,44]). Мы рассматриваем бинарные отношения как множества упорядоченных пар. Композицией (или произведением) бинарных отношений А и В называется бинарное отношение {{г, ¿) | (г, 5) £ Аи ($,£) £ В для некоторого я}. Пусть 5 — строгий частичный порядок на некотором множестве. Множество всех подмножеств 5 с определёнными на нём операцией композиции и отношением С образует полугруппу с делением. Интерпретация исчисления Ламбека в любой такой полугруппе называется реляционной моделью исчисления Ламбека или 11-моделыо.

С. Микулаш доказал в 1992 году (см. [41,42]), что исчисление Ламбека полно относительно реляционных моделей. Возник вопрос об усилении этого результата путём указания какого-нибудь конкретного простого отношения строгого частичного порядка, относительно 11-моделей на котором исчисление Ламбека было бы полно. В данной диссертации доказано, что в качестве такого отношения подходит обычный строгий линейный порядок на целых числах.

Операции умножения и делений, обладающие свойствами, описываемыми исчислением Ламбека, встречаются в различных алгебры. Например, на множестве всех двусторонних идеалов произвольного ассоциативного кольца И можно рассмотреть операции \ и / (обычно вместо \ и / пишут ' . и . '), определённые следующим образом (см. [37]): п

А»В состоит из всех конечных сумм ^ где а; £ А и Ь{ £ В; 1

А\в ^ {г £ Я | Аг С Б}; А/в ^ {г £ Я I гВ С А}.

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

Аналогичные операции на различных решётках с делением рассматриваются в монографии [15], где Г. Биркгоф приводит ряд утверждений, фактически являющихся теоремами исчисления Ламбека.

Цель работы — доказать гипотезу о полноте исчисления Ламбека относительно языковых моделей (высказанную в восьмидесятых годах Зелонкой, Бушковским, ван Бентхемом и другими) и гипотезу о полноте этого исчисления относительно реляционных моделей на обычном отношении порядка целых чисел.

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

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

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

В первой главе даются основные определения, используемые в работе. Приведём некоторые из них.

Пусть V — некоторый алфавит. Под свободной полугруппой будем понимать множество всех непустых слов У+ некоторого алфавита У. При этом полугрупповой операцией является операция конкатенации (т. е. склеивания) слов.

Типы исчисления Ламбека определяются следующим образом. Предполагаем, что задано счётное множество {р1,р2,рз, • - элементы которого будем называть примитивными типами. Типы исчисления Ламбека строятся из примитивных типов с помощью трёх бинарных связок Обозначим множество всех типов, построенных таким образом, через Тр. Прописные буквы латинского алфавита будем использовать для обозначения типов исчисления Ламбека, а прописные греческие буквы — для обозначения конечных (не обязательно непустых) последовательностей типов. Символ А будет всегда обозначать пустую последовательность типов. Иногда будем писать . *АП вместо (. . •Ап).

В статье [36] И. Ламбек ввёл два дедуктивно эквивалентных друг другу исчисления (мы будем обозначать их Ьн и Ь). Выводимыми объектами исчисления Ьн являются записи вида А —> В. Аксиомы имеют вид А А, (А»В)»С А*(В»С) и А»(В*С) (А»В)»С. Выводы строятся с помощью следующих правил:

В статье [36] доказано, что если В Е Тр, п ^ 1 и А{ Е Тр для всех г ^ п, то секвенция А\ . Ап В выводима в исчислении Ь тогда и только тогда, когда секвенция А\». *Ап —> В выводима в исчислении Ьц.

Будем писать Ь Ь Г —у А, если секвенция Г —у А выводима в исчислении Ламбека.

Разрешимость множества всех выводимых в этом исчислении секвенций была доказана Ламбеком в статье [36] путём устранения правила сечения (си1;) в исчислении Ь.

Грамматика Ламбека есть тройка (У, Я, >), где У — произвольное конечное множество (алфавит), Н — произвольный тип исчисления Ламбека и о — произвольное конечное бинарное отношение о С Тр х V.

Язык, порождённый грамматикой Ламбека (у,Н,>), определяется как множество всех непустых слов I . Лпъ алфавите У, для которых существует такая выводимая в исчислении Ламбека секвенция В\. Вп —>• Н, что для любого г < п выполняется В^ 1> £г-. Обозначим этот язык через £/:(У, Я,о).

Контекстно-свободная грамматика есть четвёрка (V, УУ, где У и УУ — два непересекающихся конечных множества, / — элемент множества >У, а — конечное множество контекстно-свободных правил вида К а, где К Е УУ и а Е (У и УУ)+.

Слово /3' непосредственно выводимо из слова ¡3 в грамматике (V, УУ, /,72.), если [3 = 71/С72, (3' = ъа12 для некоторых 71,72 Е (У и УУ)+ и К а есть правило из 71. Мы говорим, что /31 выводимо из (3 в (У, УУ,/,7£), если существует такая последовательность /Зо, /3\, . /Зп, что ^ Е (У и УУ)*, ¡3 = Д), ¡3' = ¡Зп и для каждого г ^ п — 1 слово непосредственно выводимо из слова ¡3{.

Языком, порождённым грамматикой (V, УУ,/, 72.) (обозначение: УУ,/, 7£)), называется множество всех слов в алфавите V, выводимых в рассматриваемой грамматике из однобуквен-ного слова I.

Будем говорить, что пара (ЛУ,о) является частичной полугруппой. если \У — произвольное множество и о является такой частичной функцией из ЛУ х в \У, что если определено одно из выражений а о (Ъ о с) или (а о Ъ) о с, то второе выражение тоже определено и имеет место равенство а о {Ь о с) = (а о Ь) о с. В отличие от обычной практики в алгебре, мы не исключаем случай ЛУ = 0.

Т1 -фреймом называется такая частичная полугруппа (ЛУ,о), где ЛУ является строгим частичным порядком на некотором множестве Ю (как обычно, мы рассматриваем частичный порядок как множество упорядоченных пар) и частичная бинарная операция о задаётся на множестве ЛУ следующим образом: где 5Ь 52, ¿2 6 О.

Обозначим через о) 11-фрейм, где в качестве ЛУ используется обычный строгий порядок < на множестве целых чисел. Для любых множеств 71 С ЛУ и Т С ЛУ положим

71 о Т ^ {7 Е ЛУ | существуют такие а £71 и (3 Е Т, что а о ¡3 = 7}.

Пусть (ЛУ, о) — частичная полугруппа. Будем говорить, что (V,*) является частичной подполугруппой частичной полугруппы

51, £2), если ¿1 = 52 не определено, если ¿1 ф 52

ЛУ,о), если если

1) УС¥;

2) Уо V С V;

3) операция * является ограничением операции о на множестве V.

Моделью исчисления Ламбека на частичной полугруппе (или, для краткости, просто моделью) называется такая тройка (ЛУ, о, и>), где (ЛУ, о) — частичная полугруппа, а ю — отображение, ставящее в соответствие каждому типу исчисления Ламбека некоторое подмножество множества ЛУ и удовлетворяющее следующим трем соотношениям:

1) т{А»В) = -ш(А) о т(В)]

2) т(А\В) = {7б¥| ю(А) о {7} € ш(В)};

3) ъи{В/А) = {7б¥| {7} о ю{А) е и) {В)}.

Для любых типов А\, . , Ап и любого отображения и] из Тр в частичную полугруппу (ЛУ, о) будем писать Ш(А1. Ап) вместо п){А\) о . о т(Ап).

Секвенция Г —» В истинна в модели (ЛУ, о, и)) тогда и только тогда, когда Й7(Г) С и)(В).

Пусть (W, о, т) — модель исчисления Ламбека на частичной полугруппе. Модель (ЛУ,о,ги) называется Ь-моделью, если (W,o} является свободной полугруппой. Модель (ЛУ, о,ги) называется К-моделъю, если (ЛУ, о) является 11-фреймом.

Известно, что исчисление Ламбека корректно относительно моделей на частичных полугруппах. С другой стороны, В. Бушков-ский доказал, (см. [20]), что исчисление Ламбека полно относительно класса всех моделей на полугруппах (т. е. в исчислении Ламбека выводимы все секвенции, истинные во всех моделях на полугруппах). Основной результат данной диссертации, теорема о полноте относительно класса всех Ь-моделей, усиливает теорему Бушковского, так как Ь-модели — частный случай моделей на полугруппах.

Полнота относительно класса всех 11-моделей доказана С. Ми-кулашом (см. [41]). В данной диссертации получено усиление результата Микулаша, устанавливающее полноту относительно меньшего класса моделей, а именно, относительно класса 11-моделей, основанных на обычном отношении порядка на множестве целых чисел.

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

В третьей главе приводится доказательство того, что каждый формальный язык, порождаемый некоторой грамматикой Ламбека, также порождается некоторой контекстно-свободной грамматикой (см. [5]). Эта контекстно-свободная грамматика строится конструктивно по грамматике Ламбека. При этом роль вспомогательного алфавита в построенной контекстно-свободной грамматике играет некоторое конечное множество типов исчисления Ламбека, а контекстно-свободные правила считываются с выводимых в исчислении Ламбека секвенций ограниченной длины.

В четвёртой главе определяются понятия Тр(т)-квазимо-дели исчисления Ламбека (обобщение понятия модели на частичной полугруппе) и засвидетельствованного класса Тр(т)-квазимоделей.

Длина типа А определяется как суммарное количество вхождений примитивных типов и обозначается ||А||.

Обозначим через Уаг(А) множество примитивных типов, входящих в тип А.

Для любого натурального числа т определим Тр(т) как следующее конечное множество типов:

Тр(ш) ^ {А б Тр | Уаг(А) С {ръръ • ■ • ,Рт} и ||Л|| < т].

Определение. Назовем Тр[т]-квазимоде лью любую тройку {ЛУ,о,к;}, где ъи — отображение, ставящее в соответствие каждому типу исчисления Ламбека некоторое множество элементов частичной полугруппы ("\У, о) и обладающее следующими двумя свойствами:

1) если А*В £ Тр(т), то <ш(А*В) С ю(А) о ги(Б);

2) если Г £ Тр(т)+, В £ Тр(т) и Ь Ь Г Б, то й7(Г) С -ш(В).

Определение. Секвенция Г —у А тогда и только тогда истинна в Тр(га)-квазимодели ("\У,о,и>), когда гй(Г) С ю(А).

Определение. Назовем Тр(т)-квазимодель {\У",о,и>} консервативным расширением другой Тр(т)-квазимодели ("V,-^г,у), если

1) (V,*) является частичной подполугруппой частичной полугруппы (\У,о);

2) ш(А) П V = у(А) для любого типа А.

Определение. Пусть (ЛУ, о,ги) является Тр(т)-квазимоделью. Пусть А, В £ Тр, а £ W, 7 £ и 7 ^ ъи(А\В). Назовем элемент а свидетелем того, что 7 ^ и)(А\В), если произведение а о 7 определено, а Е ш(А) и «07 ^ и)(В).

Пусть (\У,о,и>) является Тр(т)-квазимоделью. Пусть А, В Е Тр, а Е ЛУ, 7 Е и 7 ^ и)(В/А). Назовем элемент а св?2-детелем того, что 7 ^ уо^В/А), если произведение 70а определено, а; Е и>(Л) и 7 о а ^ IV(В).

Определение. Пусть (и, о) является частичной полугруппой. Пусть 1С — некоторый класс Тр(т)-квазимоделей на частичных подполугруппах частичной полугруппы (и, о). Назовем класс К засвидетельствованным, если

1) для любой Тр(ш)-квазимодели (V, о,г>) Е 1С, любого типа вида

А\В из Тр(т) и любого элемента 7 Е V верно следующее: если 7 ^ у(А\В), то в /С найдётся Тр(ш)-квазимодель (ЛУ, о,и>), которая является консервативным расширением Тр(т)-квазимо-дели {У,о,г>} и содержит свидетеля того, что 7 ^ ии(А\В);

2) для любой Тр(т)-квазимодели (V, о,г>) Е 1С, любого типа вида

В/А из Тр(т) и любого элемента 7 Е V верно следующее: если 7 ф. у{В/А), то в 1С найдётся Тр(т)-квазимодель (Л¥,о,и>), которая является консервативным расширением Тр(ш)-квазимо-дели (V, о, г>) и содержит свидетеля того, что 7 ^ ю(В/А).

Далее в четвёртой главе описывается алгоритм построения модели на частичной полугруппе как предела бесконечной последовательности Тр(т)-квазимоделей, каждая из которых является консервативным расширением предыдущей. Доказывается, что в засвидетельствованных классах Тр(т)-квазимоделей ложность секвенции в некоторой Тр(ш)-квазимодели влечёт её ложность в некоторой модели (теорема 4.13 на стр. 71). Тем самым задача доказательства полноты сводится к задаче отыскания полных засвидетельствованных классов Тр(т)-квазимоделей.

В пятой главе каждой выводимой секвенции вида Г —У В*С ставится в соответствие некоторое множество положительных целых чисел, называемых «весами» типа В относительно различных выводов секвенции Г -» В*С (см. стр. 79). Для определения «весов» вводится вспомогательное исчисление 1/* (см. стр. 75), равносильное исчислению Ламбека.

В шестой главе доказывается следующее свойство о «сращивании» выводов: если веса типов В\ и В2 относительно некоторых выводов секвенций Г —>- В\*С\ и Г —>■ В^С^ совпадают, то секвенции Г -Л В^С2 и Г —» В2*С\ выводимы (лемма 6.3 на стр. 98).

В седьмой главе доказывается ещё одно утверждение о весах: в исчислении I/ допустимо правило сечения определённого вида, причем оно сохраняет веса (лемма 7.3 на стр. 112).

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

Определение. Для любых натуральных чисел тип обозначим через Ь8Тт п следующее конечное подмножество множества Тр(т)+:

ЬЗТт>п ^ {А!. Ах | 1 < К п, € Тр(т), . , А{ е Тр(т)}.

Лемма 8.3. Для любых натуральных чисел т ип существуют конечное множество 1)щП, частичная полугруппа (УТО)П, о) Е Тр(т)-квазимодель на ней {~Ут^П1 °5 г'т,п), семейство элементов /гг, индексированное последовательностями типов Г Е Ь8Тт1П, и выделенный элемент д Е обладающие следующими свойствами:

1) Ут,п ^ И)т)П, и) /г г € для -всех Г Е Ь8ТТО|П; ш) (д, /¿г) е ьт>п(С) ^ Ь Н Г для всех Г Е ЬЭТ^ йС Е Тр(ш); (¿у) (/гг,^гв> £ для всех Г Е ЬБТ™^ и В £ Тр(т).

Основную часть девятой главы составляет доказательство технической леммы о построении «почти» Тр(т)-квазимодели с некоторыми заданными свойствами (лемма 9.1 на стр. 124). На основе этой леммы доказывается, что класс всех реляционных Тр(т)-квази-моделей на конечных строгих линейных порядках засвидетельствован (лемма 9.2 на стр. 132). Как следствие устанавливается полнота исчисления Ламбека относительно класса тех Ы-моделей, где синтаксическим типам ставятся в соответствие подмножества обычного строгого порядка на целых числах.

Теорема 9.3. В исчислении Ламбека выводимы те и только те секвенции, которые истинны во всех К-моделях на частичной полугруппе (<%, о).

Десятая глава посвящена доказательству основного результата диссертации — теоремы о полноте исчисления Ламбека относительно Ь-моделей.

Теорема 10.6. В исчислении Ламбека выводимы те и только те секвенции, которые истинны во всех Ь-моделях.

- 22

Доказательство основано на утверждении о засвидетельство-ванности некоторого класса Тр(т)-квазимоделей на конечно-порождённых свободных полугруппах, которое устанавливается с помощью леммы 9.1.

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

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

1 Определения

Приведём основные определения, используемые в диссертации, следуя обозначениям из [4,53].

Множество всех целых чисел обозначим через Ж, множество всех натуральных чисел (с нулем) — через N. Отрезок множества целых чисел [р, д], где р Е Ъ и д Е состоит из всех таких целых чисел х Е что р ^ х ^ д.

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

Под свободной полугруппой будем понимать множество всех непустых слов некоторого алфавита. При этом полугрупповой операцией является операция конкатенации (т. е. склеивания) слов.

Множество всех подмножеств произвольного множества обозначим через *}3(\У).

1.1 Исчисление Ламбека

Рассмотрим исчисление, введённое И. Ламбеком в статье [36]. Предполагаем, что задано счётное множество Уаг = ■ • ■ }? элементы которого будем называть примитивными типами. Типы исчисления Ламбека (также называемые синтаксическими типами) строятся из примитивных типов с помощью трёх бинарных связок \, /, называемых умножением, левым делением и правым делением соответственно. Обозначим множество всех типов, построенных таким образом, через Тр. Для множества всех конечных последовательностей типов используем обозначение Тр*, а для множества всех непустых конечных последовательностей типов — Тр+). Прописные буквы латинского алфавита будем использовать для обозначения типов исчисления Ламбека, а прописные греческие буквы — для обозначения конечных (не обязательно непустых) последовательностей типов. Символ А будет всегда обозначать пустую последовательность типов. Иногда будем писать А\и. *Ап вместо (. [А^А^У. *АП).

В статье [36] И. Ламбек ввёл два дедуктивно эквивалентных друг другу исчисления (мы будем обозначать их Ьн и Ь). Выводимыми объектами исчисления Ьн являются записи вида А —у В. Аксиомы имеют вид А А, (А»В)»С А»(В*С) и А»(В»С) (А»ВуС. Выводы строятся с помощью следующих правил:

Рассмотрим теперь исчисление Ь. Выводимыми объектами этого исчисления являются записи вида А\. Ап -» Б, где п ^ 1 (такие записи называются секвенциями). Интуитивно А\. Ап —» В

А*С В С ч А\В

С*А —> В С ч В/А

С А\В А*С ч В

С -л В/А С* А —В

АчВ В чС АчС означает то же, что и А1».»Ап —> В. Тип В называется сукце-дентом, а последовательность А\ . Ап — антецедентом секвенции

Аксиомы исчисления Ь имеют вид А —>• А. Выводы строятся с помощью следующих правил:

Равносильность исчислений Ь и Ьн доказана И. Ламбеком в работе [36].

Теорема 1.1 (Ламбек). Пусть В Е Тр, п ) 1 г А; Е Тр для всех г ^ п. Секвенция А] . Ап —>■ В выводима, в исчислении Ь тогда и только тогда, когда секвенция А\». *АП —В выводима в исчислении Ьн.

Будем писать Ъ Ь Г —А, если секвенция Г —> А выводима в исчислении Ь. Ах. Ап-> В.

Пример 1.2. Например, L Ь ((М.Р2)/.Рз) (рЛМрз))'

PI ->Р 1 Р2 -> Р2 /х , Pz-^Pi Pi {Pl\Pl) Р2 ,) У У Pi {{PI\V2)IPZ) Рз^Р2 У У Pi ((PI\P2)/P2) -* fe/M r (ч ((рДр2)/рз) (МЫрз)) 1 ^

Замечание. Разрешимость множества всех выводимых в этом исчислении секвенций была доказана Ламбеком в статье [36] путём устранения правила сечения (cut) в исчислении L.

Замечание. Связь исчисления Ламбека и его вариантов с линейной логикой изучалась в статье [48].

Определение. Длина типа определяется как суммарное количество вхождений примитивных типов: ы -1,

А-В\\ ^ 1ИИ + \\В

1И\-В|| ^ ||А|| + р

ЦА/В|| ^ ||А|| + \\В

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

Ai ■ ■ ■ Лг|| ^ ||Ai|| + . + ||А

Определение. Множество примитивных типов, входящих в данный тип, определяется следующим образом:

Уаг(рг-) Уаг (А»В) Уаг (А\В) Уаг (А/В)

Рг'},

Уаг(А) и Уаг(Б), Уаг(А)иУаг(Б), Уаг(А) и Уаг(Б).

Определение. Количество вхождений примитивного типа р1 в тип А определяется так:

PjWpi

А-В\\Рг \\АЩ\Р,

1, если г — у О, если г ф ]

А\\рг + \\В\\рИ \\ЦР1 + \\В\\РГ

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

А\. Ап||р(.

П\\Рг

Определение. Для любого натурального числа т определим Тр(т) как следующее конечное множество типов:

Тр(т) - {Л е Тр | Уаг(Л) С {рир2,. ,рт} и ||Л|| < т}.

Через Тр(т)+ будем обозначать множество всех непустых конечных последовательностей типов из Тр(т).

Замечание. Очевидно,

Тр= у Тр(т). тем

Заключение

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

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

Во-вторых, установлена полнота исчисления Ламбека относительно естественного класса моделей для этого исчисления. В этих моделях рассматриваются три бинарные операции •, \ и /, определённые на формальных языках в некотором алфавите У следующим образом:

А*Б ^ {а о (3 | а е А, (3 е В}] I А*{у] С В}]

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

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

Тр, 24 Тр(т), 27 Тр(\,/),50 (У,Я,>), 28 (У,УУ,7,71), 28 V*, 23 У+, 23 Уаг, 23 Уаг(А), 27 Уаг, 40 Й7, 32

Ь,фо},31 о), 29

W, о, и') (Тр(ш)-квазимодель), (ЛУ,о,и;) (квазимодель), 64 (Л¥,о,и/) (модель), 32

23 И, 23 147 23 [Г], 78 А, 24 <, 118 >, 28

2,о>, 30 алфавит, 23 антецедент, 25

- 156 вес, 79 вспомогательный алфавит, 28 грамматика Ламбека, 28 длина слова, 23 длина типа, 26 засвидетельствованный класс, 70 интерполянт, 43 интерпретация в свободной группе, 41 истинность в квазимодели, 65 истинность в модели, 33 исчисление Ламбека, 23 квазимодель, 64 Тр(т)-квазимодель, 64 консервативная последовательность, 68 консервативное расширение Тр(т)-квазимодели, 66 контекстно-свободная грамматика, 28 контекстно-свободный язык, 29 левое деление, 23 ложность в модели, 33

Ь-модель, 33 Я-модель, 33 модель исчисления Ламбека на частичной полугруппе, 32 начальный символ, 28 отрезок множества целых чисел, 23

- 157 подстановка примитивных типов, 54 правое деление, 24 предел, 68 префикс, 118 приведённое слово, 40 примитивный тип, 23 пустое слово, 23 свидетель, 69 свободная полугруппа, 23 секвенция, 24 синтаксический тип, 23 сукцедент, 25 счётчик положительный, 147 терминальный алфавит, 28 тип, 23 тонкая секвенция, 54 умножение, 23 R-фрейм, 30 частичная подполугруппа, 31 частичная полугруппа, 29

158

1. Гладкий А. В. Лекции по математической лингвистике для студентов НГУ. — Новосибирск.: Издательство НГУ, 1966.

2. Гладкий А. В. Формальные грамматики и языки. — М.: Наука, 1973.

3. Гладкий А. В., Мельчук И. А. Элементы математической лингвистики. — М.: Наука, 1969. — 192 е.: ил.

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

5. Пентус М. Р. Исчисление Ламбека и формальные грамматики: Дис. . канд. физ.-мат. наук: 01.01.06. — Защищена 01.03.1996; Утв. 14.06.1996; 01910048811. — М., 1996. — 69 с. — Библиогр.: с. 67-69.

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

7. Andreka H., Mikulas Sz. Lambek calculus and its relational semantics // Journal of Logic, Language and Information. — 1994. — Vol. 3, no. 1. — P. 1-37.

8. Bar-Hillel Y. A quasi-arithmetical notation for syntactic description // Langugage. — 1953. — Vol. 29. — P. 47-58.

9. Bar-Hillel Y., Gaifman C., Shamir E. On categorial and phrase-structure grammars // Bull. Res. Council Israel Sect. F. — 1960. — Vol. 9F. — P. 1-16.

10. Benthem J. van. Semantic parallels in natural language and computation. — Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1988. — 45 p. — (ILLC Pre-publication Series; LP-88-06).

11. Benthem J. van. Semantic parallels in natural language and computation // Logic Colloquium. Granada 1987 / Editors H.-D. Ebbinghaus et al. — Amsterdam: North-Holland, 1989. — P. 331-375.

12. Benthem J. van. Language in Action: Categories, Lambdas and Dynamic Logic. — Amsterdam etc.: North-Holland, 1991. — X, 350 p. — (Studies in Logic and the Foundations of Mathematics; Vol. 130).- 160

13. Birkhoff G. Lattice Theory. — Providence, Rhode Island, 1967. — Русский перевод: Биркгоф Г. Теория решёток / Пер. с англ. В. Н. Салия. — М.: Наука, 1984. — 568 с.

14. Buszkowski W. Undecidability of some logical extensions of Ajdukiewicz-Lambek calculus // Studia Logica. — 1978. —■ Vol. 37. — P. 59-64.

15. Buszkowski W. Compatibility of categorial grammar with an associated category system // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. — 1982. — Vol. 28. — P. 229-238.

16. Buszkowski W. Some decision problems in the theory of syntactic categories // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. — 1982. — Vol. 28. — P. 539-548.

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

18. Buszkowski W. Completeness Results for Lambek Syntactic Calculus // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. — 1986. — Vol. 32. — P. 13-28.

19. Buszkowski W. On the Equivalence of Lambek Categorial Grammars and Basic Categorial Grammars. — Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1993. — 21 p. — (ILLC Prepublication Series; LP-93-07).

20. Carpenter B. Type-Logical Semantics. — Cambridge etc.: The MIT Press, 1997. — XXI, 575 p. — (Language, Speech, and Communication) .

21. Categorial Grammars and Natural Language Structures / Editors R. T. Oehrle, E. Bach, D. Wheeler. — Dordrecht: Reidel, 1988.

22. Chomsky N. Formal properties of grammars // Handbook of Mathematical Psychology / Editors R. D. Luce et al. — New York: Wiley, 1963. — Vol. 2. — P. 323-418.

23. Cohen J. M. The equivalence of two concepts of categorial grammar // Information and Control. — 1967. — Vol. 10. — P. 475-484.

24. Dosen К. A Completeness Theorem for the Lambek Calculus of Syntactic Categories // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. — 1985. — Vol. 31. — P. 235-241.

25. Dosen K. Sequent systems and groupoid models // Studia Logica. — 1988. — Vol. 47, no. 4. — P. 353-385; 1989. — Vol. 48, no. 1. — P. 41-65. — Addenda and corrigenda: 1990. — Vol. 49. — P. 614.

26. Dosen К. A brief survey of frames for the Lambek calculus // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. — 1992, no. 2. — Vol. 38. — P. 179-187.

27. Fuchs L. Partially Ordered Algebraic Systems. — Oxford: Pergamon Press, 1963. — Русский перевод: Фукс JI. Частично упорядо- 162 ченные алгебраические системы / Пер. с англ. И. В. Стеллец-кого. — М.: Мир, 1965. — 342 с.

28. Ginsburg S. The Mathematical Theory of Context-free Languages. — New York: McGraw-Hill, 1966. — Русский перевод: Гинзбург С. Математическая теория контекстно-свободных языков / Пер. с англ. А. Я. Диковского и JI. С. Модиной. — М.: Мир, 1970. — 326 с.

29. Hendriks Н. Studied Flexibility. Categories and Types in Syntax and Semantics: Ph.D. thesis. — Amsterdam, 1993. — (ILLC Dissertation series; 1993-5).

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

31. König E. Der Lambek-Kalkül. Eine Logik für lexikalische Grammatiken: Ph.D. thesis. — Stuttgart, 1990. — 189 p.

32. Lallement G. Semigroups and Combinatorial Applications. — New York etc.: John Wiley & Sons, 1979. — Русский перевод: Лал-леман Ж. Полугруппы и комбинаторные приложения / Пер. с англ. И. О. Корякова. — М.: Мир, 1985. — 440 е.: ил.

33. Lambek J. Lectures on Rings and Modules. — Waltham, Massachusetts, etc.: Blaisdell, 1966. — Русский перевод: Ламбек И. Кольца и модули / Пер. с англ. А. В. Михалёва. — М.: Мир, 1971. — 280 с.

34. Lambek J. From categorial grammar to bilinear logic // Substructural Logics ] Editors K. Dosen, P. Schroeder-Heister. — Oxford: Clarendon Press, 1993. — P. 207-237. — (Studies in Logic and Computation; 2).

35. Moortgat М. Categorial Investigations. Logical and Linguistic Aspects of the Lambek Calculus: Ph.D. thesis. — Dordrecht: Foris, 1988. — XVII, 270 p.

36. Mikulas Sz. The Completeness of the Lambek Calculus with respect to Relational Semantics. — Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1992. — 21 p. — (ILLC Prepublication Series; LP-92-03).

37. Mikulas Sz. Taming Logics: Ph.D. thesis. — Amsterdam, 1995. — 123 p. — (ILLC Dissertation Series; 1995-12).

38. Ono H. Semantics for substructural logics // Substructural Logics / Editors K. Dosen, P. Schroeder-Heister. — Oxford: Clarendon Press, 1993. — P. 259-291. — (Studies in Logic and Computation; 2).- 164

39. Orlowska E. Relational interpretation of modal logics // Polish Acad. Sci. Inst. Philos. Sociol. Bull. Sect. Logic. —1988. —Vol. 17, no. 1. — P. 2-14.

40. Pankratiev N. On the completeness of the Lambek calculus with respect to relativized relational semantics // Journal of Logic, Language and Information. — 1994. — Vol. 3, no. 3. — P. 233-246.

41. Pentus M. Lambek calculus is L-complete. — Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1993. — 36 p. — (ILLC Prepublication Series; LP-93-14).

42. Pentus M. Language completeness of the Lambek calculus // Proceedings of the 9th Annual IEEE. Symposium on Logic in Computer Science: July 4-7, 1994. Paris, France. — Los Alamitos, California: IEEE Computer Society Press, 1994. — P. 487-496.

43. Pentus M. The conjoinability relation in Lambek calculus and linear logic // Journal of Logic, Language and Information. — 1994. — Vol. 3, no. 2. — P. 121-140.

44. Pentus M. Models for the Lambek calculus // Annals of Pure and Applied Logic. — 1995. — Vol. 75, no. 1-2. — P. 179-213.

45. Pentus M. Product-free Lambek calculus and context-free grammars // Journal of Symbolic Logic. — 1997. — Vol. 62, no. 2. — P. 648-660.

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

47. Roorda D. Interpolation in fragments of classical linear logic // The

48. Journal of Symbolic Logic. — 1994. — Vol. 59, no. 2. — P. 419-444.

49. Schütte K. Der Interpolationssatz der intuitionistischen Prädikatenlogik // Mathematische Annalen. — 1962. — Vol. 148. — P. 192-200.

50. Tiede H.-J. Deductive Systems and Grammars: Proofs as Grammatical Structures: Ph.D. thesis. — Indiana University, 1999. — 122 p.

51. Zielonka W. Axiomatizability of Ajdukiewicz-Lambek calculus by means of cancellation schemes // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. — 1981. — Vol. 27, no. 3. — P. 215-224.