Степан Львович Кузнецов

Формализм категориальных грамматик моделирует синтаксис естественного языка с помощью выводимости в некотором логическом исчислении: предложение признаётся синтаксически корректным, если некоторая построенная по нему формула доказуема. При этом используемые исчисления существенно отличаются от классической логики. А именно, несмотря на то, что в них используются правила, похожие на стандартные modus ponens и теорему о дедукции, не допускаются так называемые структурные правила. А именно, запрещены перестановка (порядок слов имеет значение), ослабление (нельзя произвольно добавлять слова в предложение), сокращение (две копии слова не эквивалентны одной). Такие неклассические логические системы называются субструктурными, наиболее известная из них — исчисление Ламбека (1958).

В рамках мини-курса будет рассказано об исчислении Ламбека и некоторых его расширениях. Мы постараемся соблюсти баланс между неформальным разговором о лингвистических применениях данных формализмов и строгими доказательствами связанных с ними нетривиальных математических результатов. Последние включают в себя как ключевые результаты о свойствах исчисления Ламбека, полученные в 1990-е гг. М.Р. Пентусом, так и недавние результаты лектора о расширениях исчисления Ламбека.

Программа курса

1. Исчисление Ламбека, категориальные грамматики Ламбека. Основы лямбда-исчисления, семантика Монтегю. Интерпретация на алгебре формальных языков, теорема о полноте (доказательство для фрагмента без умножения).
2. Интерполяционная лемма Роорды для исчисления Ламбека. Теорема Пентуса об эквивалентности грамматик Ламбека и контекстно-свободных грамматик.
3. Примеры лингвистических явлений, не охватываемых грамматиками Ламбека. Расширения исчисления Ламбека, их классификация с алгоритмической точки зрения. Алгоритмическая неразрешимость исчисления Ламбека с экспоненциалом.
4. Итерация Клини в исчислении Ламбека. Результаты об алгоритмической неразрешимости и сложности исчислений Ламбека с итерацией Клини (обычного и инфинитарного).