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

Coherence for weakly distributive categories


 
We wish to announce that the following paper may be obtained by
anonymous ftp (details below) or directly from the authors.
 
 
 
   Natural deduction and coherence for weakly distributive categories
                                  by
          R.F. Blute, J.R.B. Cockett, R.A.G. Seely, T.H. Trimble
 
 
(The abstract follows, but first let us highlight some points for two
specific audiences:)
 
Some points that might interest categorists:
 
*  Proof of coherence for weakly distributive categories. (These are
a natural generalization of monoidal categories to include a second
"interwoven" tensor, the interweaving given by tensorial strength - the
"weak distributivities".)
 
*  New uses of logical techniques to prove coherence: proof nets and empires
(from linear logic).
 
*  Conservativity of the extension to *-autonomous categories.  (Here we
mean that the unit of the adjunction is fully faithful.)
 
 
 
Some points that might interest linear logicians:
 
*  By studying the weak fragment of linear logic that weakly
distributive categories represent, one can better get to the structure
of PAR vis a vis TIMES (without duality confusing the issue).
 
* Units are handled in a constructive version of the usual treatment:
we introduce "thinning links" to attach units to the net structure so as
to preserve the "acyclic and connected" net criterion, and then
determine how these links can be moved about without disturbing the
essential structure (coherence).
 
* Coherence represents (part of) the structure of the proof theory of
logic, namely when do proof structures represent "the same proof".
 
==========================================================================
 
                             ABSTRACT
 
We define a two sided notion of proof nets, suitable for categories, like
weakly distributive categories, which have the two-tensor structure
(TIMES/PAR) of linear logic, but lack a  NEGATION operator.  These proof
nets have a structure more closely parallel to that of traditional natural
deduction than Girard's one-sided nets do. In particular, there is no cut,
and cut elimination is replaced by normalization.  We prove a
sequentialization theorem for these nets and the corresponding sequent
calculus, and deduce the coherence theorem for weakly distributive
categories.  We also extend these techniques to cover the case of
non-symmetric ("planar") tensors.
 
We further extend the treatment of coherence
to include the units for the tensors, giving a
characterization of the Lambek equivalence relation on deductions (i.e.
equality of morphisms) in terms of the notion of empire.
 
Finally, we derive a conservative extension result for the passage from
weakly distributive categories to *-autonomous categories.
 
==========================================================================
 
To obtain a copy by anonymous ftp, ftp triples.math.mcgill.ca and login
as anonymous - use your email address as password; cd to the directory
pub/rags/nets and take the appropriate file:  either nets.dvi.Z or
nets.ps.Z  (you will have to uncompress them at your own site).
Contact rags@math.mcgill.ca if you have any trouble with the ftp process or
with printing the files at your site.