On geometry of interaction for polarized linear logic
From MaRDI portal
Abstract: We present Geometry of Interaction (GoI) models for Multiplicative Polarized Linear Logic, MLLP, which is the multiplicative fragment 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. For example, they permit us to characterize the key feature of polarization, focusing, as well as being fundamental to our construction of concrete polarized GoI models. Our approach to polarized GoI involves two independent studies, based on different categorical perspectives of GoI. (i) Inspired by the work of Abramsky, Haghverdi, and Scott, a polarized GoI situation is defined in which multipoints are added to a traced monoidal category equipped with a reflexive object . Using this framework, categorical versions of Girard's Execution formula are defined, as well as the GoI interpretation of MLLP, proofs. Running the Execution formula is shown to characterize the focusing property (and thus polarities) as well as the dynamics of cut-elimination. (ii) The Int construction of Joyal-Street-Verity is another fundamental categorical structure for modelling GoI. Here, we investigate it in a multipointed setting. Our presentation yields a compact version of Hamano-Scott's polarized categories, and thus denotational models of MLLP. These arise from a contravariant duality between monoidal categories of positive and negative objects, along with an appropriate bimodule structure (representing "non-focused proofs") between them. Finally, as a special case of (ii) above, a compact model of MLLP is also presented based on Rel (the category of sets and relations) equipped with multi-points.
Recommendations
Cites work
- A categorical model for the geometry of interaction
- A categorical semantics for polarized MALL
- A multi-focused proof system isomorphic to expansion proofs
- A new constructive logic: classic logic
- A phase semantics for polarized linear logic and second order conservativity
- Focusing and polarization in linear, intuitionistic, and classical logics
- Focusing Strategies in the Sequent Calculus of Synthetic Connectives
- Focussing and proof construction
- Glueing and orthogonality for models of linear logic
- scientific article; zbMATH DE number 5080676 (Why is no real title available?)
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 3967883 (Why is no real title available?)
- scientific article; zbMATH DE number 4123722 (Why is no real title available?)
- scientific article; zbMATH DE number 1342251 (Why is no real title available?)
- scientific article; zbMATH DE number 786500 (Why is no real title available?)
- scientific article; zbMATH DE number 3367095 (Why is no real title available?)
- Linear logic
- Locus solum: From the rules of logic to the logic of rules.
- Logic Programming with Focusing Proofs in Linear Logic
- Polarized category theory, modules, and game semantics
- The blind spot. Lectures on logic
- The Scott model of linear logic is the extensional collapse of its relational model
- The uniformity principle on traced monoidal categories
- Towards a typed geometry of interaction
- Traced monoidal categories
Cited in
(7)- Geometry of interaction and the dynamics of proof reduction: a tutorial
- Polarized category theory, modules, and game semantics
- An Indexed System for Multiplicative Additive Polarized Linear Logic
- Geometry of interaction for MALL via Hughes-Van Glabbeek proof-nets
- Automata, Languages and Programming
- A categorical model for the geometry of interaction
- A categorical semantics for polarized MALL
This page was built for publication: On geometry of interaction for polarized linear logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4961719)
