[Prev][Next][Index][Thread]

Announcement of paper: FILL


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]


We wish to announce the following paper made available for ftp on our
WWW site.

            Proof theory for full intuitionistic linear logic,
                  bilinear logic, and mix categories
                                  by
                    J.R.B. Cockett and R.A.G. Seely


ABSTRACT
This note is a survey of techniques we have used in studying coherence
for monoidal categories with two tensors, corresponding to the tensor -
par fragment of linear logic.  We apply these ideas to several
situations which extend our previous work, in particular, the Full
Intuitionistic Linear Logic (FILL) of Hyland and de Paiva, and the
Bilinear Logic of Lambek. Note that the latter is a noncommutative
logic; we also consider the noncommutative version of FILL.  We show
that the essential difference between FILL and multiplicative linear
logic lies in making a tensorial strength natural transformation an
isomorphism. We briefly discuss the structure of the nucleus of a
category modelling FILL: the nucleus is a *-autonomous full subcategory.
In addition, we define and study the appropriate categorical structure
corresponding to the mix rule. For all these structures, we do not
restrict consideration to ``pure'' logic, in that we allow for the
inclusion of non-logical axioms. We define the appropriate notion of
proof nets for these logics, and use them to describe coherence results
for the corresponding categorical structures.


We would draw your attention to the following "highlights":
 - we develop proof nets for FILL (as well as bilinear logic - but this
latter is shown equivalent to the system of non-commutative *-autonomous
categories we studied in an earlier paper [BCST],
<ftp://triples.math.mcgill.ca/pub/rags/nets/nets.ps.gz>
so that is not new).
 - we show several equivalent formulations of bilinear logic =
non-commutative $*$-autonomous categories.  One interesting one is that
if one requires of a FILL category that a natural transformation
equivalent to the tensorial strength given by the weak distributivity is
isomorphic, then you get the full bilinear logic.
 - we introduce a generalisation of the notion of "nuclear map" suitable
for weakly distributive categories, and show the nucleus of a FILL
category is *-autonomous.
 - we give a rigorous definition of what it means for a category to
satisfy the MIX rule (previous attempts dealt only with the existence of
the required maps, and not the necessary coherence also needed), and
prove a coherence theorem for this doctrine.
 - these last two points are linked by the observation that a weakly
distributive category satisfies MIX iff its nucleus does.  As a
consequence we note that "cartesian" weakly distributive categories
(where the tensor is cartesian product) must satisfy MIX.


The paper is available by ftp at the URL
  <ftp://triples.math.mcgill.ca/pub/rags/nets/fill.ps.gz>  or
  <ftp://triples.math.mcgill.ca/pub/rags/nets/fill.dvi.gz>
as well as on the home page
  <http://www.math.mcgill.ca/~rags>
For assistance with ftp, please contact rags@math.mcgill.ca.

Robin Cockett <robin@cpsc.ucalgary.ca>
Robert Seely  <rags@math.mcgill.ca>