• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Статья

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-категорию. Мы предполагаем, что эта структура интересна и сама по себе, как и большинство разумно устроенных некоммутативных операторов.