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逻辑, 用于核实参数化递归量子程序, 以恒定数据和概率控制概率控制为参数。 量子逻辑可以用来证明这些量子程序的部分、 完整、 甚至概率性( 降低到完全正确性) 的校正性。 特别是两个反示例, 用来说明在核查递归回录程序时不完全性判断的断言性判断, 一种反推论是精确性推论的逻辑, 以部分正确性递定的递定的递定的递定性 。

1
下载
关闭预览

相关内容

【新书】Python编程基础,669页pdf
专知会员服务
194+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
强化学习三篇论文 避免遗忘等
CreateAMind
19+阅读 · 2019年5月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
ICLR2019最佳论文出炉
专知
12+阅读 · 2019年5月6日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
LibRec 精选:推荐的可解释性[综述]
LibRec智能推荐
10+阅读 · 2018年5月4日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
carla无人驾驶模拟中文项目 carla_simulator_Chinese
CreateAMind
3+阅读 · 2018年1月30日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
Arxiv
0+阅读 · 2021年9月25日
Arxiv
0+阅读 · 2021年9月24日
Arxiv
9+阅读 · 2020年2月15日
Physical Primitive Decomposition
Arxiv
4+阅读 · 2018年9月13日
Arxiv
4+阅读 · 2018年4月30日
VIP会员
相关VIP内容
【新书】Python编程基础,669页pdf
专知会员服务
194+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
相关资讯
强化学习三篇论文 避免遗忘等
CreateAMind
19+阅读 · 2019年5月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
ICLR2019最佳论文出炉
专知
12+阅读 · 2019年5月6日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
LibRec 精选:推荐的可解释性[综述]
LibRec智能推荐
10+阅读 · 2018年5月4日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
carla无人驾驶模拟中文项目 carla_simulator_Chinese
CreateAMind
3+阅读 · 2018年1月30日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
Top
微信扫码咨询专知VIP会员