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 which is at the core of the sup connective.

翻译：本文探讨了直觉主义乘加线性逻辑的一种证明语言，该语言引入了sup连接词，该连接词通过概率性消元引入加性对，并在证明项中引入和与标量积。我们给出了该语言的抽象刻画，揭示了任何具有双积且从标量半环到Hom(I,I)半环存在单态射的对称幺半闭范畴都适用于此任务。利用二元双积，我们定义了加权余对角映射，该映射是sup连接词的核心。