The Sup Connective in IMALL: A Categorical Semantics

TL;DR

This paper introduces a proof language for a form of linear logic that includes a novel sup connective, characterized categorically, with potential applications in probabilistic reasoning.

Contribution

It provides an abstract categorical framework for a proof language with a new sup connective in intuitionistic linear logic.

Findings

Categorical characterization of the proof language.

Definition of a weighted codiagonal map for the sup connective.

Suitability of symmetric monoidal closed categories with biproducts for the language.

Abstract

We explore a proof language for intuitionistic multiplicative additive linear logic, incorporating the sup connective that introduces additive pairs with a probabilistic elimination, and sum and scalar products within the proof-terms. We provide an abstract characterisation of the language, revealing that any symmetric monoidal closed category with biproducts and a monomorphism from the semiring of scalars to the semiring Hom(I,I) is suitable for the job. Leveraging the binary biproducts, we define a weighted codiagonal map which is at the core of the sup connective.