<p>I don't know much about category theory, but perhaps this will be helpful. The equations governing the graphical diagrams for biproduct categories [Selinger] are exactly equivalent to those for atomic flows [Gundersen] in deep inference proof theory [Guglielmi], in the negation-free fragment. These proof systems are equivalent to the monotone sequent calculus in a natural way [Brunnler, Jerabek].</p>

<p>Unfortunately there seems to be few links drawn to category theory in the latter area.</p>

<p>Selinger, P. www.mscs.dal.ca/~selinger/papers/graphical.pdf , page 45.</p>

<p>Gundersen, T. tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf , page 74.</p>

<p>Guglielmi, A. alessio.guglielmi.name/res/cos/</p>

<p>Brunnler, K. www.iam.unibe.ch/~kai/Papers/n.pdf</p>

<p>Jerabek, E. www.math.cas.cz/~jerabek/papers/cos.pdf</p>

CC BY-SA 3.0
2012-10-03T09:19:16.817Z
Thanks a lot! I'm a little too busy to follow the references right away, but I'll look at them soon.
Neel Krishnaswami
CC BY-SA 3.0
2012-10-02T14:43:21.277Z
2012-10-02T14:43:21.277Z
Anupam Das
<p>Samson Abramsky and I wrote a paper about the proof theory of compact categories with biproducts.</p>

<blockquote>
  <p>Abramsky, S. and Duncan, R. (2006) "A Categorical Quantum Logic",
  Mathematical Structures in Computer Science 16 (3).
  10.1017/S0960129506005275</p>
</blockquote>

<p>The ideas were later developed a bit further in this book chapter:</p>

<blockquote>
  <p>Duncan, Ross (2010) "Generalised Proof-Nets for Compact Categories
  with Biproducts" in Semantic Techniques in Quantum Computation,
  Cambridge University Press, pp70--134 arXiv:0903.5154v1</p>
</blockquote>

<p>The full details are there, but the short version is that your logic is inconsistent, because you have a zero proof for every implication, and the rest of your proofs are equivalent to "matrices", where the matrix entries are the proofs in the biproduct-free part of the logic.  Speaking without the caveats required to make this precise, the resulting category of proofs is the free biproduct category on some category of axioms.</p>

CC BY-SA 3.0
2012-10-05T09:11:26.703Z
A small addendum the above: there is no need to be alarmed by the fact that we treat compact categories as opposed to general categories.  In fact the additive and multiplicative parts of this logic interact rather weakly.  The parts concerning biproducts should carry over quite generally.
Ross Duncan
CC BY-SA 3.0
2012-10-03T16:29:24.370Z
2012-10-03T16:29:24.370Z
Ross Duncan
<p>A category has <a href="http://ncatlab.org/nlab/show/biproduct">biproducts</a> when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts?</p>

<p>Perhaps the best-known example is the category of vector spaces, in which the direct sum and direct product constructions give the same vector space. This means vector spaces and linear maps are a slightly degenerate model of linear logic, and I am curious what a type theory which accepts this degeneracy would look like. </p>

CC BY-SA 3.0
2011-09-09T09:39:05.080Z
Maybe Cockett & Seely? Perhaps Intro to Linear Bicategories, or something else from http://www.math.mcgill.ca/~rags/.
Dave Clarke
CC BY-SA 3.0
2011-09-09T11:33:25.857Z
Perhaps the "bi-" in "bi-products" is misleading: it's not some 2-categorical thing, it's just what happens when the same objects are both products and coproducts (plus some coherence conditions) in ordinary categories.
Neel Krishnaswami
CC BY-SA 3.0
2011-09-09T11:47:02.043Z
Maybe their paper: FINITE SUM – PRODUCT LOGIC.
Dave Clarke
CC BY-SA 3.0
2011-09-09T14:55:02.470Z
*Slightly* degenerate? I believe identifying products and coproducts implies identifying the initial and terminal object, which are typically empty and singleton types, interpreted as trivial falsehood and truth, respectively. In linear logic I think this collapses the entire additive half of the logic to a self-dual operation with an identity that annihilates both multiplications. On the other hand, the multiplicative fragment tends to be the more constructive half of linear logic, so maybe this does lead somewhere interesting...
C. A. McCann
CC BY-SA 3.0
2012-10-02T20:35:37.123Z
@camccann: There is math outside logic. In commutative algebra the initial and terminal object typically agree, as well as coproducts and products. For example, the trivial abelian group is both initial and terminal. An object which is both initial and terminal is called a zero object. Have a look at abelian categories to get some intuition of how this all works.
Andrej Bauer
CC BY-SA 3.0
2012-10-02T21:56:10.980Z
In fact I am not 100% sure there is a difference between a category with biproducts (and initial/final objects) and an additive category (abelian category minus some technical information).
cody
<reference-request><lo.logic><pl.programming-languages><type-theory><ct.category-theory>
Proof theory of biproducts?
Neel Krishnaswami
# Proof theory of biproducts?

