Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs (Extended Version)

TL;DR

This paper introduces a novel approach to analyze the expected runtimes of quantum programs by generalizing quantum weakest preconditions, representing runtimes as observable expectations, and providing a practical computation method with notable applications.

Contribution

It develops a new method for computing expected runtimes of quantum programs in finite-dimensional spaces, solving an open problem on quantum random walks.

Findings

Expected runtime expressed as an observable expectation.

Method successfully applied to quantum Bernoulli Factory.

Solved open problem on quantum random walks.

Abstract

We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory -- a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. (STOC 2001) is solved.