Denotational semantics for stabiliser quantum programs

TL;DR

This work delivers a denotational semantics framework for stabiliser quantum programs by leveraging a symplectic, affine-relational representation, enabling efficient reasoning about stabiliser maps, measurements, and classical control. By embedding mixed stabiliser dynamics through the CPM construction and affine coisotropic relations, it connects stabiliser codes, encoding, error detection and coarse-graining to a compositional, tractable algebraic setting. The authors introduce SPL, a small imperative language with fully abstract semantics in the Rel-based category, and extend it to arbitrary classical operations, illustrating practical verification potential and paving the way for fault-tolerant compilation pipelines. The approach provides polynomial-time observational equivalence in the symplectic setting and offers a modular path toward higher-level languages and diagrammatic formalisms (e.g., ZX-calculus) for stabiliser QEC.

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.

Figures (5)

• Figure 1: Formation rules for $\mathrm{SPL}$. New variables are always assumed to be fresh. $n\in \mathbb{N} ^{>0}$, $\tau\in \mathsf{Ty}$, and $\underline{\hbox{\normalfont\upshape x}}:\tau^n$ is shorthand for $\{ \underline{\hbox{\normalfont\upshape x1}}:\tau,\cdots, \underline{\hbox{\normalfont\upshape xn}}:\tau\}$ such that $\underline{\hbox{\normalfont\upshape x}} = ( \underline{\hbox{\normalfont\upshape x1}},\cdots, \underline{\hbox{\normalfont\upshape xn}}) \in \mathsf{Reg}\xspace^n$.
• Figure 2: Qupit teleportation in $\mathrm{SPL}$. Where $F$ is the Fourier transform; $C^X$ is the (coherently) controlled $X$ gate; and $Z$ and $X$ are the Pauli $Z$ and $X$ gates. Input is given on register $\underline{\hbox{\normalfont\upshape in}} : \mathbf{\mathtt{qpit}}$ and output is returned on register $\underline{\hbox{\normalfont\upshape out}} : \mathbf{\mathtt{qpit}}$.
• Figure 3: Denotations of the atomic terms of $\mathrm{SPL}$ in $\mathsf{QuantChan}$. Where $\iota:\mathsf{Stab}_p\to \mathsf{QuantChan}$ embeds pure stabiliser maps into stabiliser channels. $\mathcal{E}_Z:(\mathcal{H}_p,1_{\mathcal{H}_p})\to(\mathcal{H}_p,\mathcal{E}_Z)$ is Pauli-$Z$ measurement. $\Tr_{\mathcal{H}_p}:(\mathcal{H}_p,\mathcal{E}_Z)\to I$ is trace. $\mathcal{A}^{M}=\sum_{\vb{x}\in \mathbb{F}_p ^{m}}\dyad{M(\vb{x})}{\vb{x}}:(\mathcal{H}_p,\mathcal{E}_Z)^{\otimes m}\to(\mathcal{H}_p,\mathcal{E}_Z)^{\otimes n}$ is the classical channel for an $\mathbb{F} _p$-affine map $M: \mathbb{F} _p^{m}\to \mathbb{F} _p^{n}$. $C_P:(\mathcal{H}_p,\mathcal{E}_Z)\otimes(\mathcal{H}_p,1_{\mathcal{H}_p})\to(\mathcal{H}_p,\mathcal{E}_Z)\otimes(\mathcal{H}_p,1_{\mathcal{H}_p})$ is classically controlled Pauli for $P\in\mathcal{P}_p$.
• Figure 4: Small-step operational semantics of $\mathrm{SPL}$, where $a$ is an atomic term and $c,c'$ are well-formed terms. The interpretation of atomic terms $a$ in $\mathsf{QuantChan}$, denoted $\bigl\langle a\bigr\rangle_{\Delta}^{\Gamma}:\langle \Gamma\rangle\to\langle \Delta\rangle$ is defined in figure \ref{['fig:aden-generators']}.
• Figure 5: Denotation of $\mathrm{SPL}$ terms into $\mathop{\mathrm{Total}}\nolimits( { \mathsf{Aff} } \mathsf{Rel}_{ \mathbb{F} _p} ^Q)$, where typed environments omitted for brevity. $U=\pi(p_a,p_x,p_z)\in\mathcal{P}_p$ is a Pauli operator, $A: \mathbb{F}_p ^{m}\to \mathbb{F}_p ^n$ is an $\mathbb{F}_p$-affine transformation. For the sake of exposition we give the explicit interpretation for a generating set of the Clifford group: where $X$ is the Pauli $X$ gate, $C^X$ is the (quantum) controlled-$X$ gate, $F$ is the Fourier transform, $P$ is the quadratic phase gate.

Theorems & Definitions (72)

• Definition 1
• Example 2
• Example 3
• Example 4
• Example 5
• Lemma 6
• Lemma 7
• Definition 8
• Definition 9
• Example 10