Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of quantum while-programs. However, there are as yet no general methods for reasoning about (mutual) recursive procedures and ancilla quantum data structure in quantum computing (with measurement). We fill the gap in this paper by proposing a parameterized quantum assertion logic and, based on which, designing a quantum Hoare logic for verifying parameterized recursive quantum programs with ancilla data and probabilistic control. The quantum Hoare logic can be used to prove partial, total, and even probabilistic correctness (by reducing to total correctness) of those quantum programs. In particular, two counterexamples for illustrating incompleteness of non-parameterized assertions in verifying recursive procedures, and, one counterexample for showing the failure of reasoning with exact probabilities based on partial correctness, are constructed. The effectiveness of our logic is shown by three main examples -- recursive quantum Markov chain (with probabilistic control), fixed-point Grover's search, and recursive quantum Fourier sampling.
翻译:多数现代( 古典) 编程语言支持循环。 校正还成功地应用于设计数量子算法, 并引入了数量子编程语言。 因此, 可以预计循环将成为量子编程的基本范例之一。 已经为量子制程开发了几种程序逻辑, 用于校验量子程序与程序。 但是, 在量子计算( 测量) 中, 还没有一般的推理方法( 双向) 递归程序和 ancilla 量子数据结构。 我们提出了一个参数化量子主张逻辑来填补本文件的空白, 并在此基础上设计一个量子Hare逻辑, 用于核实参数化递归量子程序, 以恒定数据和概率控制概率控制为参数。 量子逻辑可以用来证明这些量子程序的部分、 完整、 甚至概率性( 降低到完全正确性) 的校正性。 特别是两个反示例, 用来说明在核查递归回录程序时不完全性判断的断言性判断, 一种反推论是精确性推论的逻辑, 以部分正确性递定的递定的递定的递定性 。