Type Isomorphisms for Multiplicative-Additive Linear Logic

TL;DR

This work provides a complete equational characterization of type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), extending known results from the multiplicative fragment. It develops a two-pronged approach: a syntactic, proof-net-based analysis for unit-free MALL, complemented by a sequent-calculus framework with unit-handling to extend to full MALL; it then transfers the syntactic insights to star-autonomous categories with finite products. Central to the method is reducing formulas to distributed, unit-free forms, analyzing isomorphisms via restricted unit patterns, and exploiting proof-nets to obtain a canonical, ax-unique representation of isomorphisms. The result is a sound and complete equational theory for isomorphisms in MALL and, by translation, in the corresponding categorical settings, offering precise tools for semantic reasoning and library-based type search in related logics. The work also outlines pathways to extend these results to exponentials and broader categorical frameworks, highlighting both the potential and limitations of current proof-net techniques for full linear logic.

Abstract

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.

Figures (16)

• Figure 1: Schematic representation of the second case of the proof of \ref{['lem:betafrom_etato']}
• Figure 2: Graphs from an example of a proof-net: from left to right $\mathcal{G}_{\lambda_1}$, $\mathcal{G}_{\lambda_2}$ and $\mathcal{G}_{\{\lambda_1;\lambda_2\}}$
• Figure 3: Illustration of $\mathrel{\triangleleft}$ (\ref{['def:dupcut']}) and correspondence with $\with-cut$ cut-elimination
• Figure 4: Identity proof-nets (from left to right: atom, $\parr\backslash\otimes$ and $\with\backslash\oplus$)
• Figure 5: Non bipartite proof-net (top-left), non full proof-net (top-right) and one of their compositions yielding the identity proof-net (bottom) (jump edges not represented)

Theorems & Definitions (154)

• Definition 2.1: Slice
• Definition 2.2
• Definition 2.3
• Remark 2.4
• Definition 2.5
• Remark 2.6
• Remark 2.7
• Definition 2.8: Isomorphism
• Lemma 2.9
• proof