The Sup Connective in IMALL: A Categorical Semantics
This work addresses a foundational issue in proof theory and categorical semantics for logicians and theoretical computer scientists, but it appears incremental as it builds on existing frameworks.
The paper tackles the problem of developing a proof language for intuitionistic multiplicative additive linear logic by incorporating a sup connective with probabilistic elimination, and it results in an abstract characterization showing that any symmetric monoidal closed category with biproducts and a specific monomorphism suffices for this purpose.
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.