On Geometry of Interaction for Polarized Linear Logic

We present Geometry of Interaction (GoI) models for Multiplicative Polarized Linear Logic, MLLP, the multiplicative fragment (without structural rules) of Olivier Laurent's Polarized Linear Logic. This is done by uniformly adding multipoints to various categorical models of GoI. Multipoints are shown to play an essential role in semantically characterizing the dynamics of proof networks in polarized proof theory. They permit us to characterize the key feature of polarization, focusing, as well as playing a fundamental role in helping us construct concrete polarized GoI models. Our approach to polarized GoI involves two independent studies based on different categorical approaches to GoI. (i) Inspired by work of Abramsky, Haghverdi, and Scott, a polarized GoI situation is defined which adds multipoints to a traced monoidal category with an appropriate reflexive object U. Categorical versions of Girard's Execution formula (taking into account the multipoints) are defined, as well as the GoI interpretation of MLLP proofs. The Execution formula is shown to characterize the focusing property (thus polarities) as well as the dynamics of cut-elimination. (ii) The Int construction of Joyal-Street-Verity is another fundamental categorical structure associated to GoI. Here, we investigate it in a multipointed setting compatible with the existence of certain weak pullbacks. This yields a method for constructing denotational models of MLLP, in particular a compact version of Hamano-Scott's polarized categories. These are built from a contravariant duality between so-called positive and negative monoidal categories, along with an appropriate module structure (representing "non-focused proofs") between them. As a special case of (ii) above, a compact model of MLLP is also presented based on Rel_+ with multi-points.