References & Citations
Computer Science > Programming Languages
Title: Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs (Extended Version)
(Submitted on 28 Nov 2019 (v1), last revised 14 Jul 2022 (this version, v3))
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.
Submission history
From: Junyi Liu [view email][v1] Thu, 28 Nov 2019 06:59:26 GMT (34kb)
[v2] Thu, 3 Feb 2022 13:24:28 GMT (141kb)
[v3] Thu, 14 Jul 2022 09:18:27 GMT (48kb)
Link back to: arXiv, form interface, contact.