Грамматики Ламбека: неклассическая логика для математической лингвистики

Степан Кузнецов

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

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

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

1. Исчисление Ламбека, категориальные грамматики Ламбека. Основы лямбда-исчисления, семантика Монтегю. Интерпретация на алгебре формальных языков, теорема о полноте (доказательство для фрагмента без умножения).

2. Интерполяционная лемма Роорды для исчисления Ламбека. Теорема Пентуса об эквивалентности грамматик Ламбека и контекстно-свободных грамматик.

3. Примеры лингвистических явлений, не охватываемых грамматиками Ламбека. Расширения исчисления Ламбека, их классификация с алгоритмической точки зрения. Алгоритмическая неразрешимость исчисления Ламбека с экспоненциалом.

4. Итерация Клини в исчислении Ламбека. Результаты об алгоритмической неразрешимости и сложности исчислений Ламбека с итерацией Клини (обычного и инфинитарного).

Материалы: https://vk.com/doc-91031095_678509239

Кузнецов Степан Львович — доктор физико-математических наук.

Летняя школа «Современная математика», 20-24 июля 2024 г.

Источник: vk.com

Комментарии: