В весеннем семестре спецкурс проходит по четвергам в 16:45-18:20 в аудитории 14-03. Первая лекция состоялясь 18 февраля 2010 г. Последняя лекция состоялась 13 мая 2010 г.
Краткий конспект похожего спецкурса 2005/2006 года: PostScript, pdf.
Синтаксическое исчисление Ламбека и грамматики Ламбека, устранимость сечения в секвенциальном исчислении Ламбека и её следствия, открытые проблемы, относящиеся к фрагментам и вариантам исчисления Ламбека, языковые и реляционные модели, некоммутативная линейная логика.
15.09.2009
Существует ли быстрый алгоритм для проблемы эквивалентности в исчислении Ламбека?
Пример грамматики Ламбека.
Несеквенциальное исчисление Ламбека.
Секвенциальное исчисление Ламбека L.
Исчисление Ламбека, допускающее пустые антецеденты L*.
Домашнее задание:
(1) ((AB)/B)B) = AB
(2) Существуют ли такие A, B, что A -> (A/B)B?
(3) Для всех ли A, B, C, D верно ((A\B)\C)\D -> C\((B\A)\D)?
(4) Для всех ли A, B, C, D верно A/(B/C) -> (A/(D/C))/(B/D)?
22.09.2009
Эквивалентность несеквенциального и секвенциального исчислений.
Формулировка критерия выводимости в исчислении Ламбека без умножения,
допускающем пустые антецеденты (по статье Алена Леконта 1993 года).
Домашнее задание:
(1) Вывести в несеквенциальном исчислении Ламбека монотонность правого деления.
(2) Вывести в секвенциальном исчислении Ламбека все правила
несеквенциального исчисления Ламбека.
29.09.2009
Критерий Ю. Саватеева для выводимости в исчислении Ламбека без умножения,
допускающем пустые антецеденты; доказательство достаточности.
Домашнее задание:
(1) Доказать, что при ориентации графа, построенного по методу А. Леконта,
получается ориентированное дерево.
(2) Доказать необходимость в критерии Ю. Саватеева.
(3) Выводится ли секвенция ((s/(q/(s\s)))\s)\p -> (q/((s\s)\(s\s)))\p
в исчислении Ламбека, допускающем пустые антецеденты?
06.10.2009
Доказательство необходимость в критерии Ю. Саватеева.
Исчисление Ламбека с единицей L_1.
Правила для операций пересечения и объединения.
Домашнее задание:
(1) Доказать, что можно ограничиться аксиомами с примитивными типами.
(2) Доказать, что для выводимой в L*(/) секвенции в графе, построенном по методу
А. Леконта, у аксиомной связи левый конец на этаж выше, чем правый.
13.10.2009
Устранимость сечения в L*, L, L_1.
Операция dual.
L-модели.
Домашнее задание:
(1) Доказать полноту L(\,/) относительно L-моделей, используя алфавит Tp(\,/).
20.10.2009
Формулировка задания (2), заданного 6 октября, в терминах теории графов.
Задача о том, что для выводимой в L*(/) секвенции в графе, построенном по методу
А. Леконта, для аксиомной связи с положительной чётной глубиной правого конца
либо между концами аксиомной связи имеется вершина меньшей глубины,
либо правый сосед правого конца имеет меньшую глубину.
Размер грамматики Ламбека.
Задача о построении по L(\)-грамматике КС-грамматики с полиномиальным числом вспомогательных символов.
Задача о построении автомата с магазинной памятью по L(\,/)-грамматике.
27.10.2009
Исчисление LP.
R-модели (на тотальном бинарном отношении).
Домашнее задание:
(1) Доказать полноту L(\,/) относительно L-моделей над двухбуквенным алфавитом.
(2) Доказать полноту LP относительно моделей над свободными коммутативными полугруппами.
(3) Корректность L* относительно R-моделей.
(4) Можно ли выразить / через объединение, пересечение, дополнение,
произведение и обратное?
10.11.2009
Релятивизованные R-модели для L* (на рефлексивном транзитивном бинарном отношении).
Частично упорядоченные полугруппы.
Полугруппы с делением.
Однозначность задания левого и правого частных в полугруппе с делением.
Полнота L* относительно нерелятивизованных R-моделей (без доказательства).
Релятивизованные R-модели для L (на иррефлексивном транзитивном бинарном отношении).
Полнота L относительно релятивизованных R-моделей (без доказательства).
Задача о полноте L относительно класса всех R-моделей на конечных строгих линейных порядках.
Задача о полноте L* относительно класса всех R-моделей на конечных нестрогих линейных порядках.
Корректность L с пересечением и объединением относительно R-моделей и L-моделей.
Задача о плноте L с пересечением и объединением.
Устранимость сечения для L с пересечением и объединением.
Исчисление L со связкой \Uparrow (определение 4.22).
Лингвистический пример поднятия типа.
Функция prop.
Корректность L* относительно интуиционистской логики высказываний.
Счётчик положительных вхождений примитивного типа.
Счётчик отрицательных вхождений примитивного типа.
Корректность L* относительно интерпретации в свободной абелевой группе.
Корректность L* относительно интерпретации в свободной группе.
24.11.2009
"Лемма о ромбе".
Критерии совместимости в L и L* (без доказательства).
Критерий совместимости в L(\) (без доказательства).
Каждую выводимую секвенцию можно получить подстановкой из некоторой выводимой тонкой секвенции.
Интерполяционное свойство L* (теорема 6.33).
Домашнее задание:
(1) Можно ли выразить / через объединение, пересечение, дополнение,
произведение и обращение?
(2) Выводится ли секвенция (p2 \ (p1 (p1 \ p2))) \ p2 -> p2
в исчислении Ламбека, допускающем пустые антецеденты?
Какими средствами это можно доказать?
(3) Выводится ли секвенция (((p2\p3)\((p1\p2)\p4))\((p1\p3)\p4))\(p3\p1) -> p3\p1
в исчислении Ламбека, допускающем пустые антецеденты?
Какими средствами это можно доказать?
(4) Доказать, что \overline\#(\Gamma) \geq \overline\#(A), если секвенция
\Gamma -> A выводится (теорема 6.22).
08.12.2009
Грамматики Ламбека.
Исчисление Lcut.
Построение КС-грамматики по грамматике Ламбека.
15.12.2009
Интерполяционное свойство L(\).
18.02.2010
Построение грамматики Ламбека (над L(\,/)) по КС-грамматике без пустого слова.
25.02.2010
Построение грамматики Ламбека (над L(/)) хорновского ранга 1 по КС-грамматике без пустого слова.
04.03.2010
Сети (для L*(\,/)) у А. Леконта и Ю. Саватеева.
Сети с областями (для L*).
11.03.2010
Простое типовое лямбда-исчисление.
18.03.2010
Категориальная грамматика.
25.03.2010
Некоммутативная линейная логика.
Исчисление SPNCL.
Исчисление SPNCL'.
01.04.2010
Различные определения сетей доказательства для фрагментов L и L*.
15.04.2010
Несеквенциальные исчисления для фрагментов исчисления Ламбека.
Домашнее задание:
(1) Можно ли из L_H(\cdot,\backslash) удалить
(A \cdot B) \cdot C \to A \cdot (B \cdot C)?
(2) Можно ли из L_H(\cdot,\backslash) удалить
A \cdot (B \cdot C) \to (A \cdot B) \cdot C?
(3) Допустимость правила A->B\C, C->D |- A->B\D,
правила A->B\C, D->E |- A->(E\B)\(D\C)
и правила A->B\C, D->E |- C\D->A\(B\E)
в системе L_H(\) с аксиомами A->A (рефлексивность) и B\C->(A\B)\(A\C),
правилом A->B, B->C |- A->C
и правилом A->B, C->D |- B\C->A\D (монотонность).
(4) Допустимость правил L_H(\) в системе, заданной рефлексивностью,
мнотонностью и тремя правилами из предыдущей задачи.
(5) Корректность L_H(\) относительно секвенциального исчисления L.
(6) Доказать полноту упрощённого секвенциального исчисления
(с пустым \Delta, с примитивными сукцедентами, где возмонжно).
22.04.2010
Доказательство эквивалентности несеквенциального и секвенциального исчислений
для фрагмента исчисления Ламбека с одним делением.
Домашнее задание:
(1) Найти несеквенциальное исчисление для исчисления Ламбека с одним делением,
допускающего пустые антецеденты.
29.04.2010
Построение контрмодели на конечной полугруппе с делением по статье Галатоса и Оно
(с. 6-8, 24-31, 34-35, 49-53).
Домашнее задание:
(1) Выписать таблицу умножения в контрмодели для p \to p \cdot p.
06.05.2010
Доказательство лемм о свойствах отображения g по статье Галатоса и Оно.
Адрес:
http://lpcs.math.msu.su/~pentus/spec2009w.htm
Изменения внесены 11.06.2010.
Мати Рейнович Пентус
Телефон/факс: + 7 - 495 - 939 30 31