A trivia **question** on notation:

Do people in linear type theory ever use abbreviated notation for terms

$\mathbb{1} \;\; \vdash \;\; \psi \; \colon \; \mathcal{H}$in the context of the linear tensor unit?

I am experimenting with introducing an â€śopen-colonâ€ť symbol (rhyming on â€ś$\multimap$â€ť for the linear â€ś$\to$â€ť) and then sugaring the above to:

$\vdash \;\; \psi \; \opencolon \; \mathcal{H}$ ]]>added pointer to:

- Daniel MihĂˇlyi, Valerie NovitzkĂˇ,
*What about Linear Logic in Computer Science?*, Acta Polytechnica Hungarica**10**4 (2013) 147-160 [pdf]

I also use Google (or, if that doesnâ€™t produce good hits, more specialized services, such as GoogleScholar or InSpire). With the title in hand it is often (though admittedly not always) quick to find a webpage from which the publication data (in particular the DOI-link) may easily be copy-and-pasted.

While this task of recording publication data may seem a little tedious at times, itâ€™s not specific to the nLab but the same task as for any research article one writes, hence as such integrally part of the routine of research.

In fact, I have long adopted the habit of recording on the nLab strictly all references that I need for my research, and then grabbing them from there. This is at most the same work that other people invest into their private bibtex file, but seems much more useful.

]]>Do you have an easy way of finding all the data about a paper? I try to put the DOI-link and everything but I donâ€™t have a better way than typing the name of the paper (or the book) in Google to find it and it takes a little of time.

]]>while we are at it, letâ€™s add publication data and DOI-link:

- Richard Blute, Philip Scott,
*Category theory for linear logicians*, in:*Linear Logic in Computer Science*, Cambridge University Press (2004) 3-64 [doi:10.1017/CBO9780511550850.002, pdf]

Added pointer to the page of Phil Scott

]]>Hi Valeria,

thanks for your input. Since I had been editing these entries heavily a while back, I should say and need to admit that I will not be doing so for the time being, as I am quite busy otherwise. This does not mean that I am not interested, it just means that I am finite. If you do think there is some attribution which ought to be added and or fixed on the nLab, then I would like to ask you and Todd â€“ and other experts here with some energy for this â€“ to please go ahead and do so.

So what I want to say is that I wonâ€™t be editing in these matters at the moment, but if there is something that needs to be sorted out in some nLab page then I do hope that it will be sorted out.

]]>Valeria, thanks for clarifying. I think we had started off in this thread talking about the multiplicative fragment which is of course much simpler than full linear logic that you are discussing in your last comment. These discussions deserve to be carried out with care.

Thanks also very much for your last comment mentioning Houstonâ€™s work (with Heijltjes) on the units. I wouldnâ€™t have said, â€śwhy the coherence theorems donâ€™t work with the unitsâ€ť, but their results on the complexity of decision procedures for coherence in MLL seems to answer a question I had had for ages, so itâ€™s really nice to hear this now!

]]>"No proof nets for MLL with units" http://www.cs.bath.ac.uk/~wbh22/docs/MLL.pdf ]]>

I wanted to explain that the reason I said my models were the first mathematical model of Linear Logic is because coherent spaces (the denotational structures where Girard explained he got the idea for Linear Logic from) are collapsed models of Linear Logic. They don't make the distinctions that Linear Logic wants to make between additives and multiplicatives. in particular as explicitly said in the Linear Logic wiki

