[Prev][Next][Index][Thread]
Soundness of Seely's models
There has been some discussion on this group of late about the lack of
soundness of the categorical model of linear logic I proposed many
many years ago. This is just a short note to suggest that it might
help if a sense of proportion were maintained here. A little history
too might clarify things. The current situation is nicely summarized
in the paper (to appear in the proceedings of the conference on typed
lambda calculus and applications, LNCS, April 1995, also available by
FTP as announced in a previous posting at theory.doc.ic.ac.uk in
/theory/imported/BiermanGM) of Gavin Bierman "What is a Categorical
Model of Intuitionistic Linear Logic?" - namely that in order to
model all the term equalities of Benton, Bierman, de Paiva, and
Hyland, one must add the requirement that the adjucntion between the
original category C and the Kleisli category C_! be _monoidal_. I
agree that this requirement is desirable, and I think that Bierman has
done the categorical community a service in pointing this out. It
will be clear however that this is a technical matter that does not
affect the original point - which was that the main insight of
Girard's original analysis of intuitionistic implication in terms of
linear implication and the exponential ! amounted to a passage to the
Kleisli category of a cotriple. This point was realised by a number of
people at the time, and as I said in my Boulder paper, this plus
Barr's analysis of *-autonomous categories was a striking instance of
research preceeding its most striking application. (This is even more
true of the Chu construction, as Vaughan has repeatedly pointed out.
SLNM 752 was remarkably prescient.)
The original notion of categorical model I proposed has been found
useful by a number of researchers, many of whom have encouraged me to
post this note; it would be a pity if its simplicity and appeal were
to be abandoned because of an ill-understood rumour. I suggest any
who are interested in this issue to read Bierman's paper before coming
to any conclusion. The correction (though necessary) is not profound.
(It certainly is of no interest to those who still think of proof
theory as having the structure of a preorder rather than a category -
this is entirely a coherence question involving the notion of
"equality of proofs".)
It is not my purpose here to defend the earlier paper - it did what it
stated it intended to do, and (as Bierman points out) the term
equalities were not known then (it took some time to get them right).
But the addition of the further commutative diagrams necessary to
ensure that the adjunction be monoidal does make sense to me. In
fact, in the recent paper by Blute, Cockett, Seely (! and ?: Storage
as tensorial strength) similar commutative diagrams are given among
the coherence conditions needed for weakly distributive categories
with ! and ?.
= RAG Seely =