Спецкурс "Исчисление Ламбека"

М. Р. Пентус
2009/2010

В весеннем семестре спецкурс проходит по четвергам в 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 по статье Галатоса и Оно.

Дополнительная литература

  1. Abrusci V. M. Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic // Journal of Symbolic Logic. 1991. Vol. 56, N 4. P. 1403—1451.
  2. 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).
  3. Galatos N. Cut elimination and strong separation for substructural logics: an algebraic approach [Preprint] / N. Galatos, H. Ono. — Denver: University of Denver, Department of Mathematics, 2008. — 56 p. — (M08/26). — http://www.math.du.edu/data/preprints/m0826.pdf
  4. Lambek J. The mathematics of sentence structure // American Mathematical Monthly. 1958. Vol. 65, N 3. P. 154—170.
    Русский перевод: Ламбек И. Математическое исследование структуры предложения // Математическая лингвистика: Сборник переводов / Под ред. Ю. А. Шрейдера и др. М.: Мир, 1964. С. 47—68.
  5. Lecomte A. Towards efficient parsing with proof-nets // EACL 1993, 6th Conference of the European Chapter of the Association for Computational Linguistics, April 21—23, 1993. Utrecht: OTS — Research Institute for Language and Speech, Utrecht University, 1993. P. 269—276.
  6. Moortgat M. Categorial type logics // Handbook of Logic and Language / Editors J. van Benthem and A. ter Meulen. Eslevier/MIT Press, 1997. P. 93—177. 1997.
  7. Savateev Y. Product-free Lambek calculus is NP-complete // Logical Foundations of Computer Science, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3-6, 2009. Proceedings / Editors S. N. Artemov and A. Nerode. Berlin: Springer, 2009. P. 380-394. (Lecture Notes in Computer Science; vol. 5407).

Адрес: http://lpcs.math.msu.su/~pentus/spec2009w.htm
Изменения внесены 11.06.2010.
Мати Рейнович Пентус
Телефон/факс: + 7 - 495 - 939 30 31