發(fā)布時(shí)間：2021-05-17 05:32

　　本文著重對(duì)量子Hoare邏輯（QHL）進(jìn)行擴(kuò)充和推廣,使其適應(yīng)不同的應(yīng)用場景,包括:量子程序的調(diào)試與測試,量子程序的魯棒推理,量子程序間關(guān)系性質(zhì)的推理。為了規(guī)避和克服Ying^[1,2]提出的QHL在應(yīng)用中可能遇到的困難,本文推導(dǎo)出QHL的變體——應(yīng)用量子Hoare邏輯（a QHL）。其核心是將QHL量子謂詞限制為投影算子,并且保證證明系統(tǒng)依舊具有可靠性與（相對(duì)）完備性。主要優(yōu)勢有:（1）推理規(guī)則和排序函數(shù)的簡化有利于計(jì)算;（2）可以通過投影謂詞引入斷言語句,有助于量子程序調(diào)試或測試。通過引入魯棒性推理規(guī)則,使a QHL實(shí)現(xiàn)對(duì)量子程序誤差的形式化推理。為了展示a QHL的有效性,本文對(duì)線性方程組量子算法（HHL）和量子主成分分析算法（q PCA）的正確性進(jìn)行形式化驗(yàn)證。本文將概率關(guān)系程序邏輯（p RHL）推廣至量子情形,建立了量子關(guān)系Hoare邏輯（rq PD）,可用于量子程序間關(guān)系性質(zhì)的形式化驗(yàn)證。核心思想概括為:（1）基于量子耦合定義rq PD的正確性公式及其有效性;（2）引入測量條件以便捕獲兩個(gè)量子程序控制流路徑的關(guān)聯(lián)性,以保證條件和循環(huán)同步推理規(guī)則的可靠性;... 

【文章來源】：清華大學(xué)北京市 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：154 頁

【學(xué)位級(jí)別】：博士

【文章目錄】：
摘要
abstract
第1章 引言
    1.1 量子Hoare邏輯的挑戰(zhàn)
    1.2 量子Hoare邏輯的潛在應(yīng)用
    1.3 研究內(nèi)容及主要貢獻(xiàn)
    1.4 論文組織結(jié)構(gòu)
第2章 背景知識(shí)
    2.1 量子理論
        2.1.1 Hilbert空間
        2.1.2 線性算子
        2.1.3 Hilbert空間的直積
        2.1.4 量子態(tài)以及距離
        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 證明系統(tǒng)與完備性
    2.3 概率耦合
第3章 應(yīng)用量子Hoare邏輯
    3.1 研究動(dòng)機(jī)與相關(guān)工作
    3.2 投影Hoare三元組及其推理規(guī)則
        3.2.1 終止空間
        3.2.2 投影Hoare三元組的正確性
        3.2.3 提升與簡化原理
        3.2.4 證明系統(tǒng)
        3.2.5 斷言和調(diào)試方案
    3.3 魯棒性推理規(guī)則
        3.3.1 近似滿足
        3.3.2 魯棒(投影)Hoare三元組
        3.3.3 推理規(guī)則
        3.3.4 魯棒調(diào)試方案
    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 本章小結(jié)
第4章 量子關(guān)系Hoare邏輯
    4.1 研究動(dòng)機(jī)與相關(guān)工作
    4.2 量子耦合
    4.3 關(guān)系程序邏輯
        4.3.1 判斷與滿足
        4.3.2 測量條件
        4.3.3 可分性條件
        4.3.4 證明系統(tǒng)rqPD
    4.4 范例
        4.4.1 程序?qū)ΨQ性
        4.4.2 均勻性
        4.4.3 量子隱形傳態(tài)
    4.5 投影謂詞的推理
        4.5.1 推理規(guī)則
        4.5.2 范例:量子隨機(jī)游走
    4.6 本章小結(jié)
第5章 量子差分隱私
    5.1 研究動(dòng)機(jī)與相關(guān)工作
    5.2 量子差分隱私
    5.3 量子差分隱私機(jī)制
        5.3.1 廣義振幅阻尼機(jī)制
        5.3.2 相位和幅度阻尼的組合
        5.3.3 去極化機(jī)制
        5.3.4 GAD,PAD和Dep機(jī)制的比較
        5.3.5 一個(gè)說明性的例子
    5.4 組合定理
    5.5 本章小結(jié)
第6章 總結(jié)與展望
    6.1 研究內(nèi)容總結(jié)
    6.2 未來工作與展望
參考文獻(xiàn)
致謝
附錄A 可靠性與完備性證明
    A.1 a QHL的可靠性與相對(duì)完備性
    A.2 a QHL魯棒推理規(guī)則的可靠性
    A.3 rqPD的可靠性
    A.4 rqPD-P的可靠性
個(gè)人簡歷、在學(xué)期間發(fā)表的學(xué)術(shù)論文與研究成果



本文編號(hào)：3191179