(Asked by: username_0 on 2011-09-09)

A category has [biproducts](http://ncatlab.org/nlab/show/biproduct) when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts?

Perhaps the best-known example is the category of vector spaces, in which the direct sum and direct product constructions give the same vector space. This means vector spaces and linear maps are a slightly degenerate model of linear logic, and I am curious what a type theory which accepts this degeneracy would look like.

**Tags:** reference-request, lo.logic, pl.programming-languages, type-theory, ct.category-theory

> **Comments:**
> **username_1**: Maybe Cockett & Seely? Perhaps Intro to Linear Bicategories, or something else from http://www.math.mcgill.ca/~rags/.  
> **username_0**: Perhaps the "bi-" in "bi-products" is misleading: it's not some 2-categorical thing, it's just what happens when the same objects are both products and coproducts (plus some coherence conditions) in ordinary categories.  
> **username_1**: Maybe their paper: FINITE SUM – PRODUCT LOGIC.  
> **username_2**: *Slightly* degenerate? I believe identifying products and coproducts implies identifying the initial and terminal object, which are typically empty and singleton types, interpreted as trivial falsehood and truth, respectively. In linear logic I think this collapses the entire additive half of the logic to a self-dual operation with an identity that annihilates both multiplications. On the other hand, the multiplicative fragment tends to be the more constructive half of linear logic, so maybe this does lead somewhere interesting...  
> **username_3**: @camccann: There is math outside logic. In commutative algebra the initial and terminal object typically agree, as well as coproducts and products. For example, the trivial abelian group is both initial and terminal. An object which is both initial and terminal is called a zero object. Have a look at abelian categories to get some intuition of how this all works.  
> **username_4**: In fact I am not 100% sure there is a difference between a category with biproducts (and initial/final objects) and an additive category (abelian category minus some technical information).  

---

## 2 answers

### Answer by username_6 on 2012-10-03. Score: 8 | Accepted answer

Samson Abramsky and I wrote a paper about the proof theory of compact categories with biproducts.

> Abramsky, S. and Duncan, R. (2006) "A Categorical Quantum Logic",
> Mathematical Structures in Computer Science 16 (3).
> 10.1017/S0960129506005275

The ideas were later developed a bit further in this book chapter:

> Duncan, Ross (2010) "Generalised Proof-Nets for Compact Categories
> with Biproducts" in Semantic Techniques in Quantum Computation,
> Cambridge University Press, pp70--134 arXiv:0903.5154v1

The full details are there, but the short version is that your logic is inconsistent, because you have a zero proof for every implication, and the rest of your proofs are equivalent to "matrices", where the matrix entries are the proofs in the biproduct-free part of the logic. Speaking without the caveats required to make this precise, the resulting category of proofs is the free biproduct category on some category of axioms.

> **Comments:**
> **username_6**: A small addendum the above: there is no need to be alarmed by the fact that we treat compact categories as opposed to general categories.  In fact the additive and multiplicative parts of this logic interact rather weakly.  The parts concerning biproducts should carry over quite generally.  

---

### Answer by username_5 on 2012-10-02. Score: 7

I don't know much about category theory, but perhaps this will be helpful. The equations governing the graphical diagrams for biproduct categories [Selinger] are exactly equivalent to those for atomic flows [Gundersen] in deep inference proof theory [Guglielmi], in the negation-free fragment. These proof systems are equivalent to the monotone sequent calculus in a natural way [Brunnler, Jerabek].

Unfortunately there seems to be few links drawn to category theory in the latter area.

Selinger, P. www.mscs.dal.ca/~selinger/papers/graphical.pdf , page 45.

Gundersen, T. tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf , page 74.

Guglielmi, A. alessio.guglielmi.name/res/cos/

Brunnler, K. www.iam.unibe.ch/~kai/Papers/n.pdf

Jerabek, E. www.math.cas.cz/~jerabek/papers/cos.pdf

> **Comments:**
> **username_0**: Thanks a lot! I'm a little too busy to follow the references right away, but I'll look at them soon.  

---

