量子Hoare逻辑：扩充与应用
发布时间：2021-05-17 05:32
本文着重对量子Hoare逻辑（QHL）进行扩充和推广,使其适应不同的应用场景,包括:量子程序的调试与测试,量子程序的鲁棒推理,量子程序间关系性质的推理。为了规避和克服Ying[1,2]提出的QHL在应用中可能遇到的困难,本文推导出QHL的变体——应用量子Hoare逻辑（a QHL）。其核心是将QHL量子谓词限制为投影算子,并且保证证明系统依旧具有可靠性与（相对）完备性。主要优势有:（1）推理规则和排序函数的简化有利于计算;（2）可以通过投影谓词引入断言语句,有助于量子程序调试或测试。通过引入鲁棒性推理规则,使a QHL实现对量子程序误差的形式化推理。为了展示a QHL的有效性,本文对线性方程组量子算法（HHL）和量子主成分分析算法（q PCA）的正确性进行形式化验证。本文将概率关系程序逻辑（p RHL）推广至量子情形,建立了量子关系Hoare逻辑（rq PD）,可用于量子程序间关系性质的形式化验证。核心思想概括为:（1）基于量子耦合定义rq PD的正确性公式及其有效性;（2）引入测量条件以便捕获两个量子程序控制流路径的关联性,以保证条件和循环同步推理规则的可靠性;...
【文章来源】：清华大学北京市 211工程院校 985工程院校 教育部直属院校
【文章页数】：154 页
【学位级别】：博士
【文章目录】：
摘要
abstract
第1章 引言
1.1 量子Hoare逻辑的挑战
1.2 量子Hoare逻辑的潜在应用
1.3 研究内容及主要贡献
1.4 论文组织结构
第2章 背景知识
2.1 量子理论
2.1.1 Hilbert空间
2.1.2 线性算子
2.1.3 Hilbert空间的直积
2.1.4 量子态以及距离
2.1.5 酉变换
2.1.6 量子测量
2.1.7 量子操作
2.2 量子程序理论
2.2.1 量子程序语法
2.2.2 操作语义
2.2.3 指称语义
2.2.4 量子谓词与正确性公式
2.2.5 证明系统与完备性
2.3 概率耦合
第3章 应用量子Hoare逻辑
3.1 研究动机与相关工作
3.2 投影Hoare三元组及其推理规则
3.2.1 终止空间
3.2.2 投影Hoare三元组的正确性
3.2.3 提升与简化原理
3.2.4 证明系统
3.2.5 断言和调试方案
3.3 鲁棒性推理规则
3.3.1 近似满足
3.3.2 鲁棒(投影)Hoare三元组
3.3.3 推理规则
3.3.4 鲁棒调试方案
3.4 HHL算法的形式化证明
3.4.1 HHL算法
3.4.2 HHL程序
3.4.3 部分正确性
3.4.4 完全正确性
3.5 qPCA算法的形式化证明
3.5.1 qPCA量子程序
3.5.2 理想程序qPCA′ 的正确性
3.5.3 qPCA的近似正确性
3.6 本章小结
第4章 量子关系Hoare逻辑
4.1 研究动机与相关工作
4.2 量子耦合
4.3 关系程序逻辑
4.3.1 判断与满足
4.3.2 测量条件
4.3.3 可分性条件
4.3.4 证明系统rqPD
4.4 范例
4.4.1 程序对称性
4.4.2 均匀性
4.4.3 量子隐形传态
4.5 投影谓词的推理
4.5.1 推理规则
4.5.2 范例:量子随机游走
4.6 本章小结
第5章 量子差分隐私
5.1 研究动机与相关工作
5.2 量子差分隐私
5.3 量子差分隐私机制
5.3.1 广义振幅阻尼机制
5.3.2 相位和幅度阻尼的组合
5.3.3 去极化机制
5.3.4 GAD,PAD和Dep机制的比较
5.3.5 一个说明性的例子
5.4 组合定理
5.5 本章小结
第6章 总结与展望
6.1 研究内容总结
6.2 未来工作与展望
参考文献
致谢
附录A 可靠性与完备性证明
A.1 a QHL的可靠性与相对完备性
A.2 a QHL鲁棒推理规则的可靠性
A.3 rqPD的可靠性
A.4 rqPD-P的可靠性
个人简历、在学期间发表的学术论文与研究成果
本文编号：3191179
【文章来源】：清华大学北京市 211工程院校 985工程院校 教育部直属院校
【文章页数】：154 页
【学位级别】：博士
【文章目录】：
摘要
abstract
第1章 引言
1.1 量子Hoare逻辑的挑战
1.2 量子Hoare逻辑的潜在应用
1.3 研究内容及主要贡献
1.4 论文组织结构
第2章 背景知识
2.1 量子理论
2.1.1 Hilbert空间
2.1.2 线性算子
2.1.3 Hilbert空间的直积
2.1.4 量子态以及距离
2.1.5 酉变换
2.1.6 量子测量
2.1.7 量子操作
2.2 量子程序理论
2.2.1 量子程序语法
2.2.2 操作语义
2.2.3 指称语义
2.2.4 量子谓词与正确性公式
2.2.5 证明系统与完备性
2.3 概率耦合
第3章 应用量子Hoare逻辑
3.1 研究动机与相关工作
3.2 投影Hoare三元组及其推理规则
3.2.1 终止空间
3.2.2 投影Hoare三元组的正确性
3.2.3 提升与简化原理
3.2.4 证明系统
3.2.5 断言和调试方案
3.3 鲁棒性推理规则
3.3.1 近似满足
3.3.2 鲁棒(投影)Hoare三元组
3.3.3 推理规则
3.3.4 鲁棒调试方案
3.4 HHL算法的形式化证明
3.4.1 HHL算法
3.4.2 HHL程序
3.4.3 部分正确性
3.4.4 完全正确性
3.5 qPCA算法的形式化证明
3.5.1 qPCA量子程序
3.5.2 理想程序qPCA′ 的正确性
3.5.3 qPCA的近似正确性
3.6 本章小结
第4章 量子关系Hoare逻辑
4.1 研究动机与相关工作
4.2 量子耦合
4.3 关系程序逻辑
4.3.1 判断与满足
4.3.2 测量条件
4.3.3 可分性条件
4.3.4 证明系统rqPD
4.4 范例
4.4.1 程序对称性
4.4.2 均匀性
4.4.3 量子隐形传态
4.5 投影谓词的推理
4.5.1 推理规则
4.5.2 范例:量子随机游走
4.6 本章小结
第5章 量子差分隐私
5.1 研究动机与相关工作
5.2 量子差分隐私
5.3 量子差分隐私机制
5.3.1 广义振幅阻尼机制
5.3.2 相位和幅度阻尼的组合
5.3.3 去极化机制
5.3.4 GAD,PAD和Dep机制的比较
5.3.5 一个说明性的例子
5.4 组合定理
5.5 本章小结
第6章 总结与展望
6.1 研究内容总结
6.2 未来工作与展望
参考文献
致谢
附录A 可靠性与完备性证明
A.1 a QHL的可靠性与相对完备性
A.2 a QHL鲁棒推理规则的可靠性
A.3 rqPD的可靠性
A.4 rqPD-P的可靠性
个人简历、在学期间发表的学术论文与研究成果
本文编号：3191179
本文链接：https://www.wllwen.com/shoufeilunwen/xxkjbs/3191179.html