"Remark: It is one of the main defect of coherent semantics w.r.t. linear logic that it identifies the neutrals: in coherent semantics \zero = \top and \one = \bot". (that is true=false, and some of us do not like true=false. this is in http://llwiki.ens-lyon.fr/mediawiki/index.php/Coherent_semantics. Now at that stage there was a big push to find a semantics that did not collapse any of the connectives of linear logic and Rick Blute ended up putting a topology in vector spaces to do so, to stop connectives collapsing, as he says in his hopf algebra paper.

My second Dialectica semantics(categories GC published in 89, based on a suggestion of Girard) did not have this problem, hence I claim that it was the first mathematical model who kept all connectives apart, but my first Dialectica categories were the first that could model all the intuitionistic connectives plus the bang, which is really the difficult thing to model in Linear Logic. (one of the reasons people worried about keeping connectives apart or not then was the fact that people thought products were much nicer than tensor products, as these are not universal, a view completely outdated now...). Now the other person that is missing from this is Samson Abramsky and his student Ian Mackie who definitely wrote a thesis concentrating on the fragment of

intuitionistic multiplicative linear logic with bang and describing the linear type theory associated. the problem was that Samson had the wrong rule for bang, as did Robert Seely, and the same way that Szabo thought the he had enough syntax to get confluence, Seely and Abramsky did not notice that they lost the most essential property of lambda-calculus (or type theory) which is substitution of lambda terms for the bang connective. this is the big point of TR262, it explains why the ability to substitute terms for terms was lost and how to regain it. But Barber's version later on might be a better way to regain it, depending on what you want to do with your linear type theory. ]]>

I have to go offline now, but eventually we should link to some of this information also from *coherence theorem*. In particular also your thesis should be linked to there, with a remark on what it is that it establishes. It is a shame that after all these years of editing the nLab, I see this point only now. This should to be rectified by putting more information on the nLab.

But I have to quit now. More later.

]]>This is very interesting. I wasnâ€™t aware before that categorical logic was so deeply rooted in actual problem solving. This is an excellent selling point.

]]>Urs, glad to hear it! Yes, I found this book very useful when I was first learning this. I believe this was for me a primary source for learning the nitty-gritty details of cut-elimination (that and the original papers of Lambek). May the shades of Kelly and Mac Lane forgive me for saying so, but these sources were far more illuminating for me than was their paper.

It is a shame that Szaboâ€™s work is sometimes sneered at in some categorical circles, just because his normalization schemes were flawed. The cut-elimination schemes are impeccable, however, and I believe it was Robin Houston at the n-Category Café who pointed out to me that these schemes give, in principle, full coherence theorems (in the sense that the Lambek equivalence relation is a primitive recursive set â€“ at least for those logics with which I am most familiar). Not very elegant, efficient, or humanly usable coherence theorems, it is true, but they are there.

]]>Todd,

I have now finally looked at

- M.E. Szabo,
*Algebra of Proofs*, 1978

This is excellent! The table on page 2 in the introduction (listing all sorts of logics for all sorts of monoidal categories) is just what I was hoping to see.

Thanks again for pointing this out!

I added a copy of this citation also to *linear logic*. I suppose we should add it also to *proof theory*, *internal logic* and related entries.

Maybe later, I need to go offline this second now.

]]>Thanks once more, Todd.

Yes, I guess I know why one says â€śMILLâ€ť, I was really wonderig who to credit for this.

You see, for what I am after this was more meant to be a throw-away remark like this: I would like to talk about symmetric monoidal categories and then say â€śtheir internal language is usually called â€™linear type theoryâ€™. possibly with some more qualifiersâ€ť and this is due to â€¦ â€ś.

For my intended readership ideally the ellipses here would be a single citation which states this clearly and is at the same time â€śoriginalâ€ť. But I understand now that the history of what looks like a simple idea is complicated and hard to cite. Maybe itâ€™s one of these situations where all the experts were too absorbed with going for the high-hanging fruit (coherence) that nobody took the time to write the simple clear exposition for the non-experts.

Much later roughly such an exposition appeared as Baez-Stay 09, as you know. But it seems to me in there the originators of this â€śRosetta stoneâ€ť, the way you now point it out, are not really being cited there.

But in any case, I do get the point of your comments now, I think. I am wondering now if a summary such as yours here might have been useful earlier not just to outsiders of the field like me. I will add a semi-long citation the way you just proposed to my note now. Thanks again for all the information.

]]>Thanks, Urs. I put in the Kelly-Mac Lane reference (the year was 1971, not 1972).

I wonder a bit about â€śfirst non-syntactic categorical modelâ€ť. Can that really be true? For one, I thought Girardâ€™s category of coherence spaces (mentioned in his original linear logic paper, 1987) were supposed to be a model of (and even a motivating guide which led to) full linear logic, including the modalities and everything. I have to admit that I am not too familiar with Valeriaâ€™s work, so Iâ€™m not sure what the actual claim should be.

The question

- where does the term â€śmultiplicative intuitionistic linear logicâ€ť actually originate?

is a good one, and can be interpreted either as asking for who invented the term (and what source to cite), or as asking why that term is used. Curiously (and a little embarrassingly), I donâ€™t actually know the precise answer to the first of those, but I bet I could find out. If you want, I could try writing up an answer to the second (but Iâ€™m not sure thatâ€™s what youâ€™re after here). [Edit: actually, I sort of address that below.]

