Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Sup Connective in IMALL: A Categorical Semantics

Alejandro Díaz-Caro, Octavio Malherbe

TL;DR

This work develops a categorical semantics for an IMALL-inspired language extended with the sup connective, capturing probabilistic and additive behavior via a weighted codiagonal in categories with biproducts. It shows that any symmetric monoidal closed category with biproducts and a monomorphism from a scalar semiring into End(I) suffices to interpret the language, providing both soundness and adequacy results. By internalizing probabilistic choice and vector/matrix structures through sums and scalar products in the syntax, the paper unifies probabilistic reasoning with linear logic connectives and offers a groundwork for further links to quantum computing and probabilistic programming. The categorical construction, including the map scalars, weighted codiagonal, and the delta map, provides a flexible, abstract model that extends prior PCF^R-like approaches while enabling richer connectives. This framework paves the way for applying IMALL+sup to verifiable quantum algorithms and probabilistic languages, with clear semantics grounded in biproducts and monoidal structure.

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 at the heart of the sup connective.

The Sup Connective in IMALL: A Categorical Semantics

TL;DR

This work develops a categorical semantics for an IMALL-inspired language extended with the sup connective, capturing probabilistic and additive behavior via a weighted codiagonal in categories with biproducts. It shows that any symmetric monoidal closed category with biproducts and a monomorphism from a scalar semiring into End(I) suffices to interpret the language, providing both soundness and adequacy results. By internalizing probabilistic choice and vector/matrix structures through sums and scalar products in the syntax, the paper unifies probabilistic reasoning with linear logic connectives and offers a groundwork for further links to quantum computing and probabilistic programming. The categorical construction, including the map scalars, weighted codiagonal, and the delta map, provides a flexible, abstract model that extends prior PCF^R-like approaches while enabling richer connectives. This framework paves the way for applying IMALL+sup to verifiable quantum algorithms and probabilistic languages, with clear semantics grounded in biproducts and monoidal structure.

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 at the heart of the sup connective.
Paper Structure (40 sections, 33 theorems, 71 equations, 3 figures)

This paper contains 40 sections, 33 theorems, 71 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Historical origins
  3. Modelling the sup connective
  4. Related works
  5. Compact closed categories
  6. Probabilistic coherence spaces
  7. Cones
  8. PCF$^{\mathcal{R}}$
  9. Contents of the paper
  10. The L-sup-calculus
  11. Grammars
  12. Deduction rules
  13. Reduction rules
  14. Correctness
  15. Examples and applications
  16. ...and 25 more sections

Key Result

Theorem 2.7

If $\Gamma\vdash t:A$ and $t\longrightarrow_{\mathsf p} u$, then $\Gamma\vdash u:A$. ∎

Figures (3)

  • Figure 1: The deduction rules of the $\mathcal{L}\odot^{{\mathcal{S}}\mathsf p}$-calculus.
  • Figure 2: The beta group of reduction rules of the $\mathcal{L}\odot^{{\mathcal{S}}\mathsf p}$-calculus.
  • Figure 3: The commutation group of reduction rules of the $\mathcal{L}\odot^{{\mathcal{S}}\mathsf p}$-calculus.

Theorems & Definitions (98)

  • Definition 2.1: Propositions of the $\mathcal{L}\odot^{\mathcal{S}\mathsf p}$-logic
  • Remark 2.2
  • Definition 2.3: Proof-terms of the $\mathcal{L}\odot^{{\mathcal{S}}\mathsf p}$-calculus
  • Definition 2.4: Proof-term context
  • Remark 2.5
  • Remark 2.6
  • Theorem 2.7: Subject reduction DiazcaroDowekMSCS24
  • Theorem 2.8: Confluence DiazcaroDowekMSCS24
  • Theorem 2.9: Strong normalisation DiazcaroDowekMSCS24
  • Theorem 2.10: Introduction DiazcaroDowekMSCS24
  • ...and 88 more