by R.F. Blute, J.R.B. Cockett, and R.A.G. Seely
This is an early version of the paper, dealing with the "intuitionist" case. That is, the case where only single-formula conclusions are permitted. The full version is now available. The full version has no discussion of the "intuitionist" case, but proceeds directly to the full case. In addition, the full version has none of the discussion of proof circuits that occupies the final sections of the original version of the paper. Proof circuits for the full calculus will be covered in a sequel.
In this paper we introduce the notion of contextual categories. These provide a categorical semantics for the modelling of computation in context, based on the idea of separating logical sequents into two zones, one representing the context over which the computation is occurring, the other the computation itself. The separation into zones is achieved via a bifunctor equipped with a tensorial strength. We show that a category with such a functor can be viewed as having an action on itself. With this interpretation, we obtain a fibration in which the base category consists of contexts, and the reindexing functors are used to change the context.
We further observe that this structure also provides a framework for developing categorical semantics for Girard's Unified Logic, a key feature of which is to separate logical sequents into two zones, one in which formulas behave classically and one in which they behave linearly. This separation is analogous to the context/computation separation above, and is handled by our semantics in a similar fashion. Furthermore, our approach allows an analysis of the exponential structure of linear logic using a tensorially strong action as the primitive notion. We demonstrate that from such a structure one can recover a model of the linear storage operator.
Finally, we introduce a sequent calculus for the fragment of Unified Logic modeled by contextual categories. We show cut elimination for this fragment, and we introduce a simple notion of proof circuit, which provides a description of free contextual categories.