量子程序终止性算法分析

Yangjia Li, Mingsheng Ying (2018): Algorithmic analysis of termination problems for quantum programs. PACMPL 2(POPL), 35:1-29

背景：随着量子芯片等物理技术不断发展，量子计算机实现的相关问题已经获得了计算机科学界越来越多的研究，其中在软件理论方面，量子程序的设计、分析、验证等许多问题已经成为了前沿研究的热点，而量子程序的终止性问题则是其中的代表之一，例如：在量子Hoare逻辑中，程序的完全正确性依赖于专门的终止性证明。类似于经典程序的情形，终止性问题不仅在量子程序理论中具有重要意义，同时也是实际量子程序开发中必须考虑的关键点。

科学难题：在现有的工作中，证明程序终止性的最常用方法是生成相应的ranking function，尽管我们在之前的研究中已经对量子程序的 ranking function（QRF）进行了概念性的探讨，但是如何生成满足需要QRF依然是一个未解决的难题。另一方面，概率程序可以看成量子程序的一种退化情形，近期的研究提出了一种基于RSM（ranking super-martingale）的方法可以有效的解决概率程序的终止性问题，但是由于量子线性叠加（quantum superposition）特性，这一方法并不能直接的推广到量子程序的情形，故而需要进一步深入研究。

重要突破：我们将上鞅（super-martingale）这一数学概念应用到了量子程序的情形，提出了量子程序的 LRSM（linear ranking super-martingale）用于分析其终止性。我们证明了量子程序的终止性问题可以完全转化为LRSM的存在性问题。进一步，通过应用Gleason定理以及推广形式的Farkas引理，我们找到了LRSM在数学上的矩阵描述，并将LRSM的生成问题转化为了半正定规划问题，从而可以通过数值算法在多项式时间内快速求解。该成果发表在计算机程序理论顶级会议POPL 2018上。