The Tensor-Plus Calculus

TL;DR

The paper introduces a graphical language with dual monoidal structures for modeling various computational paradigms, providing a categorical semantics and an equational theory that is both sound and complete.

Contribution

It develops a universal graphical language with a semiring-based semantics for semiadditive categories, unifying different computational models.

Findings

Provides a categorical semantics for the graphical language.

Establishes soundness and completeness of the equational theory.

Demonstrates the language's universality for modeling various computations.

Abstract

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.