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

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

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

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

ПЕНТУС МАТИ РЕИНОВ

ИСЧИСЛЕНИЕ ЛАМБЕКА И ФОРМАЛЬНЫЕ ГРАММАТИКИ

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

Автореферат

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

Москва — 1996

МШг'

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

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

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

А. А. Разборов — кандидат физико-математических наук, Н. К. Верещагин Ведущая организация — Санкт-Петербургское отделение

Математического института им. В. А. Стеклова Российской академии наук

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

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

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

Автореферат разослан 1996 г.

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

профессор В. Н. Чубариков

^т.з.-шк л .о

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

Актуальность темы. Вопрос о месте категориальных грамматик в иерархии Хомского возник в конце 50-х — начале 60-х годов. В 1960 году Бар-Хиллел, Гайфман и Шамир [1] доказали, что формальный язык может быть задан некоторой базовой категориальной грамматикой тогда и только тогда, когда он является контекстно-свободным. Они высказали гипотезу о том, что то же самое имеет место для грамматик Ламбека, т. е. для категориальных грамматик, основанных на введенном в 1958 году И. Ламбе-ком [2] синтаксическом исчислении с тремя связками (умножение или конкатенация языков, левое деление и правое деление).

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

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

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

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

4. Buszkowski W. Generative power of categorial grammars // Categorial Grammars and Natural Language Structures ] Editors 11. T. Oehrle, E. Bach, and D. Wheeler. — Dordrecht: Reidel, 1988. — P. 69-94.

5. Buszkowski W. On generative capacity of the Lambek calculus // Logics in AI / Editor J. van Eijck. — Berlin: Springer, 1991. — P. 139-152.

И. ван Бентхем в книге [6] приводит вышеупомянутую гипотезу в качестве открытой проблемы современной математической лингвистики.

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

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

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

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

Доказано, что категориальные грамматики, основанные на любом из перечисленных ниже исчислений:

• синтаксическом исчислении Ламбека,

• исчислении Ламбека с пустыми антецедентами,

• исчислении Ламбека с единицей,

• мультипликативном фрагменте циклической линейной логики,

порождают в точности все контекстно-свободные языки.

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

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

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

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

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

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

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

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

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

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

Пусть М — непустое множество, называемое алфавитом, Обозначим через М* множество всех слов в алфавите М. Множество всех непустых слов в алфавите М. будем обозначать посредством М+.

