# What is the proper name for “compact closed” multiplicative intuitionistic linear logic?

Multiplicative intuitionistic linear logic (MILL) has only multiplicative conjunction $\otimes$ and linear implication $\multimap$ as connectives. It has models in symmetric monoidal closed categories.

Compact closed categories are symmetric monoidal closed categories in which every object $A$ has a dual $A^*$ and $A \multimap B \cong A^* \otimes B$. Thought of as a resource, $A^*$ is a debt, owing someone an $A$. Is there a special name for MILL when these conditions hold? ͏ ͏

-

This logic was studied by Masaru Shirahata, "A Sequent Calculus for Compact Closed Categories". He just calls it "CMLL", but points out it is equivalent in provability to MLL (classical multiplicative linear logic) with tensor and par identified. Note that the direction tensor $\vdash$ par is commonly called "MIX", so this is also MLL + MIX as an isomorphism.

-

Compact closed categories are models of classical linear logic when tensor and par collapse.

As an aside, I'm not sure that the particular resource interpretation you're suggesting genuinely works, since linear logic offers a unified and very subtle view of action and resource. If you want a pure resource interpretation of logic, you may need to look at bunched implications (ie, at categories which simultaneously have a monoidal and cartesian closed structure).

James Brotherston has investigated a version of this logic which is directly inspired by the debt/credit view, called "classical BI", both model-theoretically and proof-theoretically (though not yet categorically).

-
Hmm...since BI is a conservative extension of IMLL, I would think that classical BI would also be conservative extension of CMLL, so that the resource interpretations of the multiplicative connectives coincide. Though reading Brotherston and Calcagno's paper (arxiv.org/PS_cache/arxiv/pdf/1005/1005.2340v2.pdf), it's not clear to me that this is the case. For example, is the CMLL equivalence $(A \multimap 1) \multimap 1 \equiv A$ valid in every CBI model? –  Noam Zeilberger Sep 1 '10 at 22:05
And I think the answer is no, because they distinguish the unit of the monoid from an element $\infty$ "that characterises the result of combining an element with its dual involution". The equivalence will be valid in CBI models coming from Abelian groups, but not in general. Brotherston and Calcagno give a bunch of examples of interesting models that don't come from Abelian groups -- but that is the form of the "credits and debits" interpretation. –  Noam Zeilberger Sep 1 '10 at 22:21

Ross Duncan calls it mCQL (for "Multiplicative Categorical Quantum Logic") in this 2006 PhD thesis Types for Quantum Computing. That might be a bit specific to your taste, but it is quite defendable, seeing that compact categories give precisely the means to study the "logic" of the resources in quantum mechanical protocols.

-