Интуиционистская линейная логика первого порядка и гиперграфовые языки

Некоммутативные субструктурные логики имеют несколько точек соприкосновения с теорией формальных языков. С одной стороны, такие логики, например, исчисление Ламбека, используются как механизм задания формальных языков в категориальных грамматиках. С другой стороны, формальные языки возникают как модели субструктурных логик; основной результат в этом направлении, доказанный М.Р. Пентусом, гласит, что исчисление Ламбека корректно и полно относительно языковой семантики.
В докладе предполагается обсудить аналогичные взаимосвязи между субструктурными логиками первого порядка и гиперграфовыми языками. В первой части доклада будет предложено определение гиперграфовых L-грамматик, основанных на произвольной первопорядковой логике L (в секвенциальном формате). Оно обобщает понятие MILL1-грамматик – категориальных грамматик, основанных на мультипликативной интуиционистской линейной логике первого порядка MILL1. Последние рассматривались в работах [Μοοt, 2014], [Slavnov, 2023]. Будет показана связь гиперграфовых MILL1-грамматик, а также грамматик над интуиционистской линейной логикой первого порядка ILL1 с порождающими гиперграфовыми грамматиками. В качестве следствия будет дан ответ на открытый вопрос из [Moot, 2014] о классе языков, задаваемых строковыми MILL1-грамматиками; в частности, будет показано, что этот класс содержит NP-полный язык.
Во второй части доклада будет дано определение языковой семантики для логики MILL1, в рамках которой формулы интерпретируются гиперграфовыми языками, а мультипликативная конъюнкция (тензор) линейной логики интерпретируется операцией параллельной композиции. Эта операция хорошо известна в теории графовых грамматик в контексте HR-алгебр [Courcelle, 1990]. Будет установлена теорема о корректности и полноте для негативного фрагмента MILL1 (с помощью аналога конструкции [Buszkowski, 1982]). Вопрос полноты всей логики MILL1 относительно гиперграфово-языковой семантики остается открытым.
Доклад основан на препринте https://arxiv.org/abs/2502.05816.