Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Am trying to get some historical citations straight at linear type theory, maybe somebody can help me:
what are the original sources of the idea that linear logic/type theory should generally be that of symmetric monoidal categories (“multiplicative intuitionistic LL”)?
In order of appearance, I am aware of
de Paiva 89 gives one particular example of a non-star-autonomous SMC that deserves to be said to interpret “linear logic” and clearly identifies the general perspective.
Bierman 95 discusses semantics in general SMCs more generally
Barber 97 reviews this and explores a bit more.
What (other) articles would be central to cite for this idea/perspective?
I am aware of more recent reviews such as
but I am looking for the correct “original sources”.
By a weird coincidence, right after I have posted the above, I see that Valeria de Paiva has posted a related comment on g+ (here).
From this I deduce two more original articles on the idea “linear logic is generally the logic of SMCs”:
Nick Benton, Gavin Bierman, Valeria de Paiva, Martin Hyland, Term assignments for intuitionistic linear logic. Technical report 262, Cambridge 1992
Martin Hyland, Valeria de Paiva, Full Intuitionistic Linear Logic (extended abstract). Annals of Pure and Applied Logic, 64(3), pp.273-291, 1993. (pdf)
See the new list of citations right at the beginning of both linear logic and linear type theory.
“linear logic is generally the logic of SMCs”
That would be (multiplicative) intuitionistic linear logic. The involutory nature of linear negation (very much emphasized by Girard) is of course dropped in MILL.
Todd,
here on the nForum I am trying to give brief hints for what i am talking about without repeating it all over again. In the nLab entry I put:
In the original definition of (Girard 87) linear logic is the internal logic of/has categorical semantics in star-autonomous categories (Seely 89, prop. 1.5). But more generally linear logic came to refer to the internal logic of any possibly-non-cartesian symmetric closed monoidal category (then usually called multiplicative intuitionistic linear logic – MILL) or even polycategory (de Paiva 89, Benton-Bierman-de Paiva-Hyland 92, Hyland-de Paiva 93, Bierman 95, Barber 97, see also Schalk 04, Melliès 09).
That said, it seems to me lots of the time one becomes more relaxed and just says “linear logic” for the general case. In fact that’s what people around here (including you, I seem to remember) made me do after I first did not.
By the way, as Valeria suggests if I’m reading her correctly, I think there are older sources for MILL being the logic of SMC’s. Rick Blute’s thesis came out in ’91 and certainly went into the various flavors of linear logic and their categorical models, including SMC’s. I’m not sure of the earliest sources for this idea (which were probably well in the air by late 80’s).
Urs, I think we had taken it even further: that what makes this “logic” linear is the dropping of the contraction and weakening rules (say for conjunction). So I think “linear” could apply just as well to weaker fragments which would include the logic of just symmetric monoidal categories. Certainly MILL is an extremely important case, but I would call for even greater inclusiveness for the meaning of “linear” and what it connotes.
Valeria,
thanks for the input! I have added the ps-reference, to your article, too, now, but I also added the pointer to citeseer
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.8666
which also lists a pdf (I am one of those people who greatly prefer being served a pdf over a ps).
So if I see correctly, then this TR262 is really the genuine first reference to consider as linear logic the internal language of general SMCs, is that right? (I want to cite this insight/perspective in some article, and I am trying to figure out what the correct attributions should be.)
So if I see correctly, then this TR262 is really the genuine first reference to consider as linear logic the internal language of general SMCs, is that right?
As I was just saying, I don’t think that’s quite right. The fragment of linear logic that is naturally modeled in SMC’s was certainly in the literature before 1992, e.g., Blute’s thesis. (This is not to deny the importance of TR262.)
Todd,
okay, I see. There is a tad of mentioning of the general meaning of “linear” in the entry, maybe you’d have a minute to expand further?
Is Blute’s thesis available online?
And by the way, is your thesis available online?
Sure, I’d be happy to expand a bit. Basically I think we’re on the same page, despite possible appearances to the contrary.
I don’t know about Blute’s thesis (I doubt it, but he lists a 1991 journal article in TCS which I think was largely based on his thesis, and which might have pointers to even earlier sources). Maybe I can write him to ask.
Mine is not available online. I can mail you a hard copy if you really want (although I am not proud of the writing style, which is a mess – only in the actual main results).
Urs, that indeed bears the same name as his 1991 thesis, and is probably virtually the same product modulo some possibly revisions after the fact. Good detective work!
Thanks! Whatever details you might have a chance to find, I’d be interested in. Also if there is anything documenting how the idea was “in the air” in the 80s (which I can easily imagine), let me know.
I’d be interested in knowing more about your thesis. Maybe there is a place somewhere on the Lab for you to record its results?
I saw pointers to it, but I haven’t maybe properly followed them yet: could anyone briefly tell me about “geometry of interactions” and what a canonical text to look at would be? Thanks.
I’ve done a little editing over at linear type theory to reflect some comments above. Urs, I would like to continue this discussion, but I may need some time (e.g., to track down sources). I can probably whip up a brief description of some of my thesis on my web page, and think about how to incorporate some of that into the Lab proper.
It’s been ages since I’ve read Girard’s Geometry of Interactions [he has a paper with that title, which might be a canonical albeit quirky source]; I’d have to reread before discussing it. Probably Valeria would be better placed to discuss it here and now.
There are six papers in the series ’Geometry of Interaction’, III-VI are here. V lists the first four
[4] J.-Y. Girard. Towards a geometry of interaction. In Categories in Computer Science and Logic, pages 69 – 108, Providence, 1989. American Mathematical Society. Proceedings of Symposia in Pure Mathematics n92.
[5] J.-Y. Girard. Geometry of interaction I: interpretation of system F. In Ferro, Bonotto, Valentini, and Zanardo, editors, Logic Colloquium ’88, pages 221 – 260, Amsterdam, 1989. North-Holland.
[6] J.-Y. Girard. Geometry of interaction II : deadlock-free algorithms. In Martin-Löf and Mints, editors, Proceedings of COLOG 88, volume 417 of Lecture Notes in Computer Science, pages 76 – 93, Heidelberg, 1990. Springer-Verlag.
[7] J.-Y. Girard. Geometry of interaction III : accommodating the additives. In Girard, Lafont, and Regnier, editors, Advances in Linear Logic, pages 329 – 389, Cambridge, 1995. Cambridge University Press.
[8] J.-Y. Girard. Geometry of interaction IV : the feedback equation. In Stoltenberg-Hansen and Väänänen, editors, Logic Colloquium ’03, pages 76 – 117. Association for Symbolic Logic, 2006.
So I started a page Geometry of Interaction for these references. I think capitalization is normal.
Todd, re #16,
thanks! I have added the pointer to Blute’s thesis at linear type theory (already did so yesterday also at linear logic).
(But I still couldn’t get hold of the thesis itself, so I am not sure what exactly Blute actually did there regarding semantics of linear logic in monoidal categories.)
Regarding your thesis: might you say briefly in a few informal words here what the central results were about?
David, re #17, #18, #19,
thanks! Let’s discuss GoI further in its own thread.
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.
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
[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.)
(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 . 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 -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
(Weakly distributive categories are very closely related to -autonomous categories: they have monoidal products , 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.)
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.
Sure, sorry. I did edit a bit for the entry.
(That’s quite a treasure of information that you provided there.)
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.
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.
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).
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).
?
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.)
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.
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.
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.
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.
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.
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!
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.
while we are at it, let’s add publication data and DOI-link:
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.
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.
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:
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:
added pointer to:
added pointer to
1 to 48 of 48