Free Quantum Computing

TL;DR

An axiomatization of quantum computing that replaces the standard continuous postulates with a small number of discrete equations, as well as a free model that replaces the standard linear-algebraic model with a category-theoretical one.

Abstract

Quantum computing improves substantially on known classical algorithms for various important problems, but the nature of the relationship between quantum and classical computing is not yet fully understood. This relationship can be clarified by free models, that add to classical computing just enough physical principles to represent quantum computing and no more. Here we develop an axiomatisation of quantum computing that replaces the standard continuous postulates with a small number of discrete equations, as well as a free model that replaces the standard linear-algebraic model with a category-theoretical one. The axioms and model are based on reversible classical computing, isolate quantum advantage in the ability to take certain well-behaved square roots, and link to various quantum computing hardware platforms. This approach allows combinatorial optimisation, including brute force computer search, to optimise quantum computations. The free model may be interpreted as a programming language for quantum computers, that has the same expressivity and computational universality as the standard model, but additionally allows automated verification and reasoning.

Figures (3)

• Figure 1: The defining property of a free model: it realises our axioms of quantum computation, and there is a unique interpretation of the free model in any other model satisfying our axioms. In this sense, the free model contains exactly what is needed to form a model, and nothing more.
• Figure 2: The landscape of models of quantum computing and their relations. Solid arrows indicate inclusion of one model into another. Incomparable models are connected with dotted lines. For each $k$, $\Pi_k$ is the free model for the axioms of bipermutative categories augmented with axioms $\left(\ref{['eq:axiom1']}\right)$--$\left(\ref{['eq:axiom3']}\right)$. The standard model of unitaries over the complex numbers also satisfies these axioms. For each $k$, $\Pi_k$ embeds in any model that also satisfies the same axioms. For another example, the model of Clifford+$\sqrt[3]{T}$ circuits is also computationally universal nebe_invariants_2001 but incomparable to any $\Pi_k$.
• Figure 3: An illustration of Axiom $\left(\ref{['eq:axiom2']}\right)$, interpreting $V$ as swapping the leftmost two wires, and $S$ as swapping the rightmost two wires.

Theorems & Definitions (59)

• Theorem 1
• Theorem 2
• proof : Proof sketch
• Theorem 3
• proof : Proof sketch
• Theorem 4
• proof : Proof sketch
• Theorem 5
• proof : Proof sketch
• Definition 6