A General Probabilistic Framework in IMALL: A Concrete Categorical Perspective
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.
Keywords
Cite
@article{arxiv.2309.04624,
title = {A General Probabilistic Framework in IMALL: A Concrete Categorical Perspective},
author = {Alejandro Díaz-Caro and Octavio Malherbe},
journal= {arXiv preprint arXiv:2309.04624},
year = {2024}
}
Comments
There is a mistake in the adequacy proof for the first language. The other languages have been integrated into arXiv:2205.02142, making this paper merely a concrete example