一句话：提出彩色 PROP 演算统一配对与选择，参数化经典、概率、非确定与量子分支，并证明通用性与等式完备性。
本文研究乘法幺半结构（用于编码配对）与加法幺半结构（用于编码选择）之间的交互，目标是在统一框架中刻画常规测试、概率与非确定性分支，以及量子分支（即叠加态）。作者提出一种彩色 PROP 作为图形化计算模型，其中选择由代数副作用参数化，因此可实例化不同分支效应。该图形语言配备基于线性映射的指称语义和等式理论。论文证明该语言具有通用性，并证明其等式理论相对于该指称语义是完备的。这为带多种选择效应的计算提供了范畴化与图形化的语义基础。
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.
@article{paperbot3418,
title = {The Many-Worlds Calculus},
author = {Kostia Chardonnet and Marc de Visme and Benoît Valiron and Renaud Vilmart},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:13)2025}
}