Return-Path: <@Xenon.Stanford.EDU:saraswat@parc.xerox.com> From: Vijay Saraswat To: linear@cs.stanford.edu Subject: LFG semantics via Constraints Date: Tue, 27 Apr 1993 10:09:52 PDT Sender: lincoln@cs.stanford.edu --text follows this line-- To make up for my previous contretemps, I offer the following meaningful post. The paper deals with the use of (tensor, -o)-fragment of first-order LL instead of the typed lambda-calculus to assemble meanings of natural language utterances from the meanings of constituent phrases. The paper appears in the proceedings of EACL '93 (European Association for Computational Linguistics, I think). It is available via anonymous ftp on parcftp.xerox.com as pub/ccp/nl/eacl93-lfg-sem.{dvi,ps}. Vijay -------------- LFG Semantics via Constraints Mary Dalrymple John Lamping Vijay Saraswat {dalrymple, lamping, saraswat}@parc.xerox.com Xerox PARC 3333 Coyote Hill Road Palo Alto CA 94304 USA ABSTRACT Semantic theories of natural language associate meanings with utterances by providing meanings for lexical items and rules for determining the meaning of larger units given the meanings of their parts. Traditionally, meanings are combined via function composition, which works well when constituent structure trees are used to guide semantic composition. More recently, the *functional structure* of LFG has been used to provide the syntactic information necessary for constraining derivations of meaning in a cross-linguistically uniform format. It has been difficult, however, to reconcile this approach with the combination of meanings by function composition. In contrast to compositional approaches, we present a deductive approach to assembling meanings, based on reasoning with constraints, which meshes well with the unordered nature of information in the functional structure. Our use of *linear logic* as a `glue' for assembling meanings also allows for a coherent treatment of modification as well as of the LFG requirements of completeness and coherence. Return-Path: <@Sunburn.Stanford.EDU:aa@cauchy.Stanford.EDU> Date: Tue, 27 Apr 93 13:21:04 PDT From: aa@cauchy.Stanford.EDU (Arnon Avron) To: linear@cs.stanford.edu, sanjiva@ecrc.de Subject: Re: Mix Rule and Girardian Turnstile Sender: lincoln@cs.stanford.edu --text follows this line-- Some counterintuitive obvious consequence of the "Mix" rule are: 1) -(A-oA)-o(B-oB). Hence the principle of variable-sharing which is well known from the relevance literature (that A implies B only if A and B share some propositional variable) is violated. 2) (A-oB) par (B-oA) becomes a theorem. This hints in the direction of using Algebraic models in which the order relation is linear (but the lack of contraction makes things more complicated). I would like to use this opportunity to question the use of the name "mix" here. This name was used for years by proof-theorticians for a variant of the cut rule (equivalent to cut in the presence of the structural rules). See the papers of Gentzen and the books of Kleene and Takeuti. Mixing this with the rule discussed here is not a good idea. Relevance Logicians have used the name "mingle" for this rule for many years (The system R-mingle or RM in short is based on it). Another possible name is "combining". Arnon Avron (aa@cauchy.stanford.edu) Return-Path: <@Sunburn.Stanford.EDU:jean@saul.cis.upenn.edu> Subject: Girardian turnstyle Date: Mon, 26 Apr 1993 14:34:28 EDT From: Jean Gallier To: linear@cs.stanford.edu Sender: lincoln@cs.stanford.edu --text follows this line-- I don't know whether this is "the official" macro, but this is the one I used in my TCS survey paper (Vol. 110, No 2), and I think it gives a pretty good approximation of the Girardian turnstyle: \def\joinrelm{\mathrel{\mkern-3mu}} \def\relbar{\mathrel{\smash-}} \def\tailpiece{\vrule height 1ex width 0.3ex depth -.1ex} \def\seqsym{\mathrel{\tailpiece\joinrelm\relbar}} \def\sequent#1#2{#1 \seqsym #2} Example: $$\sequent{\Gamma}{\Delta}$$ -- Jean Gallier Return-Path: <@Sunburn.Stanford.EDU:bellin@maths.ox.ac.uk> From: bellin@maths.ox.ac.uk ( Dr G Bellin tel 2-76933) Date: Fri, 30 Apr 93 00:41:44 +0100 To: linear@cs.stanford.edu Subject: no-short-trips on additive proof-nets Sender: lincoln@cs.stanford.edu --text follows this line-- A paper available by anonymous ftp from theory.doc.ic.ac.uk: PROOF-NETS FOR MULTIPLICATIVE AND ADDITIVE LINEAR LOGIC April 1993 Gianluigi Bellin MALL-trips.ps MALL-trips.dvi.Z It contains a very simple formulation of proof-nets (without boxes) for MALL, using (a variant of) Girard's `no-short-trip' as correctness condition. Remember (Girard 1987) that a *principal switching* (for a certain formula A in a proof-net R) is a choice of the `par' switches as follows: in the part of the trip from the visit to A upwards to the visit downwards, if any `par' link is reached *for the first time from above*, then the trip returns immediately upwards. It is easy to see that the empire of A is precisely the part of the net visited during this part of the trip. (It follows that the computation of the empire of A is linear in the size of the net.) The main idea here is to regard *additive links* (namely, `with' links and additive contractions) as `ambivalent times-par links': in a trip they behave like `times' links when they are reached for the first time *from below* and as `par' links when they are reached for the first time *from above*. At the beginning of each trip we decide a switching for all the `times' and `par' links and also for the additive links, in case they behave like `times' links (independent switching). A principal switching for a formula occurrence can be regarded as a command which overruns the original switching in a part of the trip. Whenever an additive link, with premises X and Y, is reached for the first time from below, the trip continues from the premise chosen by the independent switch, say X; now a principal switching for X is enforced; when the trip returns to X, we know the empire of X and its `doors'. Next consider a trip exactly as before, except that at the additive link in question the switch is changed: such a trip continues from the other premise Y, and a principal switching for Y computes the empire of Y. Now compare the doors of eX and eY: if they `match' as premises of exactly one `with' link and of the same set of additive contractions (but not of any `par' link; also they cannot be conclusions of R), then the test is successful; otherwise, it fails. In fact, it is possible (as shown in the paper) to detect the `matching' of the doors already within one trip, so that an unsuccessful trip actually stops (`short trip'). Anyway, it is clear that the computation of `additive correctness' (i.e., the verification that the doors `match') is linear in the complexity of the verification of correctness of the net as a multiplicative structure. As long trips produce information about the empires of the premises of `with' links, we can easily reintroduce additive boxes, by replacing the `with' link and the associated additive contractions. A sketch of the present result was presented during a visit to the Universite' Paris VII in December 1992. Thanks to V.Danos for useful discussions. The present result improves previous work by the author (Bellin [1990, 1991]). The previous version of the paper (Bellin 1991) is in fact a different project, using another correctness condition for the multiplicatives, where the notion of empire is taken as primitive; it contains also results of slicing of additive nets and extensions of larger fragments. It is also available in the file MALL-nets.ps or MALL-nets.dvi.Z. References: Girard [1987] `Linear Logic' TCS Bellin [1990] `Mechanizing Proof Theory...', Thesis, Stanford CS-Dept. Rep. STAN-CS-90-1319 and Edinburgh CS-Dept Report ECS-LFCS-91-165 Bellin [1991] `Proof Nets for MALL', Edinburgh CS-Dept. ECS-LFCS-91-161. ----------------------------------------------------------------------------- The papers MALL-trips.dvi.Z MALL-nets.dvi.Z [use uncompress to obtain the dvi-files]; MALL-trips.ps MALL-nets.ps are available by anonymous ftp from theory.doc.ic.ac.uk The files are in the directory /papers/Bellin Return-Path: <@Sunburn.Stanford.EDU:tempus@queen.math.muni.cs> From: TEMPUS Subject: Announcement of Summer School To: linear@cs.stanford.edu Date: Mon, 10 May 1993 17:03:01 +0200 (MET DST) X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 2527 Sender: lincoln@cs.stanford.edu --text follows this line-- Tempus Summer School for Algebraic and Categorical Methods in Computer Science Second Announcement Brno, June 28 - July 3, 1993 Sponsored by the European Community TEMPUS office the organizers are pleased to announce an intensive course designed to serve its students as a forum for exchange of ideas between the disciplines of mathematics and computer science. Courses: P. J. Freyd (Philadelphia), Cartesian Logic and Cartesian Categories Y. Lafont (Paris), Linear Logic J. Lambek (Montreal), Categories and Deductive Systems C. P. Stirling (Edinburgh), Modal and Temporal Logics for Processes G. Winskel (Aarhus), Models and Logic for Concurrent Computation Special lecture: D. S. Scott (Linz), The Theory of Domains: Origin, Development, Future Lectures will be held starting Monday morning, June 28, to Saturday noon, July 3; Wednesday afternoon is reserved for social activities. Each course will consist of five lectures,one lecture per day. There will be a reception for participants on the evening of Sunday, June 27th. An afternoon-excursion will be organized, followed by a conference dinner. Fees: Conference fee is 220 DM, (tuition 100 DM, accomodation 120 DM). Price includes accomodation in double bedrooms, breakfast and lunch. The tuition fees can be supported by the organizers for a limited number of participants. Please apply! Registration: Please send name, address (including e-mail, if available) and gender to the organizing office by May 20, 1993.Please indicate if you plan to bring a guest or indicate the name of participant with whom you wish to share accommodation. Organizing Committee: Jiri Rosicky Anna Sekaninova Jan Slovak Address: TEMPUS SUMMER SCHOOL Department of Algebra and Geometry Masaryk University Janackovo nam. 2a 662 95 BRNO The Czech Republic e-mail: tempus@queen.math.muni.cs fax: 42-5-74 55 10 (later 42-5-41 21 03 37) phone: 42-5-74 56 66 Return-Path: <@Sunburn.Stanford.EDU:sanjiva@ecrc.de> Date: Thu, 13 May 93 11:39:40 +0200 From: Sanjiva Prasad To: linear@cs.stanford.edu Subject: Questions on LU and ITT Sender: lincoln@cs.stanford.edu --text follows this line-- I seem to have evermore questions as I learn more about proof theory, linear logic and LU. 1. Has a sequent presentation of Martin-Lo"f Intuitionistic Type Theory been published? 2. The next pair of questions are about the Intuitionistic fragments of LU and their relation to the traditional sequent calculi for Intuitionistic logic. From my undersanding of Girard's paper on LU, the translation of the intuitionistic fragments of LU into the traditional sequent calculi for intuitionistic logic are straightforward, but the other way things may be more delicate. Has someone proven a result showing that cut-free (resp. not necessarily cut free) intuitionistic proofs translate into cut-free (resp. not necessarily cut free) proofs within the intuitionistic fragment of LU (i.e. with sequents maintaining the specified restrictions at each stage in the proof). I would appreciate any information on the connections between LU's intuitionistic fragment and usual calculi for intuitionistic logic. Thanks, Sanjiva (sanjiva@ecrc.de) Sanjiva Prasad, Guest Magus E-mail: sanjiva@ecrc.de European Computer Industry Research Centre Off: +49 89 92 69 91 58 Arabellastrasse 17 Fax: +49 89 92 69 91 70 8000 Muenchen 81, Germany Res: +49 89 16 33 59 Return-Path: <@Sunburn.Stanford.EDU:dpym@dcs.ed.ac.uk> Date: Thu, 13 May 93 16:53:27 BST From: David J Pym Subject: Re: Questions on LU and ITT To: linear@cs.stanford.edu In-Reply-To: Sanjiva Prasad's message of Thu, 13 May 93 11:39:40 +0200 Sender: lincoln@cs.stanford.edu --text follows this line-- > I seem to have evermore questions as I learn more about proof theory, linear > logic and LU. > > 1. Has a sequent presentation of Martin-Lo"f Intuitionistic Type Theory been > published? My 1990 University of Edinburgh Ph.D. thesis contains, amongst other things, a sequent calculus for the lambdaPi-calculus, a theory of first-order dependent function types (just Pi, no Sigma, a fragment of ITT). This is discussed, as part of a different analysis, in ``Proof-search in the $\lambda\Pi$-calculus'', by D.J. Pym and L.A. Wallen. In: Logical Frameworks, Gerard Huet and Gordon Plotkin (editors), Cambridge University Press, 1991. I have just submitted a paper, ``A Note on the Proof Theory of the $\lambda\Pi$-calculus'' to a journal. This paper discusses the sequent calculus for lambdaPi and some resolution calculi that arise from it. I am preparing papers on these sorts of issues for Sigma types and also for PTSs. > > (This message was earlier posted to the logic mailing > list, but no responses were received.) > I read this list, but didn't get this message. Sincerely, David. (I believe he is referring to "logic@cs.cornell.edu" moderated by Bard Bloom. I received his earlier message to that list. - Patrick Lincoln, linear mod) Return-Path: <@Sunburn.Stanford.EDU:hars@logique.jussieu.fr> Date: Sun, 16 May 93 14:19:48 +0200 From: hars@logique.jussieu.fr To: linear@cs.stanford.edu Subject: IL -- LU -- LL Sender: lincoln@cs.stanford.edu --text follows this line-- In his message to the Linear mbox of Thu, 13 May 93, Sanjiva Prasad writes: "I seem to have evermore questions as I learn more about proof theory, linear logic and LU. [ ............. ] I would appreciate any information on the connections between LU's intuitionistic fragment and usual calculi for intuitionistic logic" The paper "On the linear decoration of intuitionistic derivations" (joint work of V.Danos, J.B. Joinet and myself) might be of help in gaining some insight. It is available by anonymous ftp from "gentzen.logique.jussieu.fr". You will find it in the directory pub/scratch as `Noble1.dvi'. There's also a compressed file, `Noble1.dvi.Z'. In the paper we mention e.g. how one can transform a given derivation in the (implicational fragment of) usual sequent calculus for intuitionistic logic into a derivation in the (neutral) intuitionistic fragment of LU. A general hint: if you have some experience with linear logic, think of the intuitionistic/classical LU-fragments via their `linear interpretation': write !p for positive atoms p, ?n for negative atoms n, x for neutral atoms x, and use the linear definitions of the connectives (you then will find that "formula F is positive" corresponds to "its linear interpretation [F] has the property that [F] <=> ![F] is provable in linear logic", and, dually, for "formula F is negative" we have "[F] <=> ?[F] is provable in LL"). Harold Schellinx (NB.: You might also be interested in a second paper, related to the one mentioned above. It is called "The Structure of Exponentials: Uncovering the Dynamics of Linear Logic Proofs", and can be found in the same ftp-directory as `StrucExp.dvi(.Z)' .) Return-Path: <@Sunburn.Stanford.EDU:streiche@informatik.uni-muenchen.de> Date: Tue, 18 May 93 15:31:09 +0200 From: Thomas Streicher To: linear@cs.stanford.edu Subject: geometry of interaction & categorical models of LL Sender: lincoln@cs.stanford.edu --text follows this line-- I have tried to make a categorical model out of the ingredient's of Girard's GEOMETRY of INTERTACTION I. It all works well for the multiplicative part. Objects : countable sets Morphisms : a morphism fromm X to Y is a partial injective map m : X + Y -> X + Y Composition : if m : X + Y -> X + Y and n : Y + Z -> Y + Z then n o m is defined as the union over all i : N : [inl,0,0,inr] o ((n+m) o [in1,in3,in2,in4])^i o (n + m) o [in1,in4] Of course, this is a model where linear negation is the identity on objects, i.e. what I call strong involution. There are no additives in this model. W.r.t. to EXPONTIALS there is some good candidate for obtaining a comonad ! . But there is a severe problem which already shows up on the level of DYNAMIC ALGEBRA : !(f) = !(f o d*) o t* does not hold or in other words !(f) = lift(deril(f)) does not hold. QUESTION Has anyone overcome this problem ? I guess in the Abramsky&Jagadeesan approach this problem can be avoided. WHY? Thomas Streicher Return-Path: <@Sunburn.Stanford.EDU:blute@triples.math.mcgill.ca> Date: Thu, 20 May 93 11:51:55 EDT From: blute@triples.Math.McGill.CA (Richard Blute) To: linear@cs.stanford.edu Subject: linear topology, hopf algebras and *-autonomous categories Sender: lincoln@cs.stanford.edu --text follows this line-- The following paper is available by anonymous ftp from the site triples.math.mcgill.ca. It is in the file pub/blute in dvi and ps format(compressed). Anyone who would like the paper and cannot access it this way can of course contact me. Regards, Rick Blute LINEAR TOPOLOGY, HOPF ALGEBRAS AND *-AUTONOMOUS CATEGORIES Richard F. Blute McGill University Abstract The goal of this paper is to construct models of variants of linear logic in categories of vector spaces. We begin by recalling work of Barr, in which vector spaces are augmented with linear topologies to obtain new examples of symmetric monoidal closed (autonomous) categories. The advantage of these categories is that they have large subcategories of reflexive objects which are also autonomous, in fact *-autonomous. Thus, we obtain models of (a fragment of) classical linear logic. These models have an advantage over other models arising from linear algebra in that they do not identify the two multiplicative connectives, tensor and par. Furthermore, the models will be complete and cocomplete. We then extend Barr's work to vector spaces with additional structure, in particular to representations of Hopf algebras. As special cases, we examine cocommutative Hopf algebras, and quasitriangular Hopf algebras, also known as quantum groups. In the quasitriangular case, the representations actually form a braided *-autonomous category, first defined by the author. They thus give a model of a braided variant of linear logic, also defined by the author. This is the first example of such a model which does not identify the two multiplicative connectives. Hopf algebras, and more generally bialgebras, have been of interest recently as a possible framework for the study of concurrency, in that they encode the paradigm of interleaving processes, also known as fair merge, as well as other structural operations on concurrent processes. This was first observed by D. Benson. As a result of the work in this paper, such bialgebras will yield models of a fragment of linear logic. While these models do not equate the multiplicative connectives they do validate the MIX rule, thus giving models of a slightly larger theory, first studied by Fleury and Retore. Also, if additional restrictions are placed on the Hopf algebra, we obtain models of cyclic linear logic, defined by Yetter.