15
$\begingroup$

A category has biproducts 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.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Maybe Cockett & Seely? Perhaps Intro to Linear Bicategories, or something else from math.mcgill.ca/~rags. $\endgroup$
    – Dave Clarke
    Sep 9, 2011 at 9:39
  • $\begingroup$ 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. $\endgroup$
    – Neel Krishnaswami
    Sep 9, 2011 at 11:33
  • $\begingroup$ Maybe their paper: FINITE SUM – PRODUCT LOGIC. $\endgroup$
    – Dave Clarke
    Sep 9, 2011 at 11:47
  • $\begingroup$ 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... $\endgroup$
    – C. A. McCann
    Sep 9, 2011 at 14:55
  • 3
    $\begingroup$ @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. $\endgroup$
    – Andrej Bauer
    Oct 2, 2012 at 20:35

2 Answers 2

Reset to default
8
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Ross Duncan
    Oct 5, 2012 at 9:11
7
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks a lot! I'm a little too busy to follow the references right away, but I'll look at them soon. $\endgroup$
    – Neel Krishnaswami
    Oct 3, 2012 at 9:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.