added pointer to:

- Simon John Ambler,
*First Order Linear Logic in Symmetric Monoidal Closed Categories*, PhD thesis, Edinburgh (1991) [ECS-LFCS-92-194, pdf]

at long last I realized that this article (maybe the first to speak of linear type theory as a theory of quantum programming) has a stable DOI:

- Vaughan Pratt,
*Linear logic for generalized quantum mechanics*, in Proceedings of*Workshop on Physics and Computation (PhysCompâ€™92)*(1992) 166-180 [doi:10.1109/PHYCMP.1992.615518]

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.

]]>