As for

The study of the internal language of (closed symmetric, not necessarily Cartesian) monoidal categories goes back at least to (Lambek 68,69), then motivated as a means to syntactically prove the coherence theorems for these categories. This was further pursued by several authors, notably (Kelly-MacLane 72, Minc 77, Jay 89, Jay 90, Blute 91, Trimble 94). When (Girard 87) introduced â€ślinear logicâ€ť it was readily seen to correspond to the special case of star-autonomous categories (Seely 89) and subsequently the original general case came to be known as â€śmultiplicative intuitionistic linear logicâ€ť: In this spirit linear logic and linear type theory as the language of symmetric monoidal categories was further studied in (de Paiva 89, de Paiva-Hyland 93, Bierman 95, Barber 97).

I think Iâ€™d want to modify and expand that just a bit. Perhaps to something like this:

The study of internal languages for (symmetric, not necessarily cartesian, and typically closed) monoidal categories has an interesting history. Logical languages for closed monoidal categories go back at least to work of Lambek (68, 69), who had the fruitful idea not only that Gentzen sequent derivations could be interpreted in suitably structured categories, but that the method of Gentzen cut-elimination could be applied to study coherence problems for such structures. The first test case of this thesis was for monoidal biclosed categories, but no doubt Lambek realized precisely which fragment of Gentzen sequent calculus is naturally interpreted in closed symmetric monoidal categories. A systematic study of which internal logical languages correspond to which doctrines of monoidal categories may be found in the book (Szabo 78) by Szabo, a student of Lambek, including the important case of closed symmetric monoidal categories.

A specifically type-theoretic internal language was given in (Minc 77); see also (Howard 80) for the passage between derivations in sequent calculus and terms in type theory. The applications of the â€śCurry-Howard isomorphismâ€ť were originally to lambda calculus which is naturally interpreted in

cartesianclosed categories; it is noteworthy that this interprets certainintuitionisticsequents $A_1, \ldots, A_n \to B$. The Curry-Howard translation applied to classical sequents $A_1, \ldots, A_n \to B_1, \ldots, B_m$, with an involutive negation, yields a type theory which is â€śalgorithmically inconsistentâ€ť, i.e., uninteresting in the sense that all terms of any given type are provably equal. An essential insight of Girard is that by dropping the cartesianness (the contraction and weakening rules of inference), one could give a sequent calculus with involutive negation and de Morgan duality, whose Curry-Howard translation nevertheless yields a rich and viable type theory; on the categorical side, this type theory corresponds to $\ast$-autonomous categories. Moreover, the intuitionistic analogue of this linear sequent calculus or linear type theory gives back the original logical frameworks well studied in the tradition of Lambek. (Can add in stuff coming out of Cambridge, e.g., de Paiva, Hyland, Bierman, etc.)

Too long? I decided to trim out most of the stuff on history of coherence theory as distracting or not really belonging to the story you want to tell. (I brought that stuff up in earlier comments to help jog my memory on how these considerations actually go way back, but I think this story Iâ€™m telling now is a bit more to the point.)

]]>Todd, thanks.

Some quick comments on the entry:

the citation KM72 is not defined. (I notice that also the other nLab entries on coherence donâ€™t seem to have it)

dePaiva 92 is now advertized as providing the â€śfirst non-syntactic categorical modelâ€ť for Girardâ€™s linear logic, while I thought the point of it was that it provided a model of just a fragment;

where does the term â€śmultiplicative intuitionistic linear logicâ€ť actually originate?

So then I can come back to what motivated my question: I would like to find a way to sensibly cite the perspective that linear logic in its multiplicative fragment is the internal language of symmetric monoidal categories. I need to condense the information you kindly provided to just a very small number of sentences.

How about this:

The study of the internal language of (closed symmetric, not necessarily Cartesian) monoidal categories goes back at least to (Lambek 68,69), then motivated as a means to syntactically prove the coherence theorems for these categories. This was further pursued by several authors, notably (Kelly-MacLane 72, Minc 77, Jay 89, Jay 90, Blute 91, Trimble 94). When (Girard 87) introduced â€ślinear logicâ€ť it was readily seen to correspond to the special case of star-autonomous categories (Seely 89) and subsequently the original general case came to be known as â€śmultiplicative intuitionistic linear logicâ€ť: In this spirit linear logic and linear type theory as the language of symmetric monoidal categories was further studied in (de Paiva 89, de Paiva-Hyland 93, Bierman 95, Barber 97).

