We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus in *-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo. This yields a much richer equational theory involving distributivity and cancellation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek. We use the sequent calculus to extend our results to full MALL, including all units, thanks to a study of cut-elimination and rule commutations.

翻译：我们刻画了线性逻辑的乘法-加法片段（MALL）中的类型同构，进而刻画了具有有限积的*-自伴范畴中的类型同构，这一结果将Balat和Di Cosmo关于乘法片段的结果进行了推广。由此得到了一個更为丰富的等式理论，涉及分配律和消去律。无单位的情形是通过利用Hughes和Van Glabbeek引入的证明网语法得到的。我们使用相继式演算将结果推广到完整的MALL（包含所有单位），这得益于对切割消去和规则交换的研究。