The Many-Worlds Calculus

TL;DR

This paper introduces a unified graphical calculus for modeling complex computational effects, including probabilistic, non-deterministic, and quantum branching, using a colored PROP framework with a complete equational theory.

Contribution

It develops a novel colored PROP-based graphical language that captures multiple computational effects and proves its universality and semantic completeness.

Findings

The language supports regular tests, probabilistic, non-deterministic, and quantum branching.

The graphical language is shown to be universal.

The equational theory is complete with respect to the denotational semantics.

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.