A categorical semantics for polarized MALL

Masahiro Hamano, Philip Scott

研究成果: Article同行評審

9 引文 斯高帕斯(Scopus)

摘要

In this paper, we present a categorical model for Multiplicative Additive Polarized Linear Logic MALLP, which is the linear fragment (without structural rules) of Olivier Laurent's Polarized Linear Logic. Our model is based on an adjunction between reflective/coreflective full subcategories C-/C+ of an ambient *-autonomous category C (with products). Similar structures were first introduced by M. Barr in the late 1970's in abstract duality theory and more recently in work on game semantics for linear logic. The paper has two goals: to discuss concrete models and to present various completeness theorems. As concrete examples, we present (i) a hypercoherence model, using Ehrhard's hereditary/anti-hereditary objects, (ii) a Chu-space model, (iii) a double gluing model over our categorical framework, and (iv) a model based on iterated double gluing over a *-autonomous category. For the multiplicative fragment MLLP of MALLP, we present both weakly full (Läuchli-style) as well as full completeness theorems, using a polarized version of functorial polymorphism in a double-glued hypercoherence model. For the latter, we introduce a notion of polarized ↑-softness which is a variation of Joyal's softness. This permits us to reduce the problem of polarized multiplicative full completeness to the nonpolarized MLL case, which we resolve by familiar functorial methods originating with Loader, Hyland, and Tan. Using a polarized Gustave function, we show that full completeness for MALLP fails for this model.

原文English
頁(從 - 到)276-313
頁數38
期刊Annals of Pure and Applied Logic
145
發行號3
DOIs
出版狀態Published - 2007 3月

All Science Journal Classification (ASJC) codes

  • 邏輯

指紋

深入研究「A categorical semantics for polarized MALL」主題。共同形成了獨特的指紋。

引用此