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

Notice of paper


We wish to announce the availability of the following paper, at the
URL given below.

The logic of linear functors
 by Richard Blute, J.R.B. Cockett, and R.A.G. Seely

It has been commonplace to base logics and type theories on
categorical doctrines; with this paper we propose a more general
paradigm, suggesting that logics and type theories may be based on
functorial doctrines.  This paradigm is very general - in particular,
it subsumes all of usual categorical logic and type theory as
degenerate cases.  So as to be able to make precise claims, we
illustrate this idea with a special case, developing the logic of
linear functors with sufficient detail to see that this one doctrine
is general enough to deal with basic linear modal logic and with the
Abrusci-Ruet mixed non-commutative linear logic.  We emphasise the
case where the logic is based on a single functor, but it will be
clear that one could also base it on a family of functors, which would
allow one to deal with process logic as considered by Hennessy and
Milner.

The paper's abstract is given in full below.
The paper may be found at
     http://www.math.mcgill.ca/rags/linear/lfl.ps.gz>
or go to R.A.G. Seely's home page
     http://www.math.mcgill.ca/rags/
and click on the appropriate link.

.........................................................

The logic of linear functors
  by Richard Blute, J.R.B. Cockett, and R.A.G. Seely

ABSTRACT:

This paper describes a family of logics whose categorical semantics is
based on functors with structure rather than on categories with
structure.  This allows the consideration of logics which contain
possibly distinct logical subsystems whose interactions are mediated
by functorial mappings. For example, within one unified framework, we
shall be able to handle logics as diverse as modal logic, ordinary
linear logic, and the "noncommutative logic" of Abrusci and Ruet, a
variant of linear logic which has both commutative and noncommutative
connectives.

Although this paper will not consider in depth the categorical basis
of this approach to logic, preferring instead to emphasize the
syntactic novelties that it generates in the logic, we shall focus on
the particular case when the logics are based on a linear functor, to
give a definite presentation of these ideas.  However, it will be
clear that this approach to logic has considerable generality.

There have been several individual attempts to develop logics with
distinct but related subsystems of connectives, such as the
Abrusci--Ruet noncommutative logic and the bunch logic of O'Hearn and
Pym; generally these are presented in terms of "bunching" the formulas
in the sequents of the logics via different "punctuation".  The
present functor logic, by contrast, uses a system of "formula blocks",
which represent the functorial action and which give finer control
over what logical features may be displayed.  By displaying a family
of functor logics, we illustrate how different logical systems can be
developed along these lines, logics which are primarily distinguished
by the degree to which they permit nesting of formula blocks. Our
examples will include a basic logic where there is essentially no
nesting, a system of linear modal logic, which allows nesting, but has
only one system of connectives, and the Abrusci--Ruet logic, where
nesting is virtually unrestricted and there are two subsystems of
connectives.  We finish by showing how to translate between the
``bunch'' style of logic and our ``formula block'' or functor logic
using the Abrusci--Ruet noncommutative logic as an example.


==================
R.A.G. Seely
<rags@math.mcgill.ca>
<http://www.math.mcgill.ca/rags>