Multiplicative Intuitionistic Linear Logic

January 18, 2007

Multiplicative Intuitionistic Linear Logic

Posted by John Baez

$MathML-enabled post (click for more details).$

The following guest post is by Mike Stay:

I’ve been trying to understand multiplicative intuitionistic linear logic (MILL) from a category-theoretic perspective, and I think I’ve figured out what’s going on — see below. As Richard Guy would say, this is “probably well-known to those who know it.” If you’re one of those, I’d appreciate any references you can think of.

$MathML-enabled post (click for more details).$

In what follows I’ll say “a MILL,” since we say “a symmetric monoidal closed category”. I’ll use the sequent calculus presentation instead of the natural deduction presentation.

Here are the inference rules, copied from this paper by Benton, Bierman, de Paiva, and Hyland:

(1)

\frac{}{A\vdash A} Identity

$\,$

(2)

\frac{\Gamma,A,B,\Delta\vdash C}{\Gamma,B,A,\Delta\vdash C} Exchange

$\,$

(3)

\frac{\Gamma\vdash B \quad \B,\Delta\vdash C}{\Gamma,\Delta\vdash C} Cut

$\,$

(4)

\frac{\Gamma\vdash A}{\Gamma,I\vdash A}(I_L)

$\,$

(5)

\frac{}{\vdash I}(I_R)

$\,$

(6)

\frac{\Gamma,A,B\vdash C}{\Gamma,A\otimes B\vdash C}(\otimes_L)

$\,$

(7)

\frac{\Gamma\vdash A\quad \Delta\vdash B}{\Gamma,\Delta\vdash A\otimes B}(\otimes_R)

$\,$

(8)

\frac{\Gamma\vdash A\quad \Delta,B\vdash C}{\Gamma,\Delta,A\multimap B\vdash C}(\multimap_L)

$\,$

(9)

\frac{\Gamma,A\vdash B}{\Gamma\vdash A\multimap B}(\multimap_R)

A MILL $M$ is, apparently, a poset. (Recall that a poset is a category with at most one morphism, called $\le$ , between any pair of objects). The objects are propositions or resources. $A \le B$ if $B$ is deducible from $A$ .

There are three functors of particular note:

the tensor product, denoted either by the crossed circle ( $\otimes$ ) or by a comma (,). [The comma, as far as I can tell, is a remnant from the standard presentation of intuitionistic (nonlinear) logic.]
the external Hom functor, denoted by a turnstile $(\vdash)$ , written \vdash in TeX. [Note that the Hom set here is really more of a truth value, since given any two objects $A and B$ , either $A \le B$ or it isn’t.]
finally, the internal hom functor, denoted by a dash with a circle at the right end $(\multimap)$ , written \multimap in TeX.

A line of the proof is a functor $M^n\to Set$ for some $n\ge 0$ . The Hom functor is one of these, but there are more complicated ones, like the first line in the $(\multimap_R)$ rule:

(10)

\array{ \Gamma,A\vdash B: &M^3 &\to &Set\\ &(\Gamma,A,B) &\mapsto &Hom(\Gamma\otimes A,B) }

The inference rules themselves are natural transformations between such functors.

In a symmetric monoidal closed category, we have two natural isomorphisms

(11)

\frac{A \otimes I}{A} u, unit law \quad\quad \frac{(A \otimes B) \otimes C}{A \otimes (B \otimes C)} a, associator

satisfying the pentagon and triangle equations. In a poset, these equations are satisfied automatically.

We have a natural isomorphism

(12)

\frac{A\otimes B}{B\otimes A} b, braiding

satisfying the hexagon equations and $b^2=1$ . As before, in a poset, these equations are satisfied automatically.

The final natural isomorphism is currying:

(13)

\frac{A\otimes B\vdash C}{A\vdash B\multimap C} c, curry.

Now we have

Identity: this is a natural isomorphism between the constant functor $M\to Set$ taking every object to the one-element set $\{\cdot\}$ and the functor that assigns to each object $A$ its set of endomorphisms $A\vdash A$ (which, since this is a poset, can contain at most one element). Since identity morphisms always exist, $A\vdash A \cong \{\cdot\}$ .
Exchange: follows from the braiding.
Cut: this is just composition of morphisms. [Just as there’s a Hom functor, there’s a composition natural transformation.]
$(I_L), (I_R)$ : follow from the unit law
$(\otimes_L), (\otimes_R)$ : follow from the functoriality of tensor
$(\multimap_L)$ : this is “internal composition”
$(\multimap_R)$ : this is exactly currying

