Спецкурс «Категориальные грамматики Ламбека»

Задачки

• Часть 1 (13.11.2013)
• Часть 2 (обновлено 24.04.2014)

Краткое содержание прошедших лекций

02.10.2013

Типовое λ-исчисление: типы, термы, α-конверсия, β- и η-редукции. Свойство Чёрча — Россера и теорема о сильной нормализуемости (без доказательства). Нормальная форма λ-терма. Эквивалентность λ-термов. Теоретико-множественная интерпретация λ-исчисления, теорема о корректности и полноте (без доказательства). Семантика Монтегю (пример: «Иван любит Марью»). [2]

09.10.2013

Более сложный пример: «Нарцисс любит себя». Исчисление Ламбека. Категориальные грамматики Ламбека. Семантическая разметка; восстановление целевого терма по семантической разметке и выводу секвенции в исчислении Ламбека (соответствие Карри – Говарда для исчисления Ламбека).

16.10.2013

Интуиционистское исчисление высказываний (импликативный фрагмент, Int_→) в гильбертовской форме и в формате естественного вывода, их эквивалентность (задача). Семантика Брауэра — Гейтинга — Колмогорова (BHK-интерпретация). Соответствие Карри — Говарда. Декартово произведение типов и конъюнкция. Каррирование. Генценовская система для исчисления Ламбека. Теорема об устранении сечения (без доказательства). Погружение исчисления Ламбека в Int_→∧ (задача).

23.10.2013

Следствия из теоремы об устранении сечения: свойство подформульности, элементарные фрагменты, обратимость правил с одной посылкой, разрешимость.
Обзор результатов М. Р. Пентуса и Ю. В. Саватеева об алгоритмической сложности фрагментов исчисления Ламбека (без доказательств). [3]
Интерпретация исчисления Ламбека на полугруппе формальных языков (L-модели). Исчисление Ламбека в гильбертовской форме.
Теорема М. Р. Пентуса об L-полноте исчисления Ламбека (без доказательства).[4]
Теорема В. Бушковского о полноте для случая без операции умножения. [5]

30.10.2013

Гильбертовская форма исчисления Ламбека с одним делением (по Ю. В. Саватееву) — семантическое доказательство эквивалентности. Контекстно-свободные грамматики и семантика Монтегю для них.

06.11.2013

Схема доказательства теоремы об устранении сечения. Счётчики числа вхождений переменных. Интерполяционные леммы Крейга и Роорды.

20.11.2013

Тонкие секвенции. Интерпретация исчисления Ламбека в свободной полугруппе. Интерполяционная лемма для тонких секвенций. BR-лемма (формулировка). Исчисление Lcut_m, его связь с ограниченным фрагментом исчисления Ламбека. Теорема Пентуса: всякий язык, задаваемый категориальной грамматикой Ламбека, контекстно-свободен. [6]

27.11.2013

BR-лемма (доказательство). Построение по контекстно-свободной грамматике эквивалентной ей грамматики Ламбека (начало).

04.12.2013

Форма Грейбах для контекстно-свободных грамматик (без доказательства). Построение по контекстно-свободной грамматике эквивалентной ей грамматики Ламбека.

11.12.2013

Разбор некоторых задач.

12.02.2014

Напоминание: исчисление Ламбека, категориальные грамматики Ламбека; контекстно-свободные грамматики и языки. Язык Дика (множество правильных скобочных последовательностей). Алгоритм Кока-Янгера-Касами (метод динамического программирования) для проверки принадлежности слова данному контекстно-свободному языку. Исчисление L(\). Сети доказательств Саватеева для исчисления L(\) (формулировка).

19.02.2014

Сети доказательств Саватеева — критерий выводимости в исчислении L(\). Читал Ю. В. Саватеев.

26.02.2014

Построение по L(\)-грамматике эквивалентной ей контекстно-свободной грамматики полиномиального размера. Полиномиальный по времени работы алгоритм проверки выводимости секвенции в исчислении L(\).

05.03.2014

Построение эквивалентной грамматики Ламбека по контекстно-свободной грамматике в форме Хомского (по В. Бушковскому в изложении М. Р. Пентуса).

12.03.2014

Построение эквивалентной грамматики Ламбека по контекстно-свободной грамматике в форме Хомского (по В. Бушковскому в изложении М. Р. Пентуса) — окончание.
Мультипликативная циклическая линейная логика (MCLL).

19.03.2014

Отношение эквивалентности типов. Теорема Болговой: два типа эквивалентны в исчислении L(\) только в том случае, когда они совпадают.
Перевод типов исчисления Ламбека в формулы MCLL. ♮-счётчик. Консервативность MCLL над L* (исчислением Ламбека, допускающим пустые левые части секвенций).

26.03.2014

Более сложные примеры из английского языка (The girl whom John loves hates John).
Сети вывода (proof nets) для MCLL (теоретико-графовый критерий выводимости в мультипликативной линейной логике).

02.04.2014

Теорема: всякий контекстно-свободный язык (возможно, содержащий пустое слово) порождается некоторой L*(\)-грамматикой.

09.04.2014

Исчисление Ламбека с единицей (L₁). Теорема: все L₁-языки контекстно-свободны. Полиномиальный алгоритм проверки выводимости в исчислении L₁(\).

16.04.2014

Совместимые типы в исчислении Ламбека. Свойства отношения совместимости: рефлексивность, симметричность, свойство ромба, транзитивность; отношение совместимости — конгруэнция. Критерий совместимости в исчислениях L и L* (в терминах интерпретаций в свободной полугруппе). [7]

23.04.2014

Примеры неоднозначного присвоения типов. Грамматики с однозначным присвоением типов. Теорема Сафиуллина (начало).

30.04.2014

Теорема Сафиуллина (описание конструкции).

07.05.2014

Поднятие типа. Полиморфное присвоение типов/термов и поднятие для описания синтаксиса сочинительных союзов (and, or) в английском языке.

14.05.2014

Теорема Мининой: необходимое условие эквивалентности формул в MCLL.

21.05.2014

Заключительная лекция.

Литература