Subject: LFG semantics via Constraints
From: Vijay Saraswat <[email-masked]>
To: [email-masked]
Date: Tue, 27 Apr 1993 10:09:52 PDT

--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, [email-masked]

		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:[email-masked]>
Date: Tue, 27 Apr 93 13:21:04 PDT
From: [email-masked] (Arnon Avron)
To: [email-masked], [email-masked]
Subject: Re:  Mix Rule and Girardian Turnstile
Sender: [email-masked]
--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 ([email-masked])


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Subject: Girardian turnstyle
Date: Mon, 26 Apr 1993 14:34:28 EDT
From: Jean Gallier <[email-masked]>
To: [email-masked]
Sender: [email-masked]
--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:[email-masked]>
From: [email-masked] ( Dr G Bellin tel 2-76933)
Date: Fri, 30 Apr 93 00:41:44 +0100
To: [email-masked]
Subject: no-short-trips on additive proof-nets 
Sender: [email-masked]
--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


From: TEMPUS <[email-masked]>
Subject: Announcement of Summer School
To: [email-masked]
Date: Mon, 10 May 1993 17:03:01 +0200 (MET DST)
Content-Length: 2527      
Sender: [email-masked]
--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: [email-masked]

                              fax: 42-5-74 55 10

                              (later 42-5-41 21 03 37)

                              phone: 42-5-74 56 66


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Thu, 13 May 93 11:39:40 +0200
From: Sanjiva Prasad <[email-masked]>
To: [email-masked]
Subject: Questions on LU and ITT
Sender: [email-masked]
--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					([email-masked])

Sanjiva Prasad,  Guest Magus				E-mail: [email-masked]
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:[email-masked]>
Date: Thu, 13 May 93 16:53:27 BST
From: David J Pym <[email-masked]>
Subject: Re: Questions on LU and ITT
To: [email-masked]
In-Reply-To: Sanjiva Prasad's message of Thu, 13 May 93 11:39:40 +0200
Sender: [email-masked]
--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 "[email-masked]" moderated 
 by Bard Bloom.  I received his earlier message to that list.
 - Patrick Lincoln, linear mod)


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Sun, 16 May 93 14:19:48 +0200
From: [email-masked]
To: [email-masked]
Subject: IL -- LU -- LL
Sender: [email-masked]
--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:[email-masked]>
Date: Tue, 18 May 93 15:31:09 +0200
From: Thomas Streicher <[email-masked]>
To: [email-masked]
Subject: geometry of interaction & categorical models of LL
Sender: [email-masked]
--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:[email-masked]>
Date: Thu, 20 May 93 11:51:55 EDT
From: [email-masked] (Richard Blute)
To: [email-masked]
Subject: linear topology, hopf algebras and *-autonomous categories
Sender: [email-masked]
--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.