一句话：通过给经典可逆语言Π添加Hadamard原语，建立量子编程语言的可靠完备等式范畴语义，并给出正交矩阵群的有限呈现与合成算法。
标准量子线路模型中，在通用经典可逆门集上加入单 qubit 基变换门（常取 Hadamard 门）即可获得量子计算通用性，但这种扩展带来的计算行为尚未被完整刻画。本文引入一个小型量子编程语言，它在通用经典可逆语言 Π 上仅增加一个对应 Hadamard 门的原语，并给出由纯等式理论刻画的可靠且完备的范畴语义。完备性借助 Z[1/2] 上正交矩阵群的新有限呈现及相应合成算法证明；该语义为刻画这一量子扩展的计算行为提供了等式化基础。
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 Π 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 z [ 1 2 ] .
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FangHK26,
title = {Hadamard-Pi: Equational Quantum Programming},
author = {Wang Fang and Chris Heunen and Robin Kaarsgaard},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776647}
}