Quantum Hoare Logic: Extensions And Applications

This thesis focuses on how to extend quantum Hoare logic?QHL?proposed by Ying^[1,2],to adapt to different application scenarios,including:debugging and testing of quantum programs,robust reasoning of quantum programs,and verifying nontrivial relational properties of quantum programs.In order to circumvent the possible issues in practical use of QHL,we derive a variant of QHL-applied quantum Hoare logic?a QHL?.We restrict the quantum predicates in QHL to projections while ensuring the soundness and?relatively?completeness of the new proof system.The advantages are:?1?the new inference rules and ranking function can significantly simplify calculations;?2?it is possible to introduce assertions based on projections,which benefit the testing and debugging of quantum programs.We introduce robust inference rules that enable a QHL to reason about the robustness of quantum programs.To show the effectiveness of a QHL,we formalize the correctness of the quantum algorithm for linear systems of equations?HHL?and quantum principal component analysis?q PCA?.As an extension of probabilistic relational Hoare logic?p RHL?,we establish the quantum relational Hoare logic?rq PD?,which can be used to reason about nontrivial relational properties of quantum programs.The main ideas are as follows:?1?defining the correctness formula and validity based on quantum coupling;?2?introducing measurement conditions to capture the correlation of the control flows of two quantum programs,ensuring the soundness of the inference rules for conditions and while loop;and?3?introducing separable conditions to establish new structural rules.We also derive the rq PD-P proof system by restricting rq PD to projective predicates which are simpler and more practical.For applications,we use rq PD and rq PD-P to verify the uniformity of quantum Bernoulli factory,the correctness and reliability of quantum teleportation,and the equivalence of the quantum random walks.As a potential application of rq PD–reasoning about the differential privacy of quantum programs,we extend the conceptual framework of differential privacy to the quantum case.Quantum differential privacy ensures that it is almost impossible to distinguish the outputs of quantum computation based on similar quantum databases.Technically,we propose three quantum differential privacy mechanisms by introducing quantum noise and establish the composition theorem for combining several privacy mechanisms.