by J.R.B. Cockett and R.A.G. Seely
Abstract:
There are many situations in logic, theoretical computer science, and
category theory where two binary operations---one thought of as a (tensor)
``product'', the other a ``sum''---play a key role. In distributive and
*-autonomous categories these operations can be regarded as, respectively,
the and/or of traditional logic and the times/par of (multiplicative) linear
logic. In the latter logic, however, the distributivity of product over sum
is conspicuously absent: this paper studies a ``linearization'' of that
distributivity which is present in both case. Furthermore, we show that
this weak distributivity is precisely what is needed to model Gentzen's cut
rule (in the absence of other structural rules) and can be strengthened in
a natural way to generate *-autonomous categories. We also point out
that this ``linear'' notion of distributivity is virtually orthogonal
to the usual notion as formalized by distributive categories.
This is the journal version of the similarly named paper appearing in the Proceedings of the Durham conference (1991): M.P. Fourman, P.T. Johnstone, A.M. Pitts, eds., Applications of Categories to Computer Science, London Mathematical Society Lecture Note Series 177 (1992) 45 - 65.
The paper has been rewritten, including more details and several examples, including shifted tensors, Span categories, and categories of modules of a bialgebra. In addition, an error regarding a previous claim that distributive categories are weakly distributive is corrected.
This version is the "corrected" version, with the corrections mentioned "in proof" in the journal version (Journal of Pure and Applied Algebra, Vol 114 (1997) pp 133-173) incorporated into the text.