基于二幂阶矩阵的量子中间表示与翻译  

Quantum intermediate representation and translation based on power-of-two matrix

作　　者：陶文萱 陈钢 TAO Wenxuan;CHEN Gang(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing Jiangsu 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106

出　　处：《计算机应用》2024年第10期3141-3150,共10页journal of Computer Applications

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

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]