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 finds a suitable model in a "weighted" codiagonal map. This approach offers a valid and insightful alternative to interpreting non-determinism, especially in instances where the conventional 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.

翻译：本文考虑扩展了超类型构造子的线性λ演算，该构造子提供了加法合取而同时伴随非确定性消解子。超类型构造子最初在量子计算背景下被引入。我们在一个基于交换半环上半模范畴的简单线性逻辑范畴模型中研究该类型构造子。研究表明，非确定性消解子可在"加权"余对角映射中找到合适的模型。该方案为解释非确定性提供了有效且富有洞见的替代途径，尤其适用于传统幂集单子解释与范畴结构不兼容的情形（如半模范畴）。该替代方案的有效性依赖于范畴中双积结构的存在性。