A General Probabilistic Framework in IMALL: A Concrete Categorical Perspective

TL;DR

This paper introduces a categorical framework for probabilistic and non-deterministic constructs in linear logic, using semimodules over semirings, providing an alternative to traditional monad-based models.

Contribution

It develops a novel categorical model for the sup type constructor in linear logic, applicable to quantum computing and non-determinism, using weighted codiagonals in semimodule categories.

Findings

Models non-determinism with weighted codiagonals

Provides an alternative to Moggi's Powerset Monad in semimodule categories

Validates the approach with categories having biproducts

Abstract

We consider the linear lambda-calculus extended with the sup type constructor, which provides an additive conjunction along with a non-deterministic destructor. The sup type constructor has been introduced in the context of quantum computing. In this paper, we study this type constructor within a simple linear logic categorical model, employing the category of semimodules over a commutative semiring. We demonstrate that the non-deterministic destructor, either weighted or not, finds a suitable model in a weighted codiagonal map. Our approach offers a valid and insightful alternative to interpreting non-determinism and probability calculi, in instances where the conventional Moggi's Powerset Monad interpretation does not align with the category's structure, as is the case with the category of semimodules. The validity of this alternative relies on the presence of biproducts within the category.