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

Categorical models of linear logic.



Whilst we're on the subject of categorical models of ILL and
their relationship to models of ordinary IL, it seems I might
usefully advertise the availability of

@techreport{benton:mixed,
  author="P.~N.~Benton",
  title="A Mixed Linear and Non-Linear Logic: 
Proofs, Terms and Models (Preliminary Report)",
  institution=CUCL, month=Sep, year=1994,
  number="352"
}
which also addresses some of the issues which have been
discussed recently. In particular, one of the contributions
of the paper is the result that the notion of model given in our
earlier papers (Benton, Bierman, de Paiva, Hyland) is equivalent
to having a symmetric monoidal adjunction between a SMCC and a
CCC. Thus, assuming one believes that logical operations should
behave well with respect to contexts, our notion of model is
just what one obtains by assuming that there is a way to embed
ordinary IL into ILL. In other words, we have a semantic
reconstruction of the ! operation. I have included the abstract
below.

The paper is available via the WWW at
 http://www.cl.cam.ac.uk/users/pnb/mixed3.dvi.Z
or by anonymous ftp from
  ftp.cl.cam.ac.uk
in
 /ESPRIT/LOMAPS/LOMAPS-CAMCL-2.dvi.Z


\begin{abstract}
Intuitionistic linear logic regains the expressive power of
intuitionistic logic through the ! (`of course') modality.
Benton, Bierman, Hyland and de Paiva have given a term
assignment system for ILL and an associated notion of
categorical model in which the ! modality is modelled by a
comonad satisfying certain extra conditions. Ordinary
intuitionistic logic is then modelled in a cartesian closed
category which arises as a full subcategory of the category of
coalgebras for the comonad.  

This paper attempts to explain the connection between ILL and IL
more directly and symmetrically by giving a logic, term calculus
and categorical model for a system in which the linear and
non-linear worlds exist on an equal footing, with operations
allowing one to pass in both directions. We start from the
categorical model of ILL given by Benton, Bierman, Hyland and de
Paiva and show that this is equivalent to having a symmetric
monoidal adjunction between a symmetric monoidal closed category
and a cartesian closed category. We then derive both a sequent
calculus and a natural deduction presentation of the logic
corresponding to the new notion of model.
\end{abstract}

Nick Benton