论文标题
量子期望变压器进行成本分析
Quantum Expectation Transformers for Cost Analysis
论文作者
论文摘要
我们为混合的古典量词编程语言介绍了一种新型的期望变压器。我们的语义方法依赖于成本结构的新概念，我们介绍了成本结构，可以看作是Keimel和Plotkin的Kegelspitzen的专业化。我们表明，对于语言的操作语义，我们最弱的前提分析既声音又足够。使用诱导的预期变压器，我们为经典量词计划的预期成本分析和预期价值分析提供了形式的分析方法。我们通过计算几种众所周知的量子算法和协议的预期成本来说明我们的技术的有用性，例如抛弃硬币，重复直到成功，纠缠状态准备和量子步行。
We introduce a new kind of expectation transformer for a mixed classical-quantum programming language. Our semantic approach relies on a new notion of a cost structure, which we introduce and which can be seen as a specialisation of the Kegelspitzen of Keimel and Plotkin. We show that our weakest precondition analysis is both sound and adequate with respect to the operational semantics of the language. Using the induced expectation transformer, we provide formal analysis methods for the expected cost analysis and expected value analysis of classical-quantum programs. We illustrate the usefulness of our techniques by computing the expected cost of several well-known quantum algorithms and protocols, such as coin tossing, repeat until success, entangled state preparation, and quantum walks.
