Введение
1 Исчисление Ламбека и порождающие грамматики 14
1.1 Исчисление Ламбека L 14
1.2 Исчисление L 18
1.3 Формальные языки и операции над ними 18
1.4 Модели исчисления Ламбека 20
2 Верхняя оценка длины совмещающего типа в исчислении L 22
2.1 Критерий совместимости в исчислении Ламбека 22
2.2 Схема построения совмещающего типа 25
2.3 Построение совмещающего типа 30
3 Нижняя оценка длины совмещающего типа в исчислении L 40
3.1 Мультипликативная циклическая линейная логика 40
3.2 Отношение совместимости в исчислении MCLL 42
3.3 Упрощённые сети доказательства 45
3.4 Оценки на число вхождений атомов в совмещающий тип 47
3.5 Доказательство нижней оценки 52
4 Исчисление Ламбека с операциями замещения 57
4.1 Исчисление Ламбека с единицей 57
4.2 Разрывные операции над языками
4.3 Исчисление Ламбека с операциями замещения 59
4.4 Модели исчисления Ламбека с операциями замещения 64
5 Отношение совместимости в исчислении Ламбека с операциями замещения 66
5.1 Отношение совместимости и интерпретация в свободной абелевой группе 66
5.2 Доказательство критерия совместимости 72
6 О пересечении языков, порождаемых разрывными грамматиками Ламбека, с автоматными языками 84
6.1 Секвенциальное исчисление DL 84
6.2 Категориальные грамматики, основанные на вариантах исчисления Ламбека 91
6.3 Конечные автоматы и задаваемые ими языки 94
6.4 Пересечение с автоматными языками: описание конструкции 95
6.5 Доказательство корректности конструкции 98
Предметный указатель 108
Литература
