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

doi:10.11772/j.issn.1001-9081.2023091358

《计算机应用》唯一官方网站 ›› 2024, Vol. 44 ›› Issue (10): 3141-3150.DOI: 10.11772/j.issn.1001-9081.2023091358

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

陶文萱, 陈钢()

南京航空航天大学计算机科学与技术学院，南京 211106

收稿日期:2023-10-07 修回日期:2024-01-16 接受日期:2024-01-18 发布日期:2024-03-08 出版日期:2024-10-10
通讯作者: 陈钢
作者简介:陶文萱（1998—），女，江苏南京人，硕士研究生，CCF会员，主要研究方向：形式化方法、量子计算、量子程序验证
陈钢（1958—），男，上海人，教授，博士，CCF杰出会员，主要研究方向：形式化方法、程序语言设计、类型系统、基础软件 gangchensh@nuaa.edu.cn。

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

Wenxuan TAO, Gang CHEN()

College of Computer Science and Technology，Nanjing University of Aeronautics and Astronautics，Nanjing Jiangsu 211106，China

Received:2023-10-07 Revised:2024-01-16 Accepted:2024-01-18 Online:2024-03-08 Published:2024-10-10
Contact: Gang CHEN
About author:TAO Wenxuan， born in 1998， M. S. candidate. Her research interests include formal method， quantum computing， quantum program verification.

摘要/Abstract

摘要：

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

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

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

中图分类号:

TP311

陶文萱, 陈钢. 基于二幂阶矩阵的量子中间表示与翻译[J]. 计算机应用, 2024, 44(10): 3141-3150.

Wenxuan TAO, Gang CHEN. Quantum intermediate representation and translation based on power-of-two matrix[J]. Journal of Computer Applications, 2024, 44(10): 3141-3150.

图/表 6

表1 常用Dirac符号

Tab. 1 Common Dirac notations

符号	释义
$φ$	右矢，表示一个列向量
$φ 1 φ 2$	$φ 1$ 和 $φ 2$ 的Kronecker积，表示一个列向量
$φ 1 φ 2$	$φ 1$ 和 $φ 2$ 的外积，表示一个矩阵

表1 常用Dirac符号

Tab. 1 Common Dirac notations

符号	释义
$φ$	右矢，表示一个列向量
$φ 1 φ 2$	$φ 1$ 和 $φ 2$ 的Kronecker积，表示一个列向量
$φ 1 φ 2$	$φ 1$ 和 $φ 2$ 的外积，表示一个矩阵

表2 PMatrix矩阵运算函数的信息

Tab. 2 Information of PMatrix matrix operation functions

名称	功能
PMzero	二幂阶全零矩阵
PMid	二幂阶单位矩阵
PMeqb	判断2个二幂阶矩阵是否等价
PMplus	二幂阶矩阵的加法运算
PMopp	二幂阶矩阵的元素取反运算
PMminus	二幂阶矩阵的减法运算
PMmult	二幂阶矩阵的乘法运算
PMscale	复数与二幂阶矩阵的数乘运算
PMkron	二幂阶矩阵的Kronecker积运算
PMkron_n	二阶矩阵自身的若干次Kronecker积运算
PMconj	二幂阶矩阵的共轭运算
PMtrans	二幂阶矩阵的转置运算
PMadjoint	二幂阶矩阵的共轭转置运算
PMunitary	二幂阶酉矩阵命题

表3 PMatrix与QuantumLib运算时长比较

Tab. 3 Comparison of computation time between PMatrix and QuantumLib

自乘次数	运算时长/s
自乘次数	PMatrix	QuantumLib
1	0.002	0.004
2	0.005	0.011
3	0.014	0.062
4	0.044	0.269
5	0.180	1.340
6	0.828	6.417
7	4.149	27.969
8	17.141	—

表4 单量子比特门命令

Tab. 4 Single-qubit gate commands

名称	U 门形式	PQIR命令（i指明作用位）
I 门	$U 0,0, 0$	I i
X 门	$U π, 0, π$	X i
Y 门	$U π, π / 2, π / 2$	Y i
Z 门	$U 0,0, π$	Z i
H 门	$U π / 2,0, π$	H i
S 门	$U 0,0, π / 2$	S i
T 门	$U 0,0, π / 4$	T i
RX （θ）门	$U θ, - π / 2, π / 2$	RX θ i
RY （θ）门	$U θ, 0,0$	RY θi
RZ （λ）门	$U 0,0, λ$	RZ λi

表4 单量子比特门命令

Tab. 4 Single-qubit gate commands

名称	U 门形式	PQIR命令（i指明作用位）
I 门	$U 0,0, 0$	I i
X 门	$U π, 0, π$	X i
Y 门	$U π, π / 2, π / 2$	Y i
Z 门	$U 0,0, π$	Z i
H 门	$U π / 2,0, π$	H i
S 门	$U 0,0, π / 2$	S i
T 门	$U 0,0, π / 4$	T i
RX （θ）门	$U θ, - π / 2, π / 2$	RX θ i
RY （θ）门	$U θ, 0,0$	RY θi
RZ （λ）门	$U 0,0, λ$	RZ λi

