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.

翻译：量子理论中的稳定子片段是量子纠错与量子程序容错编译的基础构建模块。本文为稳定子操作开发了一套可靠、通用且完备的指称语义，这些操作包括测量、经典受控泡利算符以及仿射经典操作，其中量子纠错码被视作一等对象。这些操作被解释为有限域上的特定仿射关系。这为量子程序的标准算子代数语义（其时间复杂度随状态空间规模增大呈指数级增长）提供了概念清晰且计算易处理的替代方案。我们通过设计一种具有完全抽象指称语义的小型概念验证稳定子程序汇编语言，展示了该语义体系的强大表达能力。