Re: Categorical Models of Linear (and other) Logics
With regard to Greg Restall's recent question(s) about categorical models
Possible answers are as follows.
1. They help us understand our term assignment systems for
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.
As Uday Reddy comments, a prime use of category theory in computer science
is finding models of logics and type theories, that is, finding a general
categorical model which tells us about many of the abstract properties of all
models. (Knowing the properties of models in the abstract can sometimes
give guidance towards finding particular [instances of the categorical] models.)
It is certainly true that category theory can be used to prove results about
logics and type theories. An example that is quite well known is to show that
if a simply typed lambda calculus is generated by an algebraic theory, then any
closed lambda term of ground type is equal to an algebraic term, and all such
terms are equal. This can be proved both operationally and categorically.
A recent experience of mine was to prove a similar result for a richer
type theory. An operational proof would have been difficult, but two
changes in the categorical method for lambda calulus yielded a proof---the
technical details of the proof were different from that for lambda calculus,
but the overall strategy was the same.
Finally, a comment about deriving categorical models. An important observation
is that a categorical model is a "general" model which satisfies certain
basic requirements. For simple type theories, such requirements are that
"substitution is modelled by composition" and that "term formation rules are
modelled by natural transformations". Matching these categorical concepts
closely with a logic often gives excellent guidance as to the final
definition of a logic and its models.