As I asked before, if you’ve seen this somewhere, could you post a reference, please?

Posted at January 18, 2007 8:53 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1114

14 Comments & 1 Trackback

Re: Multiplicative Intuitionistic Linear Logic

This seems like the perfect opportunity to make my first post here. I’m a graduate student at McGill university in Montreal, and I’m co-supervised by Michael Barr (of *-autonomous categories fame).

Although I’m a new student this year, and still in the process of figuring these things out, I can nevertheless point you to a paper that I’m sure you’ll find useful.

The paper is written by Robert Seely, who’s an adjunct professor here at McGill , and also a former student of Dr. Barr. It’s called “Linear logic, *-autonomous categories and cofree coalgebras “, and you can find it here…

http://www.math.mcgill.ca/rags/nets/llsac.ps.gz

Posted by: Brendan on January 18, 2007 11:37 PM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

$MathML-enabled post (click for more details).$

Thank you! This paper begins by implicitly defining a linear category to be the kind of category that makes this analogy precise:

(1)

linear logic : linear category :: typed \lambda-calculus : cartesian closed category.

He sketches how this is to be done, then declares

Since the required equations may be easily generated from the above recipe (and are in essence to be found in the references given, for the most part), and since this process is familiar (for instance, to that of Lambek and Scott [1986] for $\lambda$ –calculus), I shall avoid the messy notational baggage needed to make all the details explicit, by stating boldly and without discussion:

1.4 Definition. A linear category G is a *-autonomous category with finite products.

In my case, I’m interested in the multiplicative intuitionistic fracment of linear logic. According to Wikipedia’s article on linear logic, we leave out par ( par ), why not (?), and bottom (⊥) because they require multiple conclusions (e.g. they’re separated by commas on the right of the turnstile) even when the assumptions have only one conclusion. We also leave out the additive conjuctions to get the multiplicative fragment.

I just discovered that this seems to be example 2.4.2 in Blute and Scott’s paper Category theory for linear logicians.

Posted by: Mike Stay on January 19, 2007 2:27 AM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

I knew that Seely’s paper didn’t give an explicit construction, but since you asked for any references in the area, I posted it.

Something I haven’t had access to are the Springer Lecture Notes by Michael Barr on *-autonomous categories published around 1979. This is probably a good place to look since it’s referenced very often by other papers that talk about categorical linear logic.

By the way, thanks for posting the link to the paper of Blute and Scott, it looks quite good.

Posted by: Brendan on January 19, 2007 3:27 AM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

$MathML-enabled post (click for more details).$

According to Bierman’s 1995 paper “What is a Categorical Model of Linear Logic?”, Seely’s original definition does not model all equal proofs (ie, up to $\beta\eta$ -equality) with equal morphisms, and then proposes a modification to achieve that.

Posted by: Neel Krishnaswami on January 19, 2007 3:04 AM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

This isn’t precisely relevant to your question, Mike, but I can’t resist talking about it here.

Over on another thread, I just mentioned that in July I’ll be visiting Paul-André Melliès, who works on linear logic from a category-theoretic viewpoint. I met him at Geometry of Computation ‘06. Anyway, I just looked at the transparencies for a talk of his:

Paul-André Melliès, Functorial boxes in string diagrams.

I think you should look at them! First of all, they’re all about string diagrams and linear logic. Second of all, they develop a string diagram notation for morphisms in a bunch of different categories related by functors, instead of just one category.

Posted by: John Baez on January 19, 2007 3:28 AM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

Looking at the diagrams where Melliès introduces negation, i.e., page 80 onwards, reminds me of Charles Peirce’s use of ‘cuts’ or ‘seps’ in his existential graphs. Melliès’ diagrams add an extra dimension to capture inference.

For a category theoretic treatment of the existential graphs see the third and fourth papers listed under ‘Research’ here, by Geraldine Brady and Todd Trimble.

Posted by: David Corfield on January 19, 2007 8:57 AM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

