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.

翻译：我们考虑了扩展了上确界类型构造子的线性λ演算，该构造子提供了一种加法合取以及一种非确定性析构子。上确界类型构造子最初在量子计算背景下被引入。本文在简单的线性逻辑范畴模型（采用交换半环上的半模范畴）中研究该类型构造子。我们证明了无论是否带权重的非确定性析构子，都可以在加权余对角映射中找到合适的模型。当传统的莫吉幂集单子解释与范畴结构（如半模范畴的情况）不相容时，我们的方法为解释非确定性和概率演算提供了有效且富有洞察力的替代方案。这一替代方案的有效性依赖于范畴中双积的存在性。