In this paper, we study quantitative properties of quantum programs. Properties of interest include (positive) almost-sure termination, expected runtime or expected cost, that is, for example, the expected number of applications of a given quantum gate, etc. After studying the completeness of these problems in the arithmetical hierarchy over the Clifford+T fragment of quantum mechanics, we express these problems using a variation of a quantum pre-expectation transformer, a weakest precondition based technique that allows to symbolically compute these quantitative properties. Under a smooth restriction-a restriction to polynomials of bounded degree over a real closed field-we show that the quantitative problem, which consists in finding an upper-bound to the pre-expectation, can be decided in time double-exponential in the size of a program, thus providing, despite its great complexity, one of the first decidable results on the analysis and verification of quantum programs. Finally, we sketch how the latter can be transformed into an efficient synthesis method.

翻译：本文研究量子程序的定量性质。所关注的属性包括（正）几乎必然终止、预期运行时间或预期成本，例如，给定量子门应用的预期次数等。在将这些问题置于算术层级中Clifford+T量子力学片段的完备性研究之后，我们利用量子预期望变换器的一种变体来表达这些问题——这是一种基于最弱前置条件的技术，可符号化地计算这些定量性质。在光滑限制条件下（即限制为实闭域上有界次数的多项式），我们证明：寻求预期望上界的定量问题可在程序规模的双指数时间内判定。尽管其复杂度较高，但这为量子程序分析与验证提供了首批可判定性结果之一。最后，我们简要概述了如何将后者转化为高效的语法分析方法。