图1 3量子比特傅里叶变换线路

Fig. 1 QFT circuit on 3 qubits

图2 受控U门分解线路

Fig. 2 Circuit of controlled-U gate

参考文献 45

1	DEUTSCH D， JOZSA R. Rapid solution of problems by quantum computation ［J］. Proceedings of the Royal Society A： Mathematical， Physical and Engineering Sciences， 1992， 439（1907）： 553-558.
2	EGGER D J， GUTIÉRREZ R G， MESTRE J C， et al. Credit risk analysis using quantum computers ［J］. IEEE Transactions on Computers， 2021， 70（12）： 2136-2145.
3	PIRANDOLA S， ANDERSEN U L， BANCHI L， et al. Advances in quantum cryptography ［J］. Advances in Optics and Photonics， 2020， 12（4）： 1012-1236.
4	KANDALA A， MEZZACAPO A， TEMME K， et al. Hardware-efficient variational quantum eigensolver for small molecules and quantum magnets ［J］. Nature， 2017， 549： 242-246.
5	SVORE K， GELLER A， TROYER M， et al. Q# ： enabling scalable quantum computing and development with a high-level DSL［C］// Proceedings of the Real World Domain Specific Languages Workshop 2018. New York： ACM， 2018： 1-10.
6	ALEKSANDROWICZ G， ALEXANDER T， BARKOUTSOS P， et al. Qiskit： an open-source framework for quantum computing （0.7.2）［DS/OL］. ［2023-09-27］. .
7	GREEN A S， LUMSDAINE P L F， ROSS N J， et al. Quipper： a scalable quantum programming language ［J］. ACM SIGPLAN Notices， 2013， 48（6）： 333-342.
8	MindSpore Quantum Developers. MindSpore Quantum （0.8.0）［DS/OL］. （2023-02-13）［2023-09-27］. .
9	DOU M， ZOU T， FANG Y， et al. QPanda： high-performance quantum computing framework for multiple application scenarios ［EB/OL］. （2022-12-29）［2023-05-27］. .
10	CHARETON C， BARDIN S， LEE D， et al. Formal methods for quantum programs： a survey ［EB/OL］. （2021-09-14）［2024-01-03］. .
11	LEWIS M， SOUDJANI S， ZULIANI P. Formal verification of quantum programs： theory， tools， and challenges ［J］. ACM Transactions on Quantum Computing， 2023， 5（1）： 1-35.
12	HIETALA K， RAND R， S-H HUNG， et al. Proving quantum programs correct ［EB/OL］. （2021-07-13）［2023-09-27］. .
13	PAYKIN J， RAND R， ZDANCEWIC S. QWIRE： a core language for quantum circuits ［C］// Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. New York： ACM， 2017： 846-858.
14	ZHOU L， BARTHE G， P-Y STRUB， et al. CoqQ： foundational verification of quantum programs ［J］. Proceedings of the ACM on Programming Languages， 2023， 7（POPL）： 833-865.
15	LIU J， ZHAN B， WANG S， et al. Formal verification of quantum algorithms using quantum Hoare logic ［C］// Proceedings of the 31st International Conference on Computer Aided Verification. Cham： Springer， 2019： 187-207.
16	CHARETON C， BARDIN S， BOBOT F， et al. An automated deductive verification framework for circuit-building quantum programs ［C］// Proceedings of the 30th European Symposium on Programming： Programming Languages and Systems. Cham： Springer， 2021： 148-177.
17	BORDG A， LACHNITT H， HE Y. Certified quantum computation in Isabelle/HOL ［J］. Journal of Automated Reasoning， 2021， 65（5）： 691-709.
18	HIETALA K， RAND R， S-H HUNG， et al. A verified optimizer for quantum circuits ［J］. Proceedings of the ACM on Programming Languages， 2021， 5（POPL）： Article No. 37.
19	LEHMANN A， CALDWELL B， RAND R. VyZX： a vision for verifying the ZX Calculus ［EB/OL］. （2022-05-11）［2024-01-03］. .
20	NIELSEN M A， CHUANG I L. Quantum Computation and Quantum Information： 10th Anniversary Edition ［M］. Cambridge： Cambridge University Press， 2010： 80-97.
21	南京航空航天大学. 一种应用于量子计算的特殊矩阵和向量的形式化方法： CN202310648914.8 ［P］. 2023-06-02.
	Nanjing University of Aeronautics and Astronautics. A formal method for special matrices and vectors with applications to quantum computing： CN202310648914.8 ［P］. 2023-06-02.
