Доказательство теории бипродуктов?

15

Категория имеет бипродукты, когда одни и те же объекты являются как продуктами, так и копроизведениями. Кто-нибудь исследовал теорию доказательств категорий с бипродуктами?

Возможно, наиболее известным примером является категория векторных пространств, в которой конструкции прямой суммы и прямого произведения дают одно и то же векторное пространство. Это означает, что векторные пространства и линейные отображения являются слегка вырожденной моделью линейной логики, и мне любопытно, на что была бы похожа теория типов, которая принимает это вырождение.

reference-request lo.logic pl.programming-languages type-theory ct.category-theory Нил Кришнасвами
источник
1
Может быть, Cockett & Seely? Возможно Введение в Линейные Бикатегории, или что-то еще от math.mcgill.ca/~rags .
Дэйв Кларк
Возможно, «bi» в «bi-products» вводит в заблуждение: это не какая-то 2-категориальная вещь, это просто то, что происходит, когда одни и те же объекты являются одновременно продуктами и сопутствующими продуктами (плюс некоторые условия согласованности) в обычных категориях.
Нил Кришнасвами
Может быть, их бумаги: FINITE SUM - ЛОГИКА ПРОДУКТА
Дэйв Кларк
Слегка вырожденный? Я считаю, что идентификация продуктов и сопутствующих продуктов подразумевает идентификацию исходного и конечного объекта, которые обычно являются пустыми и одноэлементными типами, интерпретируемыми как тривиальная ложь и истина, соответственно. В линейной логике я думаю, что это сводит всю аддитивную половину логики к самодвойственной операции с тождеством, которое уничтожает оба умножения. С другой стороны, мультипликативный фрагмент имеет тенденцию быть более конструктивной половиной линейной логики, поэтому, возможно, это приводит к чему-то интересному ...
CA McCann
3
@camccann: математика вне логики. В коммутативной алгебре исходный и конечный объект обычно совпадают, а также копроизведены и продукты. Например, тривиальная абелева группа является как начальной, так и конечной. Объект, который является как начальным, так и конечным, называется нулевым объектом. Посмотрите на абелевы категории, чтобы понять, как все это работает.
Андрей Бауэр

Ответы:

8

Мы с Самсоном Абрамским написали статью о теории доказательств компактных категорий с бипродуктами.

Абрамский, С. и Дункан, Р. (2006) "Категориальная квантовая логика", Математические структуры в информатике 16 (3). 10,1017 / S0960129506005275

Позднее идеи были развиты в этой главе книги:

Дункан, Росс (2010) «Обобщенные прутки для компактных категорий с бипродуктами» в семантических методах квантовых вычислений, издательство Кембриджского университета, стр. 70--134. ArXiv: 0903.5154v1

Все подробности есть, но короткая версия состоит в том, что ваша логика противоречива, потому что у вас есть нулевое доказательство для каждого следствия, а остальные ваши доказательства эквивалентны «матрицам», где записи в матрице являются доказательствами в бипродукте Свободная часть логики. Если говорить без предостережений, требуемых для уточнения, то полученная категория доказательств является категорией бесплатного бипродукта для некоторой категории аксиом.

Росс Дункан
источник
Небольшое дополнение к вышесказанному: нет необходимости беспокоиться о том, что мы относимся к компактным категориям, а не к общим категориям. На самом деле аддитивная и мультипликативная части этой логики взаимодействуют довольно слабо. Части, относящиеся к бипродуктам, должны переноситься довольно широко.
Росс Дункан
7

Я не знаю много о теории категорий, но, возможно, это будет полезно. Уравнения, управляющие графическими диаграммами для категорий бипродуктов [Selinger], в точности эквивалентны уравнениям для атомных потоков [Gundersen] в теории доказательств с глубокими выводами [Guglielmi] во фрагменте без отрицаний. Эти системы доказательств естественным образом эквивалентны монотонному исчислению секвенций [Brunnler, Jerabek].

К сожалению, в последней области, похоже, мало ссылок на теорию категорий.

Селинджер, П. www.mscs.dal.ca/~selinger/papers/graphical.pdf, стр. 45.

Гундерсен, T. tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf, стр. 74.

Гульельми, А. alessio.guglielmi.name/res/cos/

Бруннлер, К. www.iam.unibe.ch/~kai/Papers/n.pdf

Джерабек, Э. www.math.cas.cz/~jerabek/papers/cos.pdf

Анупам Дас
источник
Большое спасибо! Я слишком занят, чтобы сразу же следить за ссылками, но скоро посмотрю на них.
Нил Кришнасвами