The Many-Worlds CalculusArticle
Authors: Kostia Chardonnet ; Marc de Visme ; Benoît Valiron ; Renaud Vilmart
NULL##NULL##NULL##NULL
Kostia Chardonnet;Marc de Visme;Benoît Valiron;Renaud Vilmart
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.
Volume: Volume 21, Issue 2
Published on: May 16, 2025
Accepted on: March 7, 2025
Submitted on: December 1, 2023
Keywords: Computer Science - Logic in Computer Science, Quantum Physics
Funding:
Source : OpenAIRE Graph- Funder: French National Research Agency (ANR); Code: ANR-22-PNCQ-0002
- Probabilistic program semantics; Funder: French National Research Agency (ANR); Code: ANR-19-CE48-0014
- Reasoning with Circular proofs for Programming; Funder: French National Research Agency (ANR); Code: ANR-21-CE48-0019
- Reasoning with Circular proofs for Programming; Funder: French National Research Agency (ANR); Code: ANR-22-PETQ-0007
- Reasoning with Circular proofs for Programming; Funder: French National Research Agency (ANR); Code: ANR-22-PETQ-0013