×

\(*\)-autonomous categories and linear logic. (English) Zbl 0777.18006

The author sets out to show that \(*\)-autonomous categories [the author, \(*\)-autonomous categories (Lect. Notes Math. 752) (1979; Zbl 0415.18008)] are a model for a large fragment of linear logic, though not for the whole of it.
The paper includes a construction, due to the author’s student P.-H. Chu [see the appendix of the cited book], of the \(*\)-autonomous completion of a finitely complete autonomous category.
An autonomous category is a closed symmetric monoidal category. It is \(*\)-autonomous if in addition it has an object \(\perp\), the “dualizing object”, such that for any object \(A\), the canonical map to the second dual of \(A\) with respect to \(\perp\) is an isomorphism.
Examples of \(*\)-autonomous categories: the category of finite-dimensional vector spaces over a field (the dualizing object is the field), the category of complete inf-lattices (the dualizing object is the 2-element lattice) and the category of sets and relations (the dualizing object is the one-element set).
Given a finitely complete autonomous category \(\mathcal V\) an a fixed object \(\perp\), Chu’s construction gives a \(*\)-autonomous completion \({\mathcal V}_ \perp\) in which \(\perp\) becomes the dualizing object. If \(\mathcal V\) is a complete and cocomplete autonomous category then for any object \(\perp\) of \(\mathcal V\), its completion \({\mathcal V}_ \perp\) is also a complete and cocomplete \(*\)-autonomous category.
A model of full linear logic is a \(*\)-autonomous category equipped with a cotriple \({\mathcal G}=3D (!,\epsilon,\delta)\) such that \(!(A\times B)\) is isomorphic to \(!A\otimes!B\). This is the case in particular for the category of sets and relations. It also works for the category of relations in a topos that has at least countable limits.
One can somewhat modify Chu’s construction so that if one starts with a Cartesian closed category, one obtains a model of full linear logic; this is done in section 6.
In section 7 the author shows there is a full and faithful functor from \({\mathcal V}\) to \({\mathcal A}=3D{\mathcal V}_ \perp\), with a suitable choice of the dualizing object.
The following section gives an adjoint functor existence theorem applying in particular in the case of section 8.
Section 9 shows that the category of separated objects for \({\mathcal V}_ \perp\) is a model of full linear logic.
The next section gives an example, while the following one explains why simple recursion does not work.
The last section discusses briefly related work by de Paiva and Laffont.

MSC:

18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
03B20 Subsystems of classical logic (including intuitionistic logic)
03B70 Logic in computer science

Citations:

Zbl 0415.18008
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Seely, Contemporary Mathematics 92 pp 371–
[2] DOI: 10.1007/BFb0018360 · doi:10.1007/BFb0018360
[3] Paiva, Contemporary Mathematics 92 pp 47– (1989)
[4] Barr, Lecture Notes in Mathematics 752 (1979)
[5] Eilenberg, Proc. Conf. Categorial Algebra pp 421– (1966) · doi:10.1007/978-3-642-99902-4_22
[6] DOI: 10.1016/0022-4049(89)90163-1 · Zbl 0693.18003 · doi:10.1016/0022-4049(89)90163-1
[7] Chu, Lecture Notes in Mathematics 752 (1979)
[8] Makkai, Contemporary Mathematics 104
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.