Abstract:

All quantum gates， states and measurement operators in qubit systems can be represented as power-of-two matrices. However， existing quantum programming frameworks have not taken it into account. Therefore， a power-of-two matrix type system was proposed， and a corresponding quantum intermediate representation was designed. Firstly， the power-of-two matrix system was implemented using recursive dual structure in the theorem prover Coq. It accurately described quantum gates， states and measurement operators. Then， a quantum intermediate representation was designed as a programming tool， capable of automatically translating quantum programs into power-of-two matrix expressions. Finally， the writing and translation process of the quantum Fourier transform was demonstrated. The power-of-two matrix system provides a more accurate and concise type system for quantum programming frameworks. The quantum intermediate representation facilitates a transition from power-of-two matrices to programming languages， serving as an effective means to write quantum programs in the power-of-two matrix system.

Key words: quantum computing, type system, quantum intermediate representation, theorem prover, Coq

摘要：

在两能级量子计算系统中，所有量子门、量子态和测量算子都可以表示为2的幂次方阶矩阵（简称二幂阶矩阵）的形式，而现有量子编程语言未考虑该特性。因此，提出一种二幂阶矩阵类型系统，并设计相应的量子中间表示。首先，在定理证明器Coq中利用递归对偶结构实现二幂阶矩阵系统，可以精确描述量子门、量子态和测量算子；其次，设计一套量子中间表示作为编程工具，可以自动将量子程序翻译为二幂阶矩阵表达式；最后，展示量子傅里叶变换的编写和翻译过程。二幂阶矩阵系统为基于定理证明器的量子编程语言提供了更精确、更简洁的类型系统，量子中间表示实现了从二幂阶矩阵到程序语言的过渡，提供了在二幂阶矩阵系统中编写量子程序的有效手段。

关键词: 量子计算, 类型系统, 量子中间表示, 定理证明器, Coq