home > publications > AMPP:QPL:24

On the Hardness of Analyzing Quantum Programs Quantitatively

On the Hardness of Analyzing Quantum Programs Quantitatively
Martin Avanzini, Georg Moser, Romain Péchoux and Simon Perdrix
Quantum Physics and Logic 2024, (2024).

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

, , ,