Subject: Roma
From: Claudia Casadio <[email-masked]>
To: [email-masked]
Date: Fri, 11 Jun 93 07:55:41 SET

--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:[email-masked]>
To: [email-masked]
Subject: Full ILL paper
Cc: [email-masked]
Date: Fri, 25 Jun 93 17:27:54 +0100
From: Valeria de Paiva <[email-masked]>
Sender: [email-masked]
--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: <<Your e-mail address>>
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: [email-masked]
Cambridge CB2 3QG, England, UK     | Internet: [email-masked]
------------------------------------------------------------------------------


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Thu, 8 Jul 1993 18:07:57 +0200
From: Serena Cerrito <[email-masked]>
To: [email-masked]
Subject: limited use of exponentials
Sender: [email-masked]
--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}") 


Date: Fri, 16 Jul 1993 11:32:05 +0200
From: [email-masked] (Anne S. Troelstra )
To: [email-masked]
Subject: papers by ftp
Content-Length: 596
Sender: [email-masked]
--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:[email-masked]>
Date: Thu, 22 Jul 1993 23:19:37 +0100
To: [email-masked]
From: [email-masked] (Alessio Guglielmi)
X-Sender: [email-masked]
Subject: commutative and non-commutative tensor
Sender: [email-masked]
--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 <[email-masked]> Nax Mendler,
>[email-masked] 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:  [email-masked] .
>
>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:[email-masked]>
Date: Fri, 23 Jul 93 14:05:20 CDT
From: [email-masked] (LG Meredith)
To: [email-masked]
In-Reply-To: Alessio Guglielmi's message of Thu, 22 Jul 1993 23:19:37 +0100 <[email-masked]>
Subject: commutative and non-commutative tensor
Sender: [email-masked]
--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: <[email-masked]>
To: [email-masked]
Subject: Re: commutative and non-commutative tensor
In-Reply-To: Your message of Fri, 23 Jul 93 14:05:20 CDT.
	     <[email-masked]>
Date: Sat, 24 Jul 93 08:21:52 PDT
From: [email-masked]
Sender: [email-masked]
--text follows this line--

	Date: Fri, 23 Jul 93 14:05:20 CDT
	From: [email-masked] (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:[email-masked]>
Date: Mon, 26 Jul 93 14:40:48 +0200
From: [email-masked] (Christian Retore)
To: [email-masked]
Sender: [email-masked]
--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


Date: Mon, 26 Jul 1993 11:34:58 +0100 (BST)
From: Samson Abramsky <[email-masked]>
To: [email-masked]
Subject: The full abstraction problem for PCF
Sender: [email-masked]
--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:  <<your e-mail address>>
ftp> cd papers/Abramsky
ftp> binary
ftp> get gfapcf.dvi   
ftp> quit


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Subject: Games and Full Abstraction for PCF: Joint Announcement
Date: Tue, 27 Jul 93 16:45:24 +0100
From: Luke Ong <[email-masked]>
To: [email-masked]
Sender: [email-masked]
--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