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

• Пентус, Мати Рейнович
• доктор физико-математических наук
• 2000

Оглавление диссертации доктор физико-математических наук Пентус, Мати Рейнович

Введение

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

Список литературы диссертационного исследования доктор физико-математических наук Пентус, Мати Рейнович, 2000 год

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.