The paper extends the expectation transformer based analysis of higher-order probabilistic programs to the quantum higher-order setting. The quantum language we are considering can be seen as an extension of PCF, featuring unbounded recursion. The language admits classical and quantum data, as well as a tick operator to account for costs. Our quantum expectation transformer translates such programs into a functional, non-quantum language, enriched with a type and operations over so called cost-structures. By specializing the cost-structure, this methodology makes it possible to study several expectation based properties of quantum programs, such as average case cost, probabilities of events or expected values, in terms of the translated non-quantum programs, this way enabling classical reasoning techniques. As a show-case, we adapt a refinement type system, capable of reasoning on upper-bounds.

翻译：本文将对高阶概率程序的期望变换子分析方法扩展至量子高阶场景。我们所考察的量子语言可视为带有无界递归特性的PCF语言的扩展。该语言兼容经典与量子数据，并包含用于计量成本的tick算子。我们的量子期望变换子将此类程序转换为一种功能性的非量子语言，该语言通过类型及对所谓成本结构的运算进行了增强。通过对成本结构进行特化，该方法使得我们能够基于转换后的非量子程序研究量子程序的多种基于期望的性质，例如平均情况成本、事件概率或期望值，从而启用经典推理技术。作为示例，我们适配了一种能够推理上界的精化类型系统。