Denotational semantics for stabiliser quantum programs

TL;DR

This paper introduces a new denotational semantics for stabiliser quantum programs that is sound, complete, and computationally efficient, providing a foundational framework for quantum error correction and fault-tolerant quantum computing.

Contribution

It develops a novel, affine relation-based semantics for stabiliser operations, including measurement and classical control, with a proof-of-concept assembly language implementation.

Findings

Semantic model is sound, complete, and fully-abstract.

Offers a computationally tractable alternative to operator-algebraic semantics.

Demonstrates the semantics with a small stabiliser assembly language.

Abstract

The stabiliser fragment of quantum theory is a foundational building block for quantum error correction and the fault-tolerant compilation of quantum programs. In this article, we develop a sound, universal and complete denotational semantics for stabiliser operations which include measurement, classically-controlled Pauli operators, and affine classical operations, in which quantum error-correcting codes are first-class objects. The operations are interpreted as certain affine relations over finite fields. This offers a conceptually motivated and computationally-tractable alternative to the standard operator-algebraic semantics of quantum programs (whose time complexity grows exponentially as the state space increases in size). We demonstrate the power of the resulting semantics by describing a small, proof-of-concept assembly language for stabiliser programs with fully-abstract denotational semantics.