There is a well-developed line of thought, originating in work by Lambek on residuated categories (biclosed monoidal categories without units), see the last reference here , where particular fragments of classical logic are related to particular types of structured categories. Lambek’s basic insight was that many free categories-of-given-structure-type (such as symmetric monoidal closed categories) may be presented by means of an appropriate sequent calculus, where morphisms of the free structure are equivalence classes of sequent deductions. He then suggests a powerful application of Gentzen’s cut elimination algorithm to study the problem of deciding equality in free structured categories, commonly known as a “coherence problem.”

I think there is an embarrassing richness of references to this basic idea, but one off the top of my head is Szabo’s Algebra of Proofs (as cited here). It’s well-known among specialists that a number of his claimed solutions to coherence problems are flawed, but the material on constructing categorical semantics of sequent calculi is fine, and gives a good basic survey at the time of writing.

My thesis was on the coherence problem for SMC categories, which is connected with Girard’s linear logic. You might have a look at the paper by Blute, Cockett, Seely, and myself (see Seely’s web page) – the circuit diagrams used there have a strong string-diagrammatic flavor.

Posted by: Todd Trimble on January 19, 2007 2:55 PM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

… the tensor product, denoted either by the crossed circle or by a comma. [The comma, as far as I can tell, is a remnant of the standard presentation of intuitionistic (nonlinear) logic.]

I like to think of the comma as denoting the tensor product of the monoidal strictification of the smc category where these sequent deductions are interpreted. The objects of the strictification of a monoidal category M are finite lists of objects of M, whence the commas to separate the list entries, and M strong-monoidally embeds in its strictification as the subcategory of single-entry lists.

In other words, in giving categorical semantics of (deductions of) sequents A1, A2, …, An |- B, I prefer to interpret the turnstyle as an arrow in the strictification of M (or, if you prefer, in the monoidal multicategory canonically associated with M).

In classical Gentzen sequent calculus, commas can appear on both sides of the turnstyle; if they appear on the left, they denote conjunction, but if they appear on the right, they denote disjunction. In the *-autonomous semantics of linear logic, commas on the left are interpreted as tensor products, but commas on the right are interpreted as “pars” (in the language of Girard) which are “DeMorgan dual” to tensors. Cockett and Seely introduced the notion of weakly distributive category to model this situation of two tensor products which are related by a tensorial strength (which is used to interpret the cut rule).

Posted by: Todd Trimble on January 19, 2007 6:41 PM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

Hi Todd, can you post any links elaborating this monoidal strictification business?

I’m a programming languages guy (and hence a proof theorist by default), who only dabbles in category theory. However, treating the comma and the tensor as the same (or even the comma and conjunction in CCCs) has always rubbed me the wrong way – it fails to respect the distinction between a judgement and a connective (ie, the internalization of a judgement). A better treatment of that would be of great interest to me.

Posted by: Neel Krishnaswami on January 19, 2007 9:58 PM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

$MathML-enabled post (click for more details).$

Hi Neel. I don’t recall ever explicitly reading about this interpretation of the comma, but it’s a little song and dance which I might have picked up from reading various papers of Joachim (Jim) Lambek, and other things.

Lambek as you may know was an early pioneer with a broad range of research in, among other things, the theory of rings and modules, category theory, proof theory, type theory… Due to this confluence of interests, he was probably the first to observe that Gentzen sequents $A_1, ..., A_n \to B$ had a module-theoretic interpretation, as multilinear functions $A_1 \times \ldots \times A_n \to B$ of bimodules over a ring. This enabled him to interpret the rule of inference $\frac{\Gamma, A, B, \Delta \to C}{\Gamma, A \otimes B, \Delta \to C}$ in terms of the standard Bourbaki yoga of multilinear functions, where functions multilinear in $A$ and $B$ are in natural bijection with functions linear in the tensor product $A \otimes B$ .

My knowledge of the history is shaky, but I think this multilinear function interpretation of the comma may have been one idea leading him to the notion of multicategory, which I believe Lambek invented, where arrows have multiple domains and one codomain.

Extrapolating from this, there are formal ways of constructing a (monoidal) multicategory out of any monoidal category $M$ . One way is to consider $M$ as embedded in its so-called strictification, which is a strict monoidal category whose monoidal product may be denoted by commas. You might already know this and anyway I don’t want to get into a lecture about it, but if you want more background on strictification, there’s a good account in Joyal and Street’s paper Braided Tensor Categories (Adv. Math. 102 (1993), 20-78).

That’s about the best I can do to retrace the path of where this idea came from. Some relevant Lambek references might be:

