2022/05/04 by Díaz-Caro, Alejandro, Malherbe, Octavio · 1 citation
#18M45 03F52 03B70 #Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2205.02142
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 at the heart of the sup connective.