We propose a graphical language that accommodates two monoidal structures: a multiplicative one for pairing and an additional one for branching. In this colored PROP, whether wires in parallel are linked through the multiplicative structure or the additive structure is implicit and determined contextually rather than explicitly through tapes, world annotations, or other techniques, as is usually the case in the literature. The diagrams are used as parameter elements of a commutative semiring, whose choice is determined by the kind of computation we want to model, such as non-deterministic, probabilistic, or quantum. Given such a semiring, we provide a categorical semantics of diagrams and show the language as universal for it. We also provide an equational theory to identify diagrams that share the same semantics and show that the theory is sound and complete and captures semantical equivalence. In categorical terms, we design an internal language for semiadditive categories (C,+,0) with a symmetric monoidal structure (C,x,1) distributive over it, and such that the homset C(1,1) is isomorphic to a given commutative semiring, e.g., the semiring of non-negative real numbers for the probabilistic case.
翻译:我们提出一种图形语言,该语言容纳两种幺半结构:一种用于配对的乘法结构,以及一种用于分支的加法结构。在这个着色PROP中,并行导线是通过乘法结构还是加法结构连接是隐含的,并由上下文决定,而不是像文献中通常那样通过磁带、世界标注或其他技术显式指定。这些图被用作交换半环的参数元素,半环的选择取决于我们希望建模的计算类型,例如非确定性、概率性或量子计算。给定这样一个半环,我们为图提供范畴语义,并证明该语言对此具有普适性。我们还提供了一套等式理论来识别具有相同语义的图,并证明该理论是可靠且完备的,能够捕捉语义等价性。用范畴论的术语来说,我们为半加法范畴(C,+,0)设计了一种内部语言,该范畴具有对称幺半结构(C,x,1)且该结构对其可分配,并且使得同态集C(1,1)同构于给定的交换半环,例如在概率情形下同构于非负实数半环。