added pointer to:
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:
A trivia question on notation:
Do people in linear type theory ever use abbreviated notation for terms
in the context of the linear tensor unit?
I am experimenting with introducing an “open-colon” symbol (rhyming on “” for the linear “”) and then sugaring the above to:
]]>added pointer to:
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:
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!
]]>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
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
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 cartesian closed categories; it is noteworthy that this interprets certain intuitionistic sequents . The Curry-Howard translation applied to classical sequents , 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 -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.
]]>