The Many-Worlds Calculus
Kostia Chardonnet, Marc de Visme, Benoît Valiron, Renaud Vilmart
TL;DR
The paper addresses unifying tensor-based pairing and coproduct-based branching, including quantum and indefinite causal-order branching, by introducing the Many-Worlds Calculus. It builds three colored PROPs with world labeling, defines world-dependent and world-agnostic denotational semantics into finite dimensional $R$-semimodules, and develops a complete equational theory with a unique normal form. This framework universalizes to express any linear operator within the modeled spaces and can encode quantum control phenomena such as the Quantum Switch, while enabling direct comparisons and encodings from ZX-calculus, Tensor-Sum Logic, PBS-Calculus, and routed circuits. The approach yields a robust, compositional basis for reasoning about complex branching and quantum control, with potential applications in quantum programming and formal reasoning about mixed tensor/coproduct structures.
Abstract
In this paper, we explore the interaction between two monoidal structures: a multiplicative one, for the encoding of pairing, and an additive one, for the encoding of choice. We propose a colored PROP to model computation in this framework, where the choice is parameterized by an algebraic side effect: the model can support regular tests, probabilistic and non-deterministic branching, as well as quantum branching, i.e. superposition. The graphical language comes equipped with a denotational semantics based on linear applications, and an equational theory. We prove the language to be universal, and the equational theory to be complete with respect to this semantics.