[Prev][Next][Index][Thread]
Linear logic semantics
Date: Sat, 21 Dec 91 14:21:33 EST
In a recent note on this net, Arnon Avron said that he thought most recent
research on LL has been proof-theoretical, and it is strange that more on
semantics has not been done. He subsequently clarified this to indicate
that he meant there had been little proof-theoretic work he was aware of
using semantic techniques. Rick Blute and I responded with several notes,
to him and to the net, dealing with the original question as we understood it,
and also the more specific one about proof theory. Here is an edited version
of those remarks; we hope they might be of some interest to the TYPES audience.
Re semantics of linear logic: we wish to point out that there is a large
and active body of work on the semantics of linear logic already in the
literature, with new preprints appearing at a rapid rate.
There have been papers on the semantics of LL in the past two LICS, in
conference proceedings of meetings on Category Theory in Computer
Science in Boulder (AMS Contemporary Mathematics 92),
Manchester (SLNCS 398), Paris (SLNCS 530), Durham (LMS to appear), to name a
few, not to mention papers in Math Str in Comp Sci, and the initial book of
Barr's (SLNM 752) which shows that the study of the semantics of this logic
predates the syntax of the logic itself. Of course, a lot of this is
"categorical", but then perhaps that is because that is a natural place to
study semantics generally. In particular, AA asks what is the connection
between his results and proof nets/theory: this is explicitly dealt with
in, among other places, Blute's work on autonomous deductive systems
(as in SLNCS 530 and TCS, to appear).
As another example, in Cockett & Seely, Weakly Distributive Categories,
(Durham proceedings to appear) we define the notion of shift monoid. AA's
assignment v is just the (canonical and unique) interpretation of the
initial model (the term model) in a shift monoid defined on Z, the
integers. (The LL structure these monoids have is essentially as in Barr's
preprint "Fuzzy models of linear logic" - Barr adds the additive units,
as points at +- infinity, which AA didn't consider.) AA's theorem then
is essentially just that the shift monoids on Z are *-autonomous categories.
If one restricts to the multiplicative fragment, then the discrete structure
(ignore the order on Z) is a model, which is why he can conclude vA = c then.
We note that he only claims soundness---completeness would be very interesting.
We might also point out, concerning the categorical approach, that the
distinction between semantics and syntax is blurred, so it does provide a
good context in which to mix techniques from each. This constructive
ambiguity has proved useful in categorical proof theory, and some of the
work we refer to above suggests this may well be the case in linear logic as
well.
Of course, this is not to suggest that the categorical approach is the only
worthy approach - in our game, we can use as many tools in our toolkit as
possible.
Robert Seely <rags@triples.math.mcgill.ca>