一句话：提出混合经典-量子语言的期望变换器语义，可对量子程序做期望成本与期望值分析。
本文为混合经典-量子编程语言引入了一种新的期望变换器，用于分析程序的期望成本与期望值。其语义基础是一种新的成本结构概念，可视为 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{AvanziniMPPZ22,
title = {Quantum Expectation Transformers for Cost Analysis},
author = {Martin Avanzini and Georg Moser and Romain Pechoux and Simon Perdrix and Vladimir Zamdzhiev},
booktitle = {LICS},
year = {2022},
doi = {10.1145/3531130.3533332}
}