一句话：刻画乘法-加法线性逻辑（MALL）中的类型同构，给出含分配律与消去律的更丰富等式理论。
本文刻画了线性逻辑的乘法-加法片段（MALL）中的类型同构，从而也刻画了带有限积的 *-autonomous 范畴中的同构，扩展了 Balat 与 Di Cosmo 关于乘法片段的结果。该刻画导出比乘法情形丰富得多的等式理论，包括分配律和消去律。对于无单位情形，作者依赖 Hughes 与 Van Glabbeek 引入的证明网语法；对于含所有单位的完整 MALL，则通过研究切消与规则交换，使用序列演算将结果推广到完整系统。论文给出了 MALL 类型同构的特征，并揭示了线性逻辑中由加法结构带来的新同构规律。
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.
@article{paperbot3346,
title = {Type Isomorphisms for Multiplicative-Additive Linear Logic},
author = {Rémi Di Guardia and Olivier Laurent},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:24)2025}
}