Об отношении совместимости в исчислении Ламбека и в его варианте с операциями замещения

• Автор: Сорокин, Алексей Андреевич
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2014
• Место защиты: Москва
• Количество страниц: 120 с.

Оглавление
Введение
1 Исчисление Ламбека и порождающие грамматики
1.1 Исчисление Ламбека Ь
1.2 Исчисление Ъ*
1.3 Формальные языки и операции над ними
1.4 Модели исчисления Ламбека
2 Верхняя оценка длины совмещающего типа в исчислении

2.1 Критерий совместимости в исчислении Ламбека
2.2 Схема построения совмещающего типа
2.3 Построение совмещающего типа
3 Нижняя оценка длины совмещающего типа в исчислении

3.1 Мультипликативная циклическая линейная логика
3.2 Отношение совместимости в исчислении МСЬЬ
3.3 Упрощённые сети доказательства
3.4 Оценки на число вхождений атомов в совмещающий тип .
3.5 Доказательство нижней оценки
4 Исчисление Ламбека с операциями замещения
4.1 Исчисление Ламбека с единицей
4.2 Разрывные операции над языками

4.3 Исчисление Ламбека с операциями замещения
4.4 Модели исчисления Ламбека с операциями замещения
5 Отношение совместимости в исчислении Ламбека с операциями замещения
5.1 Отношение совместимости и интерпретация в свободной
абелевой группе
5.2 Доказательство критерия совместимости
6 О пересечении языков, порождаемых разрывными грамматиками Ламбека, с автоматными языками
6.1 Секвенциальное исчисление БЬ
6.2 Категориальные грамматики, основанные на вариантах
исчисления Ламбека
6.3 Конечные автоматы и задаваемые ими языки
6.4 Пересечение с автоматными языками: описание конструкции
6.5 Доказательство корректности конструкции
Предметный указатель
Литература

Введение
Общая характеристика работы
Актуальность темы
Диссертация посвящена исследованию отношения совместимости в различных вариантах исчисления Ламбека. В работе формулируются верхняя и нижняя оценка на длину совмещающего типа для исчисления Ламбека Ь и доказывается критерий совместимости типов для исчисления Ламбека с операциями замещения. Также в работе исследуется класс языков, порождаемых грамматиками, основанными на исчислении Ламбека с операциями замещения.
Исчисление Ламбека Ь было введено И. Ламбеком в работе [18] для формального описания синтаксиса естественных языков. Типы исчисления Ламбека строятся из счётного множества примитивных типов с помощью двуместных связок — умножения, а также левого и правого деления. Два типа Ап В исчисления Ламбека называются совместимыми, если существует такой тип С, что обе секвенции А —> С и В —> С являются выводимыми. В этом случае тип С называется совмещающим для типов А и В. Отношение совместимости было впервые введено (под другим названием) в работе [18], где было доказано, что оно является отношением эквивалентности.
В работе [27] был доказан критерий совместимости типов в исчислении Ламбека и коммутативном исчислении Ламбека, сформулированный в терминах интерпретаций типов исчисления Ламбека в свободной группе, порождённой примитивными типами. В работах [11] и [20] были получены критерии совместимости, соответственно, для неаесоциатив-

причём для всех j ^ Z выполняется равенство [CjJ = £ (типы Со и С; могут отсутствовать). Если тип Со существует, применим следствие
2.1 к типам В и Со, получим, что найдётся тип Д, такой что выполняются следующие условия: L h В —> Д, L h ф((Со))В —> D и Z(A) ^ Z(A) + 2/(Со). Если тип Со отсутствует, положим D — В, также определим типы D2 — В2, ■ ■ ■, Di = В[.
Теперь для каждого j = 1,...,/ — 1 применим следствие 2.1 к типам Д и Cj, получим, что существуют типы такие что
для каждого j = 1,...,/ — 1 выполняются следующие утверждения: L h Dj -> Dj, L В DjCj ->■ D'j и /(£>') < /(Д) + 2/(0,). Если тип С существует, аналогичным образом поступим и с типами Д и С, иначе положим D — Ci-
Положим Л2 = Д • ... • Д. Используя правила (cut) и (• —»)
нетрудно вывести, что L I- ф{{А)) —> А и L В <^>(1Л|) —» Д- Осталось

доказать оценку на длину типа А^. В самом деле, /(А) = Е КАО ^

£(КА) + 2/(0) ^ (/(А) + 2/(Со)) + 2/(СО + Е(/(Д) + 2/(0,)) -
г=1 г=
Е КА) + 2 Е КО = Е КА) + Е К<К(0)) = КФ((А)))- Лемма дока-
г=1 г=0 i=l г=
зана. □
Таким образом, мы можем оценить длины типов Аг, А на рисунке
2.1. Следующая лемма позволяет оценить также и длины типов А и А-
Лемма 2.11. Для всякого типа А £ Тр существует тип А, такой что L h А А, L В ф((А)) —> А и /(А) ^ |/2(Л) + 1(A).
Доказательство. В силу леммы 2.7 можно считать, что А не содержит отрицательных умножений. Докажем лемму индукцией по построению типа А. База индукции: А = р € Рг, тогда А = р и утверждение леммы выполняется.
На шаге индукции возможны три случая: А = В ■ С, А = В/С и А — С В. В силу симметричности левого и правого делений достаточно