Deep inference and probabilistic coherence spaces

Applied Categorical Structures. 2012. Vol. 20. No. 3. P. 209–228.

Blute R., Panangaden P., Slavnov S. A.

В статье предлагается категорная модель системы глубокого вывода BV, опеределенной Гульеми. В системах глубокого вывода реализована идея дедукций внутри формулы на любой глубине . Стандартные правила исчислений секвенций применимы только к корню дерева подформул, тогда как в этих новых системах можно вносить изменения в любой позиции дерева. В частности, глубокий вывод позволяет синтаксическое описание логик, для которых не существует исчисления секвенций. Одной их таких систем явлеется BV — расширение линейной логики с помощью некоммутативной самодвойственной связки. Цель нашей статьи — моделирование этой логики. Наше определение основывается на понятии линейного функтора, предложенного Кокетом и Сили. BV-категория — это линейно дистрибутивная категория, возможно с отрицанием, с добавочным тензорным произведением, которое, рассмотренное как бифунктор, оказывается линейным с условием вырождения. Мы показываем, что из этого простого определения следуют ключевые изоморфизмы теории.  Мы рассматриваем жираровскую категорию вероятностных пространств когерентности и показываем, что она допускает самодвойственную моноидальную структуру в дополнение к *-автономной структуре, указанной Жираром. Эта структура превращает категорию в BV-категорию. Мы предполагаем, что эта структура интересна и сама по себе, как и большинство разумно устроенных некоммутативных операторов.

Ключевые слова: категории, categorical logic, deep inference systems, linear logic, probabilistic coherence spaces, категорная логика, системы глубокого вывода, линейная логика, вероятностные пространства когерентности, основания математики