?

]]>Sure, fine Tim. Although Iâ€™m not sure what is the antecedent for your â€śthisâ€ť.

Hopefully we can keep the discussion focused on so-called â€ślinear type theoryâ€ť, in the sense of the article. Hopefully there is also some understanding too, from non-regular participants, of the fact that nLab articles are sometimes created like sausage. I was asked for details, and responded with some informal remarks, which have now managed to find their way into the article. I wouldnâ€™t want this necessarily incomplete and possibly biased â€śthumbnail sketchâ€ť Urs and I just hashed out to be felt as an affront to anyone (e.g., Phil Scott, who was never mentioned, but whose work has been historically important).

]]>Why not ask Rick Blute himself? In fact I just e-mailed him with the idea of seeing what his view on this was. Hopefully he will join in.

Phil Scott may also be helpful on the history.

]]>Okay, I had a go at reorganizing the history section so that things flowed better (I was glad you inserted my comments above, but they were not yet ripe for the Lab, as they were written in a kind of stream-of-consciousness style). I also added some annotations to the reference section, and did some slight reorganizing there too.

Iâ€™m a little tired now, but Iâ€™ll go back to it later to check to see how happy I am. Meanwhile others should look this over with a critical eye. I am not intimately familiar with all that has gone into this article (and there is an awful lot more that could be said).

I also wondered whether some parts could usefully be split off into separate articles.

]]>Sure, sorry. I did edit a bit for the entry.

(Thatâ€™s quite a treasure of information that you provided there.)

]]>Urs, maybe we could slow down just a minute. I will be glad to incorporate my remarks into the article, but I think the citing of sources and the general history needs to be handled with some care.

]]>(Continued)

The founding papers of Lambek were extremely important in my opinion, and I think could well be cited, although they concentrate mainly on the monoidal biclosed case (which Lambek was interested in for other reasons, having to do with his categorical researches in linguistics).

Blute, a student of Scedrov at U. Penn., wrote his thesis specifically on Girardâ€™s technique of proof nets as applied to coherence problems. Proof nets, introduced in one form in the original linear logic paper of Girard (cf. the material on â€ścyclic tripsâ€ť) and developed further by Danos and Regnier, are a very pretty graphical way of visualizing the essential structure of Lambek-equivalence classes of sequent proofs and their cut-elimination specifically for fragments of MLL, including MILL, and some more abstruse cases which you might not know (involving the so-called MIX rule). They are closely related to Kelly-Mac Lane extranaturality (or dinaturality) graphs, and what Blute does is how how to rederive the coherence-theoretic results of Kelly-Mac Lane for smc categories using the technique of proof nets. Actually, he treats a number of doctrines of monoidal closed type in the same way, indicating which doctrines are amenable to cut-elimination and which are not (e.g., compact closed categories), and I think he relates this also to which of these doctrines are â€śclubbableâ€ť in the sense of Kelly.

And now a few words of where my thesis and related work fits in. The coherence problem for smc cats was generally regarded as notorious and fearsomely difficult, partly because the techniques of Kelly and Mac Lane (based themselves on a close reading and rewriting of Lambekâ€™s work), based as they were on extranaturality graphs which track naturality and dinaturality instances of the variables that appear in morphisms of free structures (in the specifically â€ślinearâ€ť cases, even if they didnâ€™t call it that), were insufficient to deal with constants such as the monoidal unit $I$. Szabo, Minc, Jay, Kelly, and at least two students of Mac Lane (Voreadou and Dole) all gave their own solutions, and all were (at least IMHO) difficult with Szaboâ€™s being outright wrong. What I did in my thesis is reinterpret the proof nets so that they would manifestly apply to the units as well. In the *intuitionistic* case (MILL), it was possible to give a very satisfying rewrite system on these unit-extended (cut-free) proof nets that was strongly normalizing and confluent, so that the normalization solves the full coherence problem in a relatively simple and elegant way. It is probably fair to say that the coherence problem looks far less fearsome as a result of this work. The re-interpreted (i.e., unit-extended) proof nets also apply to MLL, so that the coherence problem for $\ast$-autonomous categories is effectively solved in terms of â€śrewiringâ€ť-equivalence classes of proof nets, although that case is, from the standpoint of writing down a rewrite system, not clean and simple as MILL: there is an input-output directionality for MILL proof nets that is not there for MLL proof nets. The work on such unit-extended MLL proof nets is covered in

