by J.R.B. Cockett and R.A.G. Seely
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.