Hadamard-Pi: Equational Quantum Programming

TL;DR

This paper introduces a quantum programming language extending classical reversible programming with the Hadamard gate, providing a complete categorical semantics and a synthesis algorithm for related orthogonal matrices.

Contribution

It presents a new quantum programming language with a sound and complete equational semantics, and a finite presentation and synthesis algorithm for specific orthogonal matrix groups.

Findings

Complete categorical semantics for the language.

Finite presentation of the orthogonal matrix groups.

A synthesis algorithm for these matrices.

Abstract

Quantum computing offers advantages over classical computation, yet the precise features that set the two apart remain unclear. In the standard quantum circuit model, adding a 1-qubit basis-changing gate -- commonly chosen to be the Hadamard gate -- to a universal set of classical reversible gates yields computationally universal quantum computation. However, the computational behaviours enabled by this addition are not fully characterised. We give such a characterisation by introducing a small quantum programming language extending the universal classical reversible programming language $\Pi$ with a single primitive corresponding to the Hadamard gate. The language comes equipped with a sound and complete categorical semantics that is specified by a purely equational theory. Completeness is shown by means of a novel finite presentation, and a corresponding synthesis algorithm, for the groups of orthogonal matrices with entries in the ring $\mathbb{Z}[\tfrac{1}{\sqrt{2}}]$.