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

Categorical Models of Linear (and other) logics



   Date: Mon, 6 Mar 1995 09:53:18 +1000
   From: Greg Restall <Greg.Restall@cisr.anu.edu.au>

   * What are categorical models of logics good for?

   Possible answers are as follows.
   1. They help us understand our term assignment systems for 
      these logics.
   2. They help us prove results about our logics, as we can 
      use category theory.
   3. We can show that our favourite logic corresponds to some
      already-found structure in category theory, and hence, our
      logic gets brownie-points for being `natural.'
   4. The category (or class of categories) we are interested in
      is the *intended model* for our logic.

While I cannot speak for logicians, I often think of programming
languages as constructive logics with certain constants (or axioms)
added.  So, I would translate the question as

  "what are categorical models of programming languages good for?" 

and answer it as follows.

>From my point of view, the most overriding purpose of categorical
models is that they help us in finding *models*.  Categorical models
embody a very good algebraic chacterization of what a model should be.
This is an essential guide to finding good models.  One sees that
almost all recent work in semantics is using categorical models in
this fashion. See e.g. [1] in the context of linear logic.  Secondly,
categorical models have a good deal of work done already.  Certain
facts hold for 'abstract reasons' and certain requirements must be met
for 'abstract reasons'.  Categorical analysis is well-suited for
dealing with such abstract reasons without getting lost in the
inessential detail of a particular model.

Thinking syntactically, categorical analysis also focuses on what
equivalences must hold between terms (or proofs).  In [2], Benton et
al. show, for example, that most of the equivalences induced by
cut-elimination and proof normalization are subsumed by the
equivalences one expects for abstract reasons.  This is quite
remarkable.  In programming, reasoning about equivalences is crucial.
Any theory that can give us a handle on equivalences is very valuable.

Finally, since categorical models describe classes of models, they are
useful for proving results that hold for entire classes of models.
For example, O'Hearn et al. [3] prove an important property of
'coherence' for a class of models described categorically.  I think
the proof is easier (in certain ways) as well as general, by doing it
at the categorical level rather than in a particular model.

I think most of this is talking about your answer 4, while touching on
answer 2.  The remaining answers are perhaps less significant in the
long run, though they are important as well.

Cheers,
Uday Reddy


[1] Abramsky, S. and Jagadeesan, R., "Games and Full Completeness for
Multiplicative Linear Logic", JSL, 59(2):543-574, 1994.

[2] Benton, P. N. and Bierman, G. M. and de Paiva, V. C. V. and
Hyland, J. M. E., "Term Assignment for Intuitionistic Linear Logic",
"Computer Laboratory, University of Cambridge", Aug. 1992.

[3] O'Hearn, P. W. and Power, A. J. and Takeyama, M. and Tennent, R.
D., "Syntactic Control of Interference Revisited", Proc. Math.
Foundations of Program. Semantics: 11th Intern. Conf., Tulane
University, New Orleans, Mar 1995.  (To appear.)

All these papers are available electronically from Imperial College
archives.