The Sup Connective in IMALL: A Categorical Semantics
Alejandro Díaz-Caro and Octavio Malherbe
我们探索了直觉乘法加线性逻辑的证明语言,结合了引入加法对具有概率消除的sup连接,以及校内的总和和标量产品。 我们提供了一个语言的抽象特征,揭示了任何对称的单向封闭类别与双产品和一个单态从标量半环到半环Hom(I,I)是适合这项工作。 利用二进制双产品,我们在sup connective的核心定义一个加权的对角线图。
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 def...