A categorical semantics for polarized MALL (Q866570)

Polarized formulas were introduced by Girard for the constructive version LC of classical logic based on linear logic. They are related to focussing in linear logic proof search. They are also mentioned in many papers on game semantics. Polarized versions of linear logic were introduced by \textit{O. Laurent} [Étude de la polarisation en logique. Thèse de doctorat (2002)] with polarized proof structures and nets. He used proof-theoretical and semantical techniques and results for polarized logics, notably full polarized linear logic LLP. For this theory the exponentials are polarity changing operations. Laurent mentions the polarized multiplicative fragment MALLP of LLP, which is the main syntax of \textit{J.-Y. Girard}'s ludics (without weakening) [``Locus solum: From the rules of logic to the logic of rules'', Math. Struct. Comput. Sci. 11, 301--506 (2001; Zbl 1051.03045)]. A fundamental point of MALLP is that the polarity-changing operations \(\uparrow\) and \(\downarrow\) are more primitive than the full exponentials. It was shown by Laurent that \textit{P. Selinger}'s control categories [``Control categories and duality: On the categorical semantics of the lambda-mu calculus'', Math. Struct. Comput. Sci. 11, 207--260 (2001; Zbl 0984.18003)] give an adequate model for LLP, but he did not give natural categorical models for MALLP, although he gave a notion of linear control category model for MALLP. To construct this model one needs canonical morphisms that do not live in the syntax. The present paper introduces a natural categorical framework for MALLP based on an ambient *-autonomous category \(\mathcal{C}\) together with reflective (resp. coreflective) subcategories \(\mathcal{C}_{-}\) and \(\mathcal{C}_{+}\) of polarized objects together with their associated adjunction and bimodule structure. If you don't assume the ambient \(\mathcal{C}\) is *-autonomous you obtain essentially pre-*-autonomous situations as defined by \textit{M. Barr} [{*}-autonomous categories. Lect. Notes Math. 752. Berlin-Heidelberg-New York: Springer-Verlag (1979; Zbl 0415.18008)]. They are discussed in Section 3 and Appendix A. More recently, \textit{J. R. B. Cockett} and \textit{R. A. G. Seely} [``Polarized category theory, modules and game semantics'', Theory Appl. Categ. 18, 4--101 (2007; Zbl 1117.03071)] have defined their notion of polarized categories motivated by AJ games [\textit{S. Abramsky} and \textit{R. Jagadeesan}, ``Games and full completeness for multiplicative linear logic'', J. Symb. Log. 59, 543--574 (1994; Zbl 0822.03007)] with an elaborate theory of focalized syntax, (2-sided) proof nets, and abstract games based on categorical proof theory. The present work was begun independently of theirs in order to model directly O. Laurent's MALLP. After talking to R. Cockett and R. Seely, the present authors have realized that their framework is a special case of their more general one; they have also become aware that structures similar to their's have arisen in (mostly unpublished) work of Melliès and Selinger [\textit{P.-A. Melliès}, ``Asynchronuous games. III. An innocent model of linear logic'', in: CTCS 2004, Electron. Notes Theor. Comput. Sci. 122, 171--192 (2005); ``Categorical models of linear logic, revisited'', Theor. Comput. Sci. (to appear)] also inspired by game semantics. So the kind of structures dealt with in the paper under review, which essentially go back to M. Barr in a different setting, are apparently a natural framework for polarized logics. Section 2, ``Syntax of polarized MALL'', defines polarized MALL (MALLP) and polarized multiplicative linear logic (MALLP) and gives the following proposition: Proposition [Focalization Property]: If \(\vdash \Gamma\) is provable in MALLP, then the sequence \(\Gamma\) contains at most one positive formula. This was proved by \textit{O. Laurent} [``Polarized proof-nets: Proof-nets for LC'', Lect. Notes Comput. Sci. 1581, 213--227 (1999; Zbl 0933.03081); Étude de la polarisation en logique. Thèse de doctorat (2002)]. Section 3, ``The categorical framework'', presents a categorical framework for proofs in polarized MALL based on the notion of categorical bimodule; the models are called polarized categories, a slightly modified version of \textit{M. Barr}'s pre-*-autonomous situations [loc. cit.]. After some definitions the authors prove several de Morgan-like laws and discuss an adjoint equivalence in polarized categories. Section 4, ``Interpretations of proofs and soundness'', interprets proofs of MALLP in a polarized *-autonomous category \(\mathcal{C}_{+, -}\) and proves soundness. Section 5, ``Examples of polarized categories'', presents many non-game-theoretic examples of the authors' frameworks, including \textit{T. Ehrhard}'s hypercoherences [``Hypercoherences: A strongly stable model of linear logic'', Math. Struct. Comput. Sci. 3, 365--385 (1993; Zbl 0802.68079)], Chu spaces, and various models based on double gluing and iterated double gluing. Section 6, ``Dinatural frameworks'', and Section 7, ``Completeness theorems'', start the authors' main focus: a study of full completeness theorems for polarized logics. Section 8, ``Some remarks on faithfulness'', discusses a theory of equations between MALLP proofs and gives a criterion for faithfulness. Section 9, ``Conclusion, other results and open problems'', does exactly that. Appendix A, ``On polarized categories à la M. Barr'', discusses M. Barr's *-autonomous categories and shows his approach to be much closer to polarized linear logic, that forms the basis of what the authors call a polarized category, than previous approaches. Appendix B, ``Double gluing'', defines the double gluing category of a given category and shows it to be a *-autonomous category if the initial one was. Finally it defines products and coproducts in the double gluing category and remarks that the evident forgetful functor from the double gluing category to the initial one is *-autonomous with left and right adjoints.