计算机应用

作者：陶文萱, 陈钢

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

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

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

来源：2024年第10期

《计算机应用》期刊编辑部

查看计算机应用杂志2024年第10期