meredith@puck.sw.mcc.com (LG Meredith) (05/17/91)
Are there any widely respected introductions to Linear Logic? I'm simply too stupid to follow Girard's positively Joycean expositions on the subject. I am, however, interested in its applications to semantics for OOLs. --greg L. Greg Meredith AMTS Software Technology Program Microelectronics and Computer Technology Corp. 3500 West Balcones Research Center Dr. Austin, TX 78759 disclaimer: _insert clever verbiage here_
gar@earth.anu.edu.au (Greg Restall) (05/17/91)
In article <3023@puck.sw.mcc.com> meredith@puck.sw.mcc.com (LG Meredith) writes:
* Are there any widely respected introductions to Linear Logic? I'm
* simply too stupid to follow Girard's positively Joycean expositions on
* the subject. I am, however, interested in its applications to semantics
* for OOLs.
Hmm.. I can't give any assistance here, but am mildly interested
in the topic too. Can anyone conversant in Linear Logic perhaps
summarise an introductory exposition for the net? I'm interested
because linerar logic seems to be very close to one of my favourite
logics, C (or RW, for those who like R), basically the relevant
Logic R, without contraction. John Slaney has stated in print that
C is Linear Logic, with distribution of conjunction and disjunction
added to it. I've never had the time or energy to show this, it being
a bit off the track of my research. But I've noted that Girard
fulminates against the confusions of relevant logicians, and I'd
like to know a bit more of what he's on about. I'd also like to
know what the Slaney result is - is it extensional disjunction
and conjunction (which distribute in C), or intensional conjunction
with extensional disjunction (which also distribute in C)? I cannot
see why anyone ought to fulminate against any of these. (But,
I used to think contraction was harmless too, I suppose!)
Any enlightenment is most welcome.
Greg.mueck@hal.fmi.uni-passau.de (Andreas Mueck) (05/17/91)
In article <1991May16.232218.8032@newshost.anu.edu.au> gar@earth.anu.edu.au (Greg Restall) writes: >In article <3023@puck.sw.mcc.com> meredith@puck.sw.mcc.com (LG Meredith) writes: >* Are there any widely respected introductions to Linear Logic? I'm >* simply too stupid to follow Girard's positively Joycean expositions on >* the subject. I am, however, interested in its applications to semantics >* for OOLs. > There is a good paper of Samson Abramsky named "Computational Interpretation of Linear Logic" (Imperial College Research Report DOC 90/20). It gives a good intro to Intuitionistic LL as well as to Classical LL. Andy Mueck, University of Passau, P.O. Box 2540, D-8390 Passau, FRG mueck@unipas.fmi.uni-passau.de ..... god save the Rolling Stones
mantha@mum.wrc.xerox.com (S. Mantha (co-op)) (05/17/91)
In article <1991May17.082838.3274@forwiss.uni-passau.de>, mueck@hal.fmi.uni-passau.de (Andreas Mueck) writes: |>In article <1991May16.232218.8032@newshost.anu.edu.au> gar@earth.anu.edu.au (Greg Restall) writes: |>>In article <3023@puck.sw.mcc.com> meredith@puck.sw.mcc.com (LG Meredith) writes: |>>* Are there any widely respected introductions to Linear Logic? I'm |>>* simply too stupid to follow Girard's positively Joycean expositions on |>>* the subject. I am, however, interested in its applications to semantics |>>* for OOLs. |>> |>There is a good paper of Samson Abramsky named "Computational Interpretation |>of Linear Logic" (Imperial College Research Report DOC 90/20). It gives a good |>intro to Intuitionistic LL as well as to Classical LL. |> |>Andy Mueck, University of Passau, P.O. Box 2540, D-8390 Passau, FRG |>mueck@unipas.fmi.uni-passau.de |> |> ..... god save the Rolling Stones There is another paper by Yves Lafont called "Introduction to Linear Logic". It is from "Lecture notes for the Summer School on Constructive Logics and Category Theory (Isle of Thorns, August 1988). This is a readable paper too. It introduces linear logic from the denotational point of view (coherence spaces .... ) and also talks about sequent calculus and proof nets. After trying to read Girard's original paper, "Finnegan's Wake" reads like "TV Digest". A (probably very stupid) question: The unary connective "!" is supposed to be the modality "ofcourse". In what sense is it "of course"? Girard mentions that "!" and "?" are like the modal operators "box" and "diamond". Is it possible to give a "possible worlds" semantics for formulae with "!" and "?". Girard talks about being able to use something only once or as many times as needed and says that this is related to the philosophical tradition of "strict implication" which originates from Lewis. Could someone explain this? The traditional separation of syntax from semantics (starting from Hilbert) and the identification of "meaning" with "truth" is probably somewhat restrictive, specially if logic is to be used to specify computations. But these new logics (at least at this point in time and certainly to me) seem to lack the simplicity of the traditional logical apparatus. I am only too willing to be proved wrong and to be educated on this. cheers Surya
cbrown@daimi.aau.dk (Carolyn Brown) (05/21/91)
Why all this slagging off of Girard's writing? Sure, I wouldn't start people on that (and the Scedrov and Lafont papers previously mentioned are excellent places to start) but Girard has a lot to offer. Rather like Ulysses (can't speak for Finnegan's Wake, not having read it). I find new ideas in Girard's original TCS paper at each reading (I have been working with linlog for about 4 years). Unravelling his hints gives a lot of insight. I'd rather work hard to read one good paper than have to read 15 simpler papers. (to touch on another thread in this newsgroup). So, for those worried about starting to understand linlog, don't be afraid to read Girard, he is extremely good! Caro
andrews@cs.ubc.ca (Jamie Andrews) (05/22/91)
I think it's important to note, in this discussion, that
linear logic is (or should be) part of a wider field of study.
Linear logic is what Peter Schroeder-Heister calls a
"sub-structural" logic: it's a logic with a proof system which
has restricted structural rules.
The important thing is not necessarily to understand the
details and mystique of the system called linear logic, but
rather to get some feel for the effect of using restricted
structural rules in combination with the various kinds of
connectives.
I have seen several papers in which people studied logical
systems weaker than linear logic and claimed that they were
doing linear logic. But systems weaker than LL are also weaker
than classical logic; five years ago, these people could have
written exactly the same paper and claimed they were doing
classical logic! It might be better to say that they are doing
sub-structural logic inspired by some of Girard's ideas.
The main reason to claim you're doing "linear logic" is to
get a buzzword into your paper. Not a bad reason, but it does
encourage a rather narrow view.
--Jamie.
andrews@cs.ubc.caremo@ecrc.de (Remo Pareschi) (05/22/91)
In article 1991May21.222324.12820@cs.ubc.ca Jamie Andrews (andrews@cs.ubc.ca) writes: > I think it's important to note, in this discussion, that >linear logic is (or should be) part of a wider field of study. >Linear logic is what Peter Schroeder-Heister calls a >"sub-structural" logic: it's a logic with a proof system which >has restricted structural rules. ................. > I have seen several papers in which people studied logical >systems weaker than linear logic and claimed that they were >doing linear logic. But systems weaker than LL are also weaker >than classical logic; five years ago, these people could have >written exactly the same paper and claimed they were doing >classical logic! It might be better to say that they are doing >sub-structural logic inspired by some of Girard's ideas. However, doesn't Linear Logic offer a comprehensive framework which subsumes all other "sub-structural" as well "structural" logics? In fact, Linear Logic drops both Contraction and Weakening, but at the same reintroduces them in a "controlled" fashion by means of the so called exponentials (in his TCS paper, Girard provides translations in Linear Logic of a "structural" logic like Classical Logic and of a "semi-structural" one like Intuitionistic Logic by crucially exploiting the regained expressive power coming from the exponentials); there is a non-commutative version of Linear Logic (described in a JSL paper by Yetter) which drops the remaining structural rule of Exchange, and reintroduces it in a controlled fashion in terms of yet another exponential. Therefore, I would be very interested if Jamie Andrews could provide examples of other logics which are weaker than Linear Logic _because of a restricted use of the structural rules_. Of course, I know of several efforts which make use of _fragments_ of Linear Logic: that is, logics obtained from a subset of the vocabulary of Linear Logic, where any formula is a theorem if and only if is a theorem of Linear Logic. These efforts include the concurrent object oriented/logic programming language LO developed here at ECRC (papers in the proceedings of ICLP'90, OOPSLA/ECOOP'90, and forthcoming in New Generation Computing and in the proceedings of OOPSLA'91), which is based on one such fragment of Linear Logic. But there is a clear distinction between logical systems which are weaker than other systems (i.e. the same formula is a theorem in one system and is not a theorem in the other), and logical systems which are fragments of other systems (i.e. the formulae of one systems are a subset of the formulae of the other system, but for such a subset, the set of theorems for the two systems coincide). Cheers -- Remo
hrubin@pop.stat.purdue.edu (Herman Rubin) (05/22/91)
There have been attempts to come up with a reasonable linear logic since at
least 1919. The problem is that they run into extreme difficulties.
A simple example is the truth value of X&Y, where that of X is .5, as is
that of Y. Now what if Y is X? What if Y is ~X? The extension needed
to take care of things like this is probability.
Linear logics are possible in "Brouwerian" logic, but unless X is false,
~X is false. Negations in Brouwerian logic satisfy Boolean logic.
Certainly one can define any type of system one wants, but giving it a
catchy name like linear logic or fuzzy logic does not mean that is succeeds
in accomplishing its ostensible purpose.
--
Herman Rubin, Dept. of Statistics, Purdue Univ., West Lafayette IN47907-1399
Phone: (317)494-6054
hrubin@l.cc.purdue.edu (Internet, bitnet) {purdue,pur-ee}!l.cc!hrubin(UUCP)gar@earth.anu.edu.au (Greg Restall) (06/06/91)
People were discussing linear logic a while back, and I got to thinking a few things. One question is this - I can understand the weakening of implicational principles involved in LL, but things I don't like missing are the axioms of distributivity. I know that once you drop contraction and weakening from the standard Gentzen formulation of classical logic, distributivity goes with it - but what is so special about that Gentzen formulation? My question is this - is distribution rejected simply because it goes with contraction and weakening in that setup, or do LL'ers have an independent gripe against it? The logic C (which happens to be LL+distributivity, but predates it) seems more natural to me. I wonder why others do not see it that way. Greg. -- --------------------------------------------------------------------------- Greg Restall | Philosophy Department, University of Queensland. gar@lingua.cltr.uq.oz.au | Queensland, 4072. Australia. ---------------------------------------------------------------------------