Reasoning about Parameterized Recursive Quantum Programs with Ancilla Data and Probabilistic Control

ACM Transactions on Computational Logic, vol. 27, pp. 1–63

Abstract

Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. In addition, ancilla quantum data, e.g., ancilla qubits, have been extensively employed in designing various quantum algorithms, especially in the design of quantum circuits, and are also included in the mainstream quantum programming languages. Several program logics have been developed for the verification of quantum While-programs. However, there are as yet no general methods for reasoning about general recursive procedures with parameter passing and ancilla data in quantum computing (with measurement). We fill the gap in this article by proposing a parameterized quantum assertion logic and, based on which, designing a Hoare logic for verifying parameterized recursive quantum programs with ancilla data and probabilistic control (induced by quantum measurement). The assertion logic is a unifying framework for defining various assertions of both classical (deterministic or probabilistic) and quantum programs. Besides proving partial and total correctness of the above quantum programs, the Hoare logic can be used to prove probabilistic correctness of these programs by reducing it to total correctness. Concretely, an axiomatic basis of reasoning with both approximate and exact probabilities is established grounded on the soundness and completeness theorem of the Hoare logic. In particular, two counterexamples for illustrating incompleteness of non-parameterized assertions in verifying recursive procedures, and, one counterexample for showing the failure of reasoning with exact probabilities based on partial correctness, are constructed. The effectiveness of our logic in verifying quantum programs with the above mechanisms is shown by three main examples—recursive quantum Markov chain (with probabilistic control), fixed-point Grover’s search, and recursive quantum Fourier sampling. What’s more, the successful verification of recursive quantum Fourier sampling illustrates that the Hoare logic has the potential in verifying more complicated programs, e.g., with data structure of arrays and functionality of quantum uncomputation (i.e., restoring the allocated quantum data to their original state before deallocation).

Authors 3

1. Dominique Unruh Aachen

   RWTH Aachen University · University of Tartu

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany and University of Tartu, Tartu, Estonia

2. Benoît Valiron

   Centre National de la Recherche Scientifique · Université Paris-Saclay · Institut national de recherche en sciences et technologies du numérique · CentraleSupélec · Laboratoire Méthodes Formelles

   Affiliation as printed

   Université Paris-Saclay, CentraleSupélec, Inria, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Gif-sur-Yvette, France

3. Mingsheng Ying

   University of Technology Sydney

   Affiliation as printed

   Centre for Quantum Software and Information, University of Technology Sydney, Broadway, Australia