查看文章

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 two natural ways to generate full distributivity and ∗-autonomous categories.