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.
翻译:我们为一种混合的古典-量子编程语言引入一种新的预期变压器。 我们的语义学方法依赖于一种成本结构的新概念,我们引入了这个概念,它可以被视为Keimel和Plotkin的Kegelspitzen的专业化。 我们表明,我们最薄弱的先决条件分析对于语言的操作语义来说既健全又充分。 我们使用诱导的预期期望变压器,为古典-量子程序预期成本分析和预期价值分析提供了正式的分析方法。 我们通过计算一些众所周知的量子算法和协议的预期成本,例如抛掷硬币、重复到成功、纠缠国家准备和量子行等,来说明我们技术的效用。