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

Natural deduction and coherence



We wish to announce the availability (by ftp or WWW) of the following paper
(revised version)

                     Natural deduction and coherence 
                    for weakly distributive categories

                                 by

         R.F. Blute, J.R.B. Cockett, R.A.G. Seely, and T.H. Trimble


ABSTRACT:
This paper examines coherence for certain monoidal categories using
techniques coming from the proof theory of linear logic, in particular
making heavy use of the graphical techniques of proof nets.  We define a two
sided notion of proof net, suitable for categories like weakly distributive
categories which have the two-tensor structure (times/par) of linear logic,
but lack a negation operator.  Representing morphisms in weakly distributive
categories as such nets, we derive a coherence theorem for such categories.
As part of this process, we develop a theory of expansion-reduction systems
with equalities and a term calculus for proof nets, each of which is of
independent interest.  In the symmetric case the expansion reduction system
on the term calculus yields a decision procedure for the equality of maps
for free weakly distributive categories.

The main results of this paper are these.  First we have proved coherence
for the full theory of weakly distributive categories, extending similar
results for monoidal categories to include the treatment of the tensor
units.  Second, we extend these coherence results to the full theory of
*-autonomous categories - providing a decision procedure for the maps of
free symmetric *-autonomous categories.  Third, we derive a conservative
extension result for the passage from weakly distributive categories to
*-autonomous categories.  We show strong categorical conservativity, in the
sense that the unit of the adjunction between weakly distributive and
*-autonomous categories is fully faithful.


NOTES:
This is a significant revision of an earlier version announced a year ago.
The paper has been completely rewritten, and has been enhanced in several
ways:  
1) We now treat the cases with non-logical axioms, and with non-commutative
tensor and par, in considerable detail, pointing out in passing where the
traditional treatment (of the pure commutative case) does not work in these
cases.  For example, the traditional proof of sequentiality (via splitting
links) does not work in the presence of non-logical axioms.  
2) We develop a term calculus for proof nets, and a theory of expansion -
reduction rewrite systems, both of which are of independant interest.
3) Using this new material has made the proofs clearer and more complete.


TO OBTAIN THE PAPER:
By ftp: ftp triples.math.mcgill.ca
        login as anonymous
        use your email address as password
        cd pub/rags/nets
        binary
        get nets.ps.gz        (or  nets.dvi.gz   if you prefer)

(You will have to gunzip this file to get the PostScript - or DVI - file for
the paper.)

By WWW (Mosaic, netscape, ...) My home page is:
   ftp://triples.math.mcgill.ca/pub/rags/ragstriples.html
   click on the item labelled with the paper's title
   - this will display the PostScript file.
   (other papers dealing with weakly distributive categories and proof nets
    may be found easily via my home page.)

(If you need to get gunzip, you can find it at pip.shsu.edu: issue the
command "quote site index gzip" once you have ftp'd the site to get a 
list of files suitable for various computer platforms.)


= rags =