On the Hardness of Analyzing Quantum Programs Quantitatively
Abstract
We study quantitative properties of quantum programs such as (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 pre-condition 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. Finally, we sketch how the latter can be transformed into an efficient synthesis method.
Categories
Quantum, Complexity Analysis, Expectation Transformers, Automation