22	Developers Coq. Coq manual（8.18.0）［DS/OL］. ［2024-01-03］ .
23	NIPKOW T， WENZEL M， PAULSON L C. Isabelle/HOL： A Proof Assistant for Higher-Order Logic ［M］. Berlin： Springer， 2002： 9-63.
24	J-C FILLIÂTRE， PASKEVICH A. Why3： where programs meet provers ［C］// Proceedings of the 22nd European Symposium on Programming： Programming Languages and Systems. Cham： Springer， 2013： 125-128.
25	RAND R. Formally verified quantum programming ［D］. Philadelphia： University of Pennsylvania， 2018： 80-85.
26	KAYE P， LAFLAMME R， MOSCA M. An Introduction to Quantum Computing ［M］. New York： Oxford University Press， 2016： 80-82.
27	DEUTSCH D. Quantum theory， the Church-Turing principle and the universal quantum computer ［J］. Proceedings of the Royal Society A： Mathematical， Physical and Engineering Sciences， 1985， 400（1818）： 97-117.
28	YING M. Floyd-Hoare logic for quantum programs ［J］. ACM Transactions on Programming Languages and Systems， 2012， 33（6）： Article No. 19.
29	GROVER L K. A fast quantum mechanical algorithm for database search ［C］// Proceedings of the 28th Annual ACM Symposium on Theory of Computing. New York： ACM， 1996： 212-219.
30	MAHBOUBI A， TASSI E. Mathematical Components （1.0.2）［DS/OL］. （2022-09-28）［2023-06-04］. .
31	LOMONT C. The hidden subgroup problem： review and open problems ［EB/OL］. （2004-11-05）［2024-01-03］. .
32	HARROW A W， HASSIDIM A， LLOYD S. Quantum algorithm for linear systems of equations ［J］. Physical Review Letters， 2009， 103（15）： 150502.
33	INQWIRE Developers. INQWIRE QuantumLib（1.1.0）［DS/OL］. （2022-08-01）［2023-08-12］. .
34	SHI Z P， XIE G J， CHEN G. CoqMatrix： formal matrix library with multiple models in Coq ［J］. Journal of Systems Architecture， 2023， 143： 102986.
35	BOLDO S， LELAY C， MELQUIOND G. Coquelicot： a user-friendly library of real analysis for Coq ［J］. Mathematics in Computer Science， 2015， 9： 41-62.
36	BLANQUI F， KOPROWSKI A. CoLoR： a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ［J］. Mathematical Structures in Computer Science， 2011， 21（4）： 827-859.
37	马振威，陈钢.基于Coq记录的矩阵形式化方法［J］.计算机科学，2019，46（7）：139-145.
	MA Z W， CHEN G. Matrix formalization based on Coq record ［J］. Computer Science， 2019， 46（7）： 139-145.
38	麻莹莹，马振威，陈钢.基于Coq的分块矩阵运算的形式化［J］.软件学报，2021，32（6）：1882-1909.
	MA Y Y， MA Z W， CHEN G. Formalization of operations of block matrix based on Coq ［J］.Journal of Software， 2021， 32（6）： 1882-1909.
39	DIRAC P A M. A new notation for quantum mechanics ［J］. Mathematical Proceedings of the Cambridge Philosophical Society， 1939， 35（3）： 416-418.
40	NAKAHARA M， OHMI T. Quantum Computing： From Linear Algebra to Physical Realizations ［M］. Boca Raton： CRC Press， 2008： 38-39.
41	CROSS A， JAVADI-ABHARI A， ALEXANDER T， et al. OpenQASM 3： a broader and deeper quantum assembly language ［J］. ACM Transactions on Quantum Computing， 2022， 3（3）： Article No. 12.
42	LI C-K， ROBERTS R， YIN X. Decomposition of unitary matrices and quantum gates ［J］. International Journal of Quantum Information， 2013， 11（1）： 1350015.
43	CLEVE R， EKERT A， MACCHIAVELLO C， et al. Quantum algorithms revisited ［J］. Proceedings of the Royal Society A： Mathematical， Physical and Engineering Sciences， 1997， 454（1969）： 339-354.
44	BRASSARD G， HØYER P， MOSCA M， et al. Quantum amplitude amplification and estimation ［EB/OL］. （2000-05-15）［2023-11-03］. .
45	SHOR P W. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer ［J］. SIAM Journal on Computing， 1997， 26（5）： 1484-1509.

[1]	张瑜, 昌燕, 张仕斌. 基于量子局部内在维度的对抗样本检测算法[J]. 《计算机应用》唯一官方网站, 2024, 44(2): 490-495.
[2]	曹锋, 杨小玲, 易见兵, 李俊. 矛盾体分离超演绎方法及应用[J]. 《计算机应用》唯一官方网站, 2024, 44(10): 3074-3080.
[3]	赵学武刘广亮程新党冀俊忠. 基于拓扑序列和量子遗传算法的贝叶斯网结构学习[J]. 计算机应用, 2013, 33(06): 1595-1603.
[4]	易正俊何荣花侯坤. 量子位Bloch坐标的量子人工蜂群优化算法[J]. 计算机应用, 2012, 32(07): 1935-1938.
[5]	郑焕张景中. 可由用户持续发展的几何自动推理平台的推理算法[J]. 计算机应用, 2011, 31(08): 2101-2104.
[6]	付国瑜黄贤英. 基于Web页面平均质量的Web搜索模型和优化算法[J]. 计算机应用, 2009, 29(4): 1114-1116.
[7]	武妍包建军 . 一种新的求解TSP的混合量子进化算法[J]. 计算机应用, 2006, 26(10): 2433-2436.

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

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

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 6

参考文献 45

相关文章 7

编辑推荐

Metrics