Определение. Контекстно-свободная грамматика есть четверка (Т, УУ, с, где Т и УУ — два непересекающихся конечных множества, (Т — элемент множества УУ, а И — конечное множество кон-текстно-свободпых правил вида а => и, где а £ УУ и и 6 (ТиУУ)+.

Слово и/ непосредственно выводимо из слова ш в грамматике {Т,УУ,с,7£), если ю — У\аь2, и>' = ихииг для некоторых VI, У2 (Е (Т и УУ)+ и а и есть правило из 'Я. Мы говорим, что м' выводимо из т в (Т, УУ, <т, %), если существует последовательность хпа, • • • "'п, такая, что и>,- € (7~ и УУ)*, из = 1Уо, V)' = ю„

и для каждого г < п — 1 слово од+1 непосредственно выводимо из слова од. Языком, порожденным грамматикой (Т,УУ,(г,71), (обозначение: 0(Т, УУ, а, 71)) называется множество всех слов в алфавите Т, выводимых в рассматриваемой грамматике из однобуквенно-го слова а.

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

В § 1.2, § 1.3 и § 1.4 приводятся определения, связанные с синтаксическим исчислением Ламбека, обозначаемым через Ь,

Предполагаем, что задано счетное множество Уаг = {Р1,Р2,РЗ) • • •}• Элементы этого множества будем называть примитивными типами.

Синтаксические типы (или просто типы) строятся из примитивных типов с помощью трех бинарных операторов \, /, называемых соответственно умножением, левым делением и правым делением. Обозначим через Тр множество всех типов.

Большими буквами А, В, ... будем обозначать типы исчисления Ламбека, большими греческими буквами — конечные (возможно пустые) последовательности типов.

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

Аксиомами исчисления Ламбека служат все секвенции вида Р| 14, где р,- € Уаг.

Исчисление Ламбека имеет следующие правила:

Г -+Л А^В ( ч ТАВА -> С , ч

(_+*)> тчл тл . п (* "*)'

ГД —► А'В к " Т(А.В)А^С

АН —» В , П,А П -> А ГВА С /\ ч

тГЩв ^ где п * л' гп(л\д)д —► с

II А^В , л „ , . ц А ГВА — С ,, ч

—щ /)• где П ф Л, г(вМ)ПД^с (/

П — В Г В А — А

ГИД

(аи).

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

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

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

Определение. Для каждого примитивного типа р 6 Уаг определим два отображения и из множества Тр в множество N натуральных чисел:

1, если р = q, О, если q £ Уаг ир/д, #р (?) ^ 0, если q € Уаг, #+(Л.Д) ^ #+(Л) + #+(5), #р-(Л.Л) ^ #-(Л)+#р"(В), #+(А\В) ^ #~(А) +#+(В), #;(А\В) ^ #+(Л) + #-(5), #+(А/В) ^ #+(Л) + #;(5), ф-(А/В) - #р-(Л)+#+(Л),

Определение. Исчисление Ь* получается из первоначального исчисления Ь, если отбросить требование нспустоты антецедента секвенции и условие П ф Л в правилах (—► \) и (—> /). Определение. Исчисление Ламбека с единицей Ь^ получается из Ь* при добавлении константы 1, аксиомы —► 1 и правила

Г1А —► С

В § 1.5 дается определение категориальных грамматик Ламбека, основанных на синтаксическом исчислении Ламбека. Определение. Грамматика Ламбека есть тройка (Т, II, >), где Т — некоторое конечное множество (алфавит), II — тип исчисления Ламбека и > — некоторое конечное бинарное отношение > С Тр х Т.

Язык, порожденный грамматикой Ламбека (Т,Н,*>), определяется как множество всех непустых слов ¿1.. Лп в алфавите Т, для которых существует такая выводимая в исчислении Ламбека

секвенция В\.. .Вп —* Я, что для любого г < п выполняется B^ >4,-. Обозначим этот язык через £¿(7", II, >).

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

Обозначим через _Г(Уаг) свободную группу, порожденную счетным множеством примитивных типов {рх, р2) Рз, • • •}• Единицей построенной свободной группы ^(Уаг) является пустое слово е.

Для каждого элемента и £ .Р(Уаг) определим |и| как длину приведенного слова для и.

В § 2.2 доказывается корректность исчисления Ламбека относительно интерпретации в свободной группе:

Лемма 2. Если секвенция Г —► С выводима в исчислении Ламбека, то [Г] = [С].

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

В § 2.3 получен некоторый факт о свободных группах, на который опирается доказательство ключевой леммы из § 5.3:

Лемма 3. Если ы,..., и„ € Г(Уаг), п>1 и щ .. .ип — £, то найдется индекс к<п, такой, что < тах(|и*|, |и<;+1|).

В третьей главе вводится понятие тонкой секвенции. Определение. Секвенция П —* А называется тонкой тогда и только тогда, когда для любого р 6 Уаг справедливы неравенства #+(П-Л)<1и#-(И-Л)<1.

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

В четвертой главе (§ 4.1) приводится доказательство интерполяционной теоремы Крейга для исчисления Ламбека.

Лемма 5. Пусть Ь Ь Ф0Ф С, где Ф 6 Тр*, 0 е Тр+, Ф 6 Тр* и С € Тр. Тогда существует такой тип Е, что

(i) L ье - E;

(ii) L h Ф£Ф — C;

(iii) для любого примитивного типа р £ Var имеет место неравенство #+(Е) < min(#+(6), #+(С) + #р"(ФФ));

(iv) для любого примитивного типа р 6 Var имеет место нера-

венство #"(£) < min(#p-(0), #р (С) + #+(ФФ)).

Это доказательство, основанное на методе Маехары и Шют-те, является простой модификацией доказательства Д. Роорды, данного для варианта исчисления Ламбека, допускающего пустые антецеденты. В § 4.2 доказывается, что в случае тонкой секвенции длина интерполянта, построенного по методу Маехары и Шют-те, равна длине приведенного слова, представляющего в свободной группе интерполируемую часть исходной секвенции. Этот факт будет существенно использоваться в § 5.3.

Пятая глава посвящена доказательству основного результата диссертации — гипотезы о том, что языки, задаваемые грамматиками Ламбека, контекстно-свободны. В § 5.1 конструктивно строится контекстно-свободная грамматика, соответствующая произвольно заданной грамматике Ламбека. При этом роль вспомогательного алфавита в построенной контекстно-свободной грамматике играет некоторое конечное множество типов исчисления Ламбека, а контекстно-свободные правила считываются с выводимых в исчислении Ламбека секвенций ограниченной длины. Определение. Для любых двух натуральных чисел mus определим конечное множество типов Tp(m, s) и конечное множество последовательностей типов Ls(m, s):

Tp(m, s) ^ {ЛбТр|Уаг(Л)С{Р1,...,р,}и1И||<т};

Ls(m,s) ^ {П GTp(m,s)+ | ||П|| < 2m}.

Рассмотрим произвольную грамматику Ламбека (Т,Н,>). Поскольку определение языка, порождаемого этой грамматикой, затрагивает только конечное число типов, найдутся такие положительные целые числа m и s, что H € Tp(m,s) и если B>t для некоторого t £ Т, то В € Tp(m, s).

Построим теперь искомую контекстно-свободную грамматику (Т,Щ<т,П):

W ^ Tp(m,s), сг ^ Я,

п ^ {В =>t I t GT и B>t)U

и{Л =» Г I А € Тр(т, в), Г 6 Ls(m, а), и L Ь Г -+ А}.

В § 5.4 доказывается, что CL(T,H,>) - G(T,W,<r,K).

Теорема 2. Пусть (T,H,t>) — некоторая грамматика Ламбека. Тогда язык £¿(7", Я,>) является контекстно-свободным.

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

Определение. Пусть £ С {\,/,*} и С есть либо £(£), либо £*(£). Скажем, что исчисление С обладает интерполяционным свойством, если для любой выводимой в С секвенции вида А —* С, где А € Тр(£) и Се Тр(£), найдется такой тип В £ Тр(Е), что

(i) С b А В;

(ii) С Ь В С;

(iii) Var(B) С Уаг(Л) U Var(C).

Доказывается, что фрагменты L(\,/), L(\) и L(/) обладают интерполяционным свойством (§ 6.1). (То же для остальных элементарных фрагментов известно из работ Д. Роорды [7,8].)

7. Roorda D. Resource Logics: Proof-theoretical Investigations: PhD thesis / Fac. Math, and Сотр. Sc., University of Amsterdam. —Amsterdam, 1991.

8. Roorda D. Interpolation in fragments of classical linear logic // The Journal of Symbolic Logic. — 1994. — Vol. 59, № 2. — P. 419-444.

Кроме того, автором вводится понятие обобщенного интерполяционного свойства, представляющее интерес во фрагментах без умножения.

Определение. Пусть £ С {\, /, •} и С есть либо ¿(2), либо Скажем, что исчисление С обладает обобщенным интерполяционным свойством, если для любой выводимой в С секвенции П —> С, где П 6 Тр(£)* и С € Тр(Е), найдется такой тип В £ Тр(Е), что

(О С Ь П — В;

(и) С Ь В - С;

(¡11) Уаг(В) С Уаг(П) и Уаг(С).

Доказывается, что фрагменты Ь(\) и Ь{/) обладают обобщенным интерполяционным свойством (§ 6.3), а £(\, /) этим свойством не обладает (§ 6.2).

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

В восьмой главе приводится определение совместимых синтаксических типов из книги [6] и доказывается, что два типа совместимы тогда и только тогда, когда их интерпретации в свободной группе равны. Это дает положительный ответ на поставленный в работе [6] вопрос о разрешимости отношения совместимости.

Определение. Два типа Ли В совместимы тогда и только тогда, когда найдется тип С, такой, что Ь А С п Ь\~ В С.

Теорема 4. Типы А и В совместимы тогда и только тогда, когда ¡Л] = [В].

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

В § 9.1 приводится определение мультипликативного фрагмента циклической линейной логики. В § 9.2 доказывается корректность мультипликативной циклической линейной логики относительно интерпретации в свободной группе. В § 9.3 определяются тонкие секвенции в мультипликативной циклической линейной логике. В § 9.4 доказывается интерполяционная теорема. В § 9.5 определяется понятие грамматики, основанной на мультипликативной циклической линейной логике. В § 9.6 устанавливается теорема о совпадении класса языков, порождаемых грамматиками, основанными на мультипликативном фрагменте циклической линейной логики, с классом всех контекстно-свободных языков.

Определим множество формул Fm(», Р, 1, J.) исчисления CLL как наименьшее множество, удовлетворяющее следующим условиям:

• 16 Fm(., р, 1,1) и 1 G Fm(., р, 1,1);

• если pi G Var, то р{ G Fm(., р, 1, ±) и р/- е Fm(», р, 1, ±);

• если А G Fm(», р, 1,1) и В G Fin(., р, 1, -L), то (Л.5) € Fm(., Р, 1, ±) и (АрВ) G Fm(., Р, 1,1).

Секвенции исчисления CLL имеют вид —► Г, где Г G Fm(», р, 1, !.)*. IIa множестве Fm(», р, 1, ±) определена операция

(О^ГтС-РД^^Гт^рД,!), сопоставляющая каждой формуле ее отрицание.

(1)х J.

(I)1 1

(Pi)1 rt

(р.1)1 Pi

(.А.В)1 ((j3)хр(А)х)

(ApB)L

Аксиомами исчисления CLL служат все секвенции вида —> (pi)L pi, где pi G Var, а также секвенция —+ 1.

Исчисление CLL имеет следующие правила. - ГЛВД р) -»ГЛ —» ДА н #)

Т(АрВ)А 4 Г(у1.В)Д

ГА , ч -+ ГА —► (А)х А , х (rotate) -_Гд М)

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

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

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

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

3. Pentus М. Lambek grammars are context free: Препринт / РАН. Математический институт им. В. А. Стеклова, отдел математической логики, серия Математическая логика и теоретическая информатика. — М., 1992. — № 8. — 10 с.

4. Pentus М. The conjoinability relation in Lambek calculus and linear logic: ILLC Prepublication Series, ML-93-03. — Amsterdam: Institute for Logic, Language and Computation, University of Amsterdam, 1993. — 20 p.

5. Pentus M. Lambek grammars are context free // Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science. — IEEE Computer Society Press, 1993. — P. 429-433.

6. Pentus M. The Conjoinability Relation in Lambek Calculus and Linear Logic // Journal of Logic, Language and Information. — 1994. — Vol. 3, № 2. — P. 121-140.