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