Return-Path: <@Sunburn.Stanford.EDU:PZ7RAIS1%ICINECA.BITNET@forsythe.stanford.edu> Date: Fri, 11 Jun 93 07:55:41 SET From: Claudia Casadio Subject: Roma To: linear@cs.stanford.edu Sender: lincoln@cs.stanford.edu --text follows this line-- Dear colleagues, we send the program of a workshop to be held in Rome at the end of June. Best regards, Michele Abrusci (University of Rome) Claudia Casadio (University of Chieti) 88888888888888888888888888888888888888888888888 WORKSHOP LINEAR LOGIC AND LAMBEK CALCULUS Extensions and Linguistic Applications **************************************************** Dipartimento di Studi Filosofici ed Epistemologici Universita' di Roma - "la sapienza" June 28 - 30, 1993 The aim of this workshop is to address a set of relevant topics concerning the interrelations between Linear Logic and Lambek Calculus in the perspective of a formal theory of language developing the principles of categorial grammar and lexical semantics. The workshop is intended as an inter- disciplinary effort aimed at exchanging scientific results and drawing attention to developments in the area of research involving logic, formal linguistics and computational linguistics. The workshop is held by the department of Studi Filosofici ed Epistemologici, Universita' di Roma, "la sapienza", with the sponsorship of the DYANA Project (Esprit BRA 6852, Dyana-2), under the auspices of the Italian Society of Logics and Philosophy of Science (SILFS). The Department is located at Villa Mirafiori, Via Nomentana 118, 00161 ROMA. For further informations and hotel reservation contact: Claudia Casadio Institute of Philosophy University of Chieti e-mail: PZ7RAIS1@ICINECA FAX: +39-544-217436 ---------------------- PROGRAM ---------------------- MONDAY JUNE 28 Opening addresses: T.De Mauro (Univ.Rome) C.Cellucci (Univ.Rome-SILFS) Introduction: M.Moortgat(OTS Utrecht), M.Abrusci(Univ.Roma) Y.Venema (OTS): Hybrid Substructural Logics H.Leiss & M.Emms(CIS Muenchen): Cut elimination for the second order Lambek Calculus N.Kurtonina (OTS): Possible World Semantics for Categorial logic G.Mascari(IAC,CNR Rome): Linguistics and Proof Nets G.Morrill(Univ.Politecnica Barcelona) Structural Facilitation, Structural Inhibition and Prosodic Islands T.Solias(Univ.Valladolid): Unassociativity, Sequence Product and Gapping TUESDAY JUNE 29 M.Abrusci(Univ.Rome) Exchange connectives for Non-commutative Linear Logic (Lambek Calculus) M.Moortgat(OTS):Types, Sorts and Features M.Emms(CIS, Muenchen): Parsing with Polymorphism A.Lecomte(GRIL Clermont-Ferrand): Syntactic Connection Revisited M.Piazza(Univ.Genova): Some Algebraic Remarks on exchanging connectives G.Morrill(Barcelona): Model Theory and Proof Theory for Discontinuity WEDNESDAY JUNE 30 C.Bohem(Univ.Rome): Title to be announced M.Hepple(UPENN): Labelled Deduction Resource Management and Discontinuous Constituency C.Casadio(Chieti): Syntactic Calculus and Linguistic Theory Panel Discussion: Linear Logic and Lambek Calculus ************************************************************ Return-Path: <@Sunburn.Stanford.EDU:Valeria.Paiva@cl.cam.ac.uk> To: Linear@cs.stanford.edu Subject: Full ILL paper Cc: Valeria.Paiva@cl.cam.ac.uk Date: Fri, 25 Jun 93 17:27:54 +0100 From: Valeria de Paiva Sender: lincoln@cs.stanford.edu --text follows this line-- The following paper is now available by anonymous ftp. FULL INTUITIONISTIC LINEAR LOGIC Martin Hyland and Valeria de Paiva University of Cambridge In this paper we give a brief treatment of a theory of proofs for a system of Full Intuitionistic Linear Logic. Since Girard and Lafont's original paper on Intuitionistic Linear Logic it seems to have been generally assumed that the multiplicative disjunction, {\em par}, does not make sense outside the context of Classical Linear Logic; in particular par was thought to present problems for an interpretation of proofs as functions. However the connective par does have an entirely natural interpretation in models which appeared in the second author's doctoral dissertation, and it is our intention to make good the claim that full intuitionistic is a significant dialect of linear logic. The novelty of Full Intuitionistic Linear Logic lies in its treatment of the interaction between par (which has the same 2-sided sequent-calculus rules as the Classical Linear Logic par) and the linear implication (which only satisfies the intuitionistic properties of an implication). We take as the main initial problem to be overcome the observation of Schellinx that cut elimination fails outright for the intuitive formulation of such a logical system. Our response is to develop a term assignment system which gives an interpretation of proofs as some kind of non-deterministic function (which appears as a sequence of partial functions evaluated in parallel). In this way we find a system which {\em does} enjoy cut elimination. The system is a direct result of an analysis of the categorical semantics, though we make an effort to present the system as if it were purely a proof-theoretic construction. ----------- This paper is available by anonymous ftp from IMPERIAL COLLEGE. If you can not use ftp, send me your postal address. % ftp theory.doc.ic.ac.uk To: Name: anonymous Password: <> ftp> cd theory/papers/dePaiva ftp> binary ftp> get fill.dvi.Z ftp> bye The BibTeX entry for this paper is @unpublished{depaiva93, author = "Valeria de Paiva and Martin Hyland", title = "Full Intuitionistic Linear Logic (Extended Abstract)", institution = "Computer Laboratory, University of Cambridge", month = May, year = 1993, note = ``To appear in Annals of Pure and Applied Logic'' } Valeria de Paiva ------------------------------------------------------------------------------ Valeria de Paiva, | University of Cambridge | Phone: +44 (0)223 334418 Computer Laboratory | Fax: +44 (0)223 334678 New Museums Site, Pembroke Street | JANET: Valeria.Paiva@uk.ac.cam.cl Cambridge CB2 3QG, England, UK | Internet: Valeria.Paiva@cl.cam.ac.uk ------------------------------------------------------------------------------ Return-Path: <@Sunburn.Stanford.EDU:serena@lri.fr> Date: Thu, 8 Jul 1993 18:07:57 +0200 From: Serena Cerrito To: LINEAR@CS.Stanford.EDU Subject: limited use of exponentials Sender: lincoln@cs.stanford.edu --text follows this line-- Does anybody knows something about decidability (indecidability) results for FRAGMENTS of linear logic involving a RESTRICTED use of EXPONENTIALS (where the ``!" modality could be applied just to formulae of a given simple form) ? If yes, I would greatly appreciate any indication of papers which I could look at. Thanks in advance. Serenella Cerrito moderators note: there are a few results along these these lines. Prop LL is undecidable even if there are only negative !, and only wrapping "small" formulas (with two connectives (-o and either * or +) and three propositional atoms). Two sided Tensor Bang LL is decidable for arbitrary uses of !. M. Kanovich claims constant-only prop LL is undecidable, but hasn't published his proof yet. @inproceedings( CL92, Author = "J. Chirimar and J. Lipton", title = "{Provability in TBLL: A Decision Procedure}", Booktitle="Computer Science Logic '91", year = "1992", publisher = "{\it Lecture Notes in Computer Science, Springer}") @article( LMSS92, Author="Lincoln, P. and Mitchell, J. and Scedrov, A. and Shankar, N.", Title="Decision Problems for Propositional Linear Logic", Journal="Annals Pure Appl. Logic", Volume="56", Year="1992", pages="239-311", Note="{Special Volume dedicated to the memory of John Myhill}") Return-Path: Date: Fri, 16 Jul 1993 11:32:05 +0200 From: anne@fwi.uva.nl (Anne S. Troelstra ) X-Organisation: Faculty of Mathematics & Computer Science University of Amsterdam Kruislaan 403 NL-1098 SJ Amsterdam The Netherlands X-Phone: +31 20 525 7463 X-Telex: 10262 hef nl X-Fax: +31 20 525 7490 To: Linear@cs.stanford.edu Subject: papers by ftp Content-Length: 596 Sender: lincoln@cs.stanford.edu --text follows this line-- Not long ago a public domain has been opened for papers by members of the Amsterdam Institute of Language, Logic and Information. In the mean time a new operating system has been installed on our local network and there are corresponding changes for ftp. Instead of ftp vera.fwi.uva.nl one should now use ftp mail.fwi.uva.nl otherwise as before (don't forget binary for dvi and ps files). My papers are as before found in the file pub/illc/astro. So far I have put there only ps files; since not every machine can process our ps files, I shall now also include dvi files. A. S. Troelstra Return-Path: <@Sunburn.Stanford.EDU:guglielm@di.unipi.it> Date: Thu, 22 Jul 1993 23:19:37 +0100 To: Linear@cs.stanford.edu From: guglielm@di.unipi.it (Alessio Guglielmi) X-Sender: guglielm@macmailer.di.unipi.it Subject: commutative and non-commutative tensor Sender: lincoln@cs.stanford.edu --text follows this line-- The following article, together with my follow-up, appeared this evening on sci.logic. Does someone in Linear have a better answer? Alessio Guglielmi >In article <1993Jul22.192010.7169@csi.uottawa.ca> Nax Mendler, >nmendler@csi.uottawa.ca writes: >>I've been daydreaming about a linear logic with two tensors: >> A*B "...afterwards..." >> A|B "...in parallel with..." >>so | is symmetric and * isn't. >> >>Does anyone know of any references to such a beast? >>Especially concerning proof theory. For instance, >>in its sequent calculus, how should the sequents be structured? >>Also, is it sensible to make each tensor its own deMorgan dual? >>What about their right adjoints? What about "!": I can imagine >>different ones like: >> 1) !A |- A * !A >> 2) |A |- A | !A | !A >>What would the proof nets be? etc...etc... >> >>--Nax > >I'm interested in the same question, too. >I haven't read it carefully yet, but the following paper is about >noncommutative linear logic: > >V. Michele Abrusci "Phase semantics and sequent calculus for pure >noncommutative classical linear propositional logic", The Journal of >Symbolic Logic, v. 56, n. 4, Dec. 1991. > >e-mail of the author: abrusci@vaxrma.sci.uniroma1.it . > >Unfortunately, it seems to me that inside Abrusci's calculus there are >only noncommutative connectives, whereas we need noncommutative _plus_ >commutative ones. > >If you come to something interesting, please, let me know. > > Alessio Guglielmi > Dipartimento di Informatica > Corso Italia 40 > 56125 Pisa - Italia > ph.: +39 (50) 510 248 > fax: +39 (50) 510 226 Return-Path: <@Sunburn.Stanford.EDU:lgreg@mcc.com> Date: Fri, 23 Jul 93 14:05:20 CDT From: lgreg@mcc.com (LG Meredith) To: Linear@cs.stanford.edu In-Reply-To: Alessio Guglielmi's message of Thu, 22 Jul 1993 23:19:37 +0100 <9307231657.AA06708@Ghoti.Stanford.EDU> Subject: commutative and non-commutative tensor Sender: lincoln@cs.stanford.edu --text follows this line-- Alessio Guglielmi writes: >The following article, together with my follow-up, appeared this evening on >sci.logic. Does someone in Linear have a better answer? > ... >>I haven't read it carefully yet, but the following paper is about >>noncommutative linear logic: >> >>V. Michele Abrusci "Phase semantics and sequent calculus for pure >>noncommutative classical linear propositional logic", The Journal of >>Symbolic Logic, v. 56, n. 4, Dec. 1991. >> ... >>Unfortunately, it seems to me that inside Abrusci's calculus there are >>only noncommutative connectives, whereas we need noncommutative _plus_ >>commutative ones. Here's what i feel to be the most reasonable of the references i've dug up on non-commutative linear logic: "A representation theorem for quantales", Carolyn Brown, Doug Gurr in Journal of Pure and Applied Algebra 85 (1993) 27-42. This paper proves that every quantale is isomorphic to a relational quantale. This is a nice result since quantales provide a sound and complete class of models for LL, non-commutative or otherwise. "Relations and non-commutative linear logic", Carolyn Brown, Doug Gurr to appear in Journal of Pure and Applied Algebra. This paper presents a sequent calculus from non-commutative linear logic. It proves cut elimination. It gets soundness and completeness essentially by appealing to the representation theorem of the previously mentioned paper. Also, along the lines of >>I've been daydreaming about a linear logic with two tensors: >> A*B "...afterwards..." >> A|B "...in parallel with..." >>so | is symmetric and * isn't. there's V. Pratt's paper on action logic, "Action Logic and Pure Induction" which available via anonymous ftp at boole.stanford.edu in the file jelia.{dvi ps}. He makes some very suggestive comments: "There is no reason to limit action algebras to a single monoid (A,;,1). A logic of concurrency would quite naturally have two such structures, a noncommutative one for sequence and a commutative one for concurrence. Each may then have its own residuations and iteration as required. This would then constitute a 3D logic, <= still being a dimension, namely the static one." Just off the top of my head, it seems to me that the Hilbert style presentation of ACT ought to be useful in thinking about a sequent presentation of the 3D logic Dr. Mendler is "daydreaming" about. Further, if my understanding is correct, one ought to be able to use 3-Cats for sharpening semantic intuitions. Hope this helps, --greg L.G. Meredith MCC 3500 W Balcones Center Dr. Austin, TX 78759 Return-Path: To: Linear@cs.stanford.edu Subject: Re: commutative and non-commutative tensor In-Reply-To: Your message of Fri, 23 Jul 93 14:05:20 CDT. <9307232023.AA06790@Ghoti.Stanford.EDU> Date: Sat, 24 Jul 93 08:21:52 PDT From: pratt@CS.Stanford.EDU Sender: lincoln@cs.stanford.edu --text follows this line-- Date: Fri, 23 Jul 93 14:05:20 CDT From: lgreg@mcc.com (LG Meredith) there's V. Pratt's paper on action logic, "Action Logic and Pure Induction" which available via anonymous ftp at boole.stanford.edu in the file jelia.{dvi ps} [actually {jelia.tex,DVI/jelia.dvi} -vp]. He makes some very suggestive comments: "There is no reason to limit action algebras to a single monoid (A,;,1). A logic of concurrency would quite naturally have two such structures, a noncommutative one for sequence and a commutative one for concurrence. Each may then have its own residuations and iteration as required. This would then constitute a 3D logic, <= still being a dimension, namely the static one." Just off the top of my head, it seems to me that the Hilbert style presentation of ACT ought to be useful in thinking about a sequent presentation of the 3D logic Dr. Mendler is "daydreaming" about. Further, if my understanding is correct, one ought to be able to use 3-Cats for sharpening semantic intuitions. Yes, though it is not strictly necessary for my suggested "3D extension" of action logic, for the following reason. A 3-category has three compositions whose hierarchical organization is as on the left: 2-composition | 1-composition cut rule | / \ 0-composition concurrence sequence with the interchange law holding at all three pairs 01, 12, and 02 (the order matters), but with these compositions otherwise being orthogonal. The "3D" compositional structure I described placed concurrence vs. sequence both below logical implication (whose composition is realized logically as the cut rule), as on the right. In retrospect "3D" underestimates the degree of interaction of concurrence and sequence. Both express temporal accumulation (in the sense of "Temporal Structures", Math.Struct.in CS 1:2, 179-213), with concurrence as the symmetric (permutable) version of sequence. Thus I am more inclined to regard this combination as basically 2D. n-categories model n-dimensional geometry, albeit having monoidal homotopy, i.e. of the kind where not every corner can be backed out of, as in deadlock and its dual wedlock. I don't see three distinct dimensions with cut, concurrence, and sequence because of the above strong interaction between the last two preventing them from being orthogonal dimensions. -- Vaughan Pratt Return-Path: <@Sunburn.Stanford.EDU:retore@logique.jussieu.fr> Date: Mon, 26 Jul 93 14:40:48 +0200 From: retore@logique.jussieu.fr (Christian Retore) To: Linear@cs.stanford.edu Sender: lincoln@cs.stanford.edu --text follows this line-- Reseaux et Sequents ordonnes / Pomset Logic Concerning the previous messages I wanted to report that i passed a thesis this winter under the direction of girard which is devoted to a logical calculus involving the usual par and times -associative and commutative - and a third multiplicative connective which is associative NON-commutative and self dual; this connective is linearly implied by times and lineraly implies par. This calculus deals with partially ordered (multiset)sets of formulae, which are in fact generalised or n-ary connectives. As this order also concerns the cuts this syntax naturally encodes a concurrent strategy for computing proofs. The par corresponds to two formulae equivalent in the order, while the precede corresponds to two formulae the first one being the only predecessor of the second, and the second the only successor of the first one. Binary rules times and mix are a bit more complicated to describe, but the idea is that the order on the conclusion sequent is as large as possible provided that it is correct wrt semantics and proofnet syntax. THis can be characterised using a notion of orthogonality bewtween non-symmetrical relations. THe mix rule (see eg forthcoming paper in mscs) is highly necessary to this calculus otherwise the order would remain empty. Concerning this calculus, we proved the followings: it has a sequent calculus presentation - there was none for previous generalised connectives it also has a proofnet syntax whose criterion is quite simple -this was not really the case for non-commutative calculi- its presevation under cut elimination of the calculus which strongly normalises and conflues it enjoys a denotationnal semantics based on ordered products of coherence spaces which can be computed both on the sequent or proofnet syntax for which A precedes B and B precedes A are non- isomorphic - this seems to improve both the non-commutative and generalised connectives the sequent calculus is schown to be the largest to be sound wrt proofnet syntax or coherence semantics - sequentialistion is still in progress the generalised connectives which are definable using the binary ones correspond to partial orders without N, ie they exactly are series parallel orders, precede being the serie composition, and par the parallel one! - i did not know of these sries paralllel orders when i wrote the thesis... the extension to modalities and quantifiers - with boxes - is straight forward. Up to now the only thing i wrote down on this topic is my thesis and i must apologise that except the introducion in english it is in french, and that it is not available by ftp, because of handmade drawings. Nevertheless i can send a copy to anyone interested in, and the corresponding paper should be ready by next autumn. Chritian Retor\'e Equipe de Logique Universit\'e Paris 7 Return-Path: <@Sunburn.Stanford.EDU,@Aphid.Stanford.EDU:sa@doc.ic.ac.uk> Date: Mon, 26 Jul 1993 11:34:58 +0100 (BST) From: Samson Abramsky Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII To: linear@cs.stanford.edu Subject: The full abstraction problem for PCF Sender: lincoln@cs.stanford.edu --text follows this line-- Games and Full Abstraction for PCF: Preliminary Announcement Samson Abramsky, Radha Jagadeesan and Pasquale Malacaria We define a model for PCF to be *intensionally fully abstract* if it is algebraic, and all its compact elements are definable. Any intensionally fully abstract model yields the (order-extensional, inequationally) fully abstract model as its ``extensional collapse''. An intensionally fully abstract model contains no ``junk''. No previously known model of PCF defined independently of the syntax of PCF has had this property. We have found an intensionally full abstract model for PCF based on a refinement of the category of games and history-free strategies previously introduced by Abramsky and Jagadeesan. A preliminary note containing some further details is available by anonymous ftp, using the protocol: % ftp theory.doc.ic.ac.uk Name: anonymous Password: <> ftp> cd papers/Abramsky ftp> binary ftp> get gfapcf.dvi ftp> quit Return-Path: <@Sunburn.Stanford.EDU:Luke.Ong@cl.cam.ac.uk> Subject: Games and Full Abstraction for PCF: Joint Announcement Date: Tue, 27 Jul 93 16:45:24 +0100 From: Luke Ong To: linear@cs.stanford.edu Sender: lincoln@cs.stanford.edu --text follows this line-- Games and Full Abstraction for PCF: Joint Announcement Say that a model for PCF is *intensionally fully abstract* if it is algebraic, and all its compact elements are definable. No previously known models of PCF defined independently of the syntax of PCF have had this property. Intensionally fully abstract models of PCF have now been found, independently, by two groups: Abramsky, Jagadeesan and Malacaria; and Hyland and Ong. Although the presentations are quite different, its seems that the models are very close. Documents giving some further details of the two approaches can be obtained by anonymous ftp from theory.doc.ic.ac.uk in papers/Abramsky/gfapcf.dvi papers/Ong/dgis.ps