- Blute, Cockett, Seely, Trimble,
*Natural deduction and coherence for weakly distributive categories*, JPAA 113 (1996), 229-296. (web)

(Weakly distributive categories are very closely related to $\ast$-autonomous categories: they have monoidal products $\otimes$, $\wp$ for the multiplicative conjunction and disjunction, with an appropriate distributivity or strength relating the two, but without linear negation. The paper gives precise details on the relationship.)

]]>I donâ€™t think I read Bluteâ€™s thesis in detail, but he and I were talking a bit back in those days and so I have an idea of whatâ€™s in his thesis. The main reason I brought up his thesis is that itâ€™s one concrete place where I know various fragments of MLL and their categorical semantics are discussed, not because that semantics is the main focus of the work, but because the proof theory of the fragments is being related to coherence-theoretic results over on the categorical doctrine side. My memory of original sources for categorical semantics of fragments of linear-type logic is pretty bad, but I can tell you that *I* myself was aware of how this basically works back in that day. It was pretty well-known by anyone working in the area, even if the word â€ślinearâ€ť was not always used.

For example, in Manfred Szaboâ€™s Algebra of Proofs, written in the 1970â€™s even, you will find descriptions of many fragments of classical propositional logic and their sequent calculi, including quite specifically the fragments that correspond to sm and smc categories, discussed in quite some detail.

- M.E. Szabo,
*Algebra of Proofs*, Studies in Logic and the Foundations of Mathematics, vol. 88 (1978), North-Holland.

Szabo was a student of Lambek, who was perhaps the founding father of the entire area: it was Lambek who first related the proof theory of various fragments of logic to category theory and promoted (categorified, in a sense) the crucial cut-elimination method of Gentzen to obtain coherence-theoretic results on the categorical side. This started already back in the 1960â€™s, basically with monoidal biclosed categories (or what were called residuated categories) but dropping the monoidal unit, of which more in a moment.

J. Lambek,

*Deductive systems and categories*, Mathematical Systems Theory 2 (1968), 287-318.J. Lambek,

*Deductive systems and categories II*, Lecture Notes in Math. 86, Springer-Verlag (1969), 76-122.

Cut-elimination is usually presented in the context of sequent calculus, but workers in the area were also aware of how to translate into other logical frameworks (e.g., types and terms). For example, I believe this is discussed in

- G.E. Minc,
*Closed categories and the theory of proofs*, translated from an article in Russian in Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Mat. Instituta im. V.A. Steklova AN SSSR 68 (1977), 83-114.

[Thatâ€™s the reference as written in the bibliography for my thesis; hopefully the transliteration doesnâ€™t look like gibberish to Russian speakers.] Also I recall some papers of Barry Jay,

C.B. Jay,

*Languages for monoidal categories*, JPAA 59 (1989), 61-85.C.B. Jay,

*Coherence in category theory and the Church-Rosser property*. Unpublished preprint (1990), cited in the following reference.C.B. Jay,

*The structure of free closed categories*, JPAA 66 (1990), 271-285.

that develop a term calculus to give coherence-theoretic results for mc and smc categories in particular. So I think these references back up my claim that ideas on categorical semantics of fragments of logic, including famously the case of smc categories, were well â€śin the airâ€ť by the late 80â€™s, and not just in the air but written down, even if not all of them gave a nod to Girard (a contentious and controversial figure as it is!).

To give some further information: Szaboâ€™s work has unfortunately been derided in some circles, because he wrongly claimed to have a rewrite system of sequent proofs for a batch of cases including sm and smc categories that was strongly normalizing and Church-Rosser; the claim of being Church-Rosser was refuted by Jay in the second of the three references I gave. Personally, however, I found Szaboâ€™s book quite valuable because it had very concrete details on the sequent calculi themselves and their categorical semantics. It should probably be cited, if one is looking for original sources.

To be frank, I found Jayâ€™s articles that give his own solution to the coherence problem for smc cats too sketchy or otherwise difficult to read. (cont.)

]]>