Multicategories Revisited. Contemporary Mathematics 92 (J. W. Gray and A. Scedrov, eds.), Amer. Math. Soc. (1989), 217-240.

What is a Deductive system? Studies in Logic and Computation 4, Oxford U. Press (1994), 141-159.

(Sorry I don’t have online links for you, to these or other relevant references.)

Posted by: Todd Trimble on January 20, 2007 12:15 PM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

$MathML-enabled post (click for more details).$

Todd wrote:

…consider [a monoidal category] M as embedded in its so-called strictification, which is a strict monoidal category whose monoidal product may be denoted by commas. You might already know this and anyway I don’t want to get into a lecture about it, but if you want more background on strictification, there’s a good account in Joyal and Street’s paper Braided Tensor Categories (Adv. Math. 102 (1993), 20-78).

and

Sorry I don’t have online links for you

One place where you can read about strictification online is Theorem 3.1.6 (p.72) of this. (Strictification is called “strict cover” there.)

I should explain one piece of terminology, to save you wading through the preliminaries: an unbiased monoidal category is just like an ordinary monoidal category, except that instead of specifying just a binary tensor product ( $(a, b) \mapsto a \otimes b$ ) and a nullary tensor product (that is, a unit object $I$ ), you specify an $n$ -fold tensor product ( $(a_1, \ldots, a_n) \mapsto (a_1 \otimes \cdots \otimes a_n)$ ) for each natural number $n$ . The idea behind the terminology is that the classical definition is “biased” towards the arities 0 and 2. Once you’ve filled in the details of the definition, it can be shown to be essentially equivalent to the classical definition. So you can choose whichever you prefer: the unbiased definition is often more convenient when you’re doing theory, and the classical definition when you’re doing examples.

Posted by: Tom Leinster on January 21, 2007 3:35 PM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

Thanks a lot, both of you! I had suspected that multicategories were lurking around the edges of my question.

Offhand, the idea of unbiasing looks very reminiscent of the idea of focalisation in structural proof theory. The idea is to fuse all binary connectives whose rule applications in the sequent calculus can be permuted are treated as a single n-ary connective. (This was invented by Andreoli in 1992 to improve proof search for linear-logic based theorem provers, but it is an idea of very general interest – Girard’s new ludics is based in part on this.)

Posted by: Neel Krishnaswami on January 21, 2007 7:55 PM | Permalink | Reply to this

Read the post Melliès on Functorial Boxes
Weblog: The n-Category Café
Excerpt: Functorial boxes
Tracked: August 22, 2008 2:42 PM

Re: Multiplicative Intuitionistic Linear Logic

hi,
I realize that this thread is by now very old, but I thought I’d mention that lots of people, myself included did much work on the multiplicative intuitionistic fragment of linear logic from a categorical theory perspective. While Todd mentioned the work of Szabo, there were several issues there and the intuitions from functional programming as discussed in detail in (Term Assignment for Intuitionistic Linear Logic. (with Benton, Bierman and Hyland). Technical Report 262, University of Cambridge Computer Laboratory. August1992. from
http://www.cs.bham.ac.uk/~vdp/publications/papers.html) helped to improve the categorical intuitions sharply. Gavin Bierman’s paper on the subject was rightfully mentioned (as the hard bit is to put intuitionistic and linear logic together in the same system), but I guess for the fragment that Mike asked for, the reference I’d give is Ian Mackie’s LILAC functional programming language. Ian has done much work on Linear Logic, including interaction nets, that I thought you guys might be interested.
best
Valeria

Posted by: Valeria de Paiva on October 17, 2011 4:13 PM | Permalink | Reply to this

Re: Multiplicative Intuitionistic Linear Logic

$MathML-enabled post (click for more details).$

Thanks for that perspective, Valeria. In a comment where I mentioned Szabo, I believe I did insert appropriate caveats.

I am not familiar with Mackie’s LILAC. I would however like to sound a note of caution regarding the trickiness in giving satisfactory internal languages for MILL; if I recall correctly, Bart Jacobs’ review of the article “An Internal Language for Autonomous Categories”, by Mackie, Román, and Abramsky, points out a problem with their handling of the unit object. I do not know whether LILAC references that language at all. Is there an online article available for LILAC that you would recommend?

Posted by: Todd Trimble on October 17, 2011 6:20 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

January 18, 2007