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

Re: Categorical Models of Linear (and other) Logics



With regard to Greg Restall's recent question(s) about categorical models
of logics:

   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.

-----------------

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.

Roy Crole