[Prev][Next][Index][Thread]
Paper on linear bicategories and non-commutative linear logic
I would like to announce the following paper, which has been posted on
my www site <http://www.math.mcgill.ca/~rags>. (The McGill ftp site is
currently not functionning, but as soon as it is restored, this paper
ought to appear on the Hypatia mirror site as well.)
Readers of the TYPES list in particular might be interested in the
following aspects of the paper.
1) The main focus of this paper essentially is the semantics of non-
commutative multiplicative linear logic (both the ordinary and the
cyclic varieties). The structure of a bicategory may be viewed as the
representation of tensor structure by composition (for example,
functional composition, relational composition, etc.). Linear
bicategories represent both the tensor and the par of linear logic as
compositions. In fact, a primary model of linear bicategories is given
by relations, tensor being the usual relational composition and par its
deMorgan dual. In this sense, linear bicategories give a semantics for
a logic of generalised relations.
2) Since composition is naturally a non-commutative operation, linear
bicategories give a natural (perhaps the "first" natural) semantics for
non-commutative linear logic, clarifying what the appropriate aspects of
that theory are. We exploit this in the paper by giving a detailed
study of the coherence conditions necessary for a smooth development of
the proof-theory of the logic.
3) This setting presents a wealth of analogies which we begin to explore
in the paper. For example, in compositional settings, the notion of
adjoint is fundamental; in the linear setting, the corresponding notion
turns out to be complementation, and so leads to a better understanding
of negation in non-commutative linear logic. Our contention is that
linear bicategories are a natural context for understanding the
algebraic structure of non-commutative linear logic.
The abstract follows.
===================================
Introduction to linear bicategories
by J.R.B. Cockett, J. Koslowski, R.A.G. Seely
Linear bicategories are a generalization of the notion of a bicategory,
in which the one horizontal composition is replaced by two (linked)
horizontal compositions. These compositions provide a semantic model for
the tensor and par of linear logic: in particular, as composition is
fundamentally noncommutative, they provides a suggestive source of
models for noncommutative linear logic.
In a linear bicategory, the logical notion of complementation becomes a
natural linear notion of adjunction. Just as ordinary adjoints are
related to (Kan) extensions, these linear adjoints are related to the
appropriate notion of linear extension.
There is also a stronger notion of complementation, which arises, for
example, in cyclic linear logic. This sort of complementation is
modelled by cyclic adjoints. This leads to the notion of a *-linear
bicategory and the coherence conditions which it must satisfy. Cyclic
adjoints also give rise to linear monads: these are, essentially, the
appropriate generalization (to the linear setting) of Frobenius
algebras.
A number of examples of linear bicategories arising from different
sources are described, and a number of constructions which result in
linear bicategories are indicated.
This paper is dedicated to Jim Lambek, as part of the celebration of his
75th birthday.