Algebraic Theories and Quantum Communication

With the advent of quantum computing and communication comes the need for corresponding programming language primitives. In this dissertation, we study a notion of classically controlled quantum communication (sending and receiving qubits) using Staton’s language of parameterised algebraic theories (PAT) (Staton 2015). More specifically, we start by showing the well-formedness of the standard combinations of algebraic theories (sums and tensors) for PATs. Then, we define a PAT for quantum communication, \(\mathsf{I/O}\otimes \mathsf{Quantum}\), as the tensor of a standard I/O theory and Staton’s complete axiomatisation for qubit quantum computing \(\mathsf{Quantum}\). Finally, we give two complementary models to this algebraic theory: one operational and one denotational. The first model is based on an operational semantics where the program sends and receives qubits to and from an environment modelled by a quantum stream. It concretely demonstrates the notion of quantum communication and ensures that our theory is non-degenerate (unlike the Eckmann-Hilton setting). The second model is based on an elegant denotational semantics, constructed as a free I/O monad on \(\mathbf{CP}^{\infty}\), the category of matrix algebras and CP maps completed with infinite biproducts (Pagani, Selinger, Valiron 2013). We show that these two models correspond to the same notion of communication in the sense that the denotational model is adequate and fully abstract with respect to the operational model.

[PDF]Thesis