Основы исчисления Ламбека
- Реляционные модели для исчисления Ламбека с пересечением и константами (arXiv)
Автор :Степан Л. Кузнецов
Аннотация: мы рассматриваем реляционную семантику (R-модели) для исчисления Ламбека, расширенного пересечением и явными константами для нуля и единицы. Для его варианта без констант и ограничения, запрещающего пустые антецеденты, Андрека и Микулаш (1994) доказывают сильную полноту. Мы показываем, что без этого ограничения она не работает, но, с другой стороны, доказываем слабую полноту для нестандартной интерпретации констант. Для стандартной интерпретации даже слабая полнота не работает. Слабый результат полноты распространяется на бесконечную настройку для так называемых итерационных делений (звезда Клини при делении). Мы также доказываем строгие результаты полноты для фрагментов без произведений.
2. Грамматики исчисления Ламбека с перестановкой: распознавание мощности и связи с системами сложения ветвящихся векторов с состояниями (arXiv)
Автор : Тихон Пшеницын
Аннотация: В [Van Benthem, 1991] доказано, что все замыкания перестановок контекстно-свободных языков могут быть порождены грамматиками над исчислением Ламбека с правилом перестановки (LP-грамматики); однако, насколько нам известно, не установлено, выполняется ли обратное утверждение или нет. В этой статье мы показываем, что LP-грамматики эквивалентны линейно ограниченным системам сложения ветвящихся векторов с состояниями и дополнительной памятью (сокращенно lBVASSAM), которые представляют собой модифицированные системы сложения ветвящихся векторов с состояниями. Затем приводится пример такого lBVASSAM, который генерирует неполулинейный набор векторов; это приводит к тому, что LP-грамматики генерируют больше, чем перестановочные замыкания контекстно-свободных языков. Более того, эквивалентность LP-грамматик и lBVASSAM позволяет представить нормальную форму для LP-грамматик и, как следствие, доказать, что LP-грамматики эквивалентны LP-грамматикам без произведения.
3. Нормализация с помощью оценки для исчисления Ламбека (arXiv)
Автор:Никколо Велтри
Аннотация:Синтаксическое исчисление Ламбека представляет собой дедуктивную систему для мультипликативного фрагмента интуиционистской некоммутативной линейной логики. В качестве мелкозернистого исчисления ресурсов он имеет множество применений, в основном в формальных вычислительных исследованиях естественных языков. Эта статья вводит исчисление бета-эта-длинных нормальных форм для производных в исчислении Ламбека с мультипликативной единицей и конъюнкцией среди его логических связок. Приведение к нормальной форме следует стратегии нормализации путем оценки (NbE): (i) оценить вывод в модели Крипке исчисления Ламбека; (ii) извлечь нормальные формы из полученных семантических значений. Реализация алгоритма NbE требует наличия сильной монады в крипке-интерпретации положительных формул по аналогии с расширением интуиционистской пропозициональной логики с ложностью и дизъюнкцией. Алгоритм NbE также может быть реализован с небольшими вариациями исчислений для связанных субструктурных логик, таких как мультипликативная и двойная интуиционистская линейная логика (MILL и DILL).
