Search

In this paper, we introduce dynamic lifting to a quantum circuit-description language, following the Proto-Quipper language approach. Dynamic lifting allows programs to transfer the result of measuring quantum data -- qubits -- into classical data -- booleans -- . We propose a type system and an operational semantics for the language and we state safety properties. Next, we introduce a concrete categorical semantics for the proposed language, basing our approach on a recent model from Rios\&Selinger for Proto-Quipper-M. Our approach is to construct on top of a concrete category of circuits with measurements a Kleisli category, capturing as a side effect the action of retrieving classical content out of a quantum memory. We then show a soundness result for this semantics., Comment: accepted for publication in FSTTCS 2021

While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is achallenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. Recent works initiate solutions for problems occurring at every stage of the development process: high-level program design, implementation, compilation, etc. We review the induced challenges for an efficient use of formal methods in quantum computing and the current most promising research directions.

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. Several program logics have been developed for verification of quantum while-programs. However, there are as yet no general methods for reasoning about (mutual) recursive procedures and ancilla quantum data structure in quantum computing (with measurement). We fill the gap in this paper by proposing a parameterized quantum assertion logic and, based on which, designing a quantum Hoare logic for verifying parameterized recursive quantum programs with ancilla data and probabilistic control. The quantum Hoare logic can be used to prove partial, total, and even probabilistic correctness (by reducing to total correctness) of those quantum programs. 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 is shown by three main examples -- recursive quantum Markov chain (with probabilistic control), fixed-point Grover's search, and recursive quantum Fourier sampling.

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. Several program logics have been developed for verification of non-recursive quantum programs. However, there are as yet no general methods for reasoning about recursive procedures in quantum computing. We fill the gap in this paper by presenting a logic for recursive quantum programs. This logic is an extension of quantum Hoare logic for quantum While-programs. The (relative) completeness of the logic is proved, and its effectiveness is shown by a running example: fixed-point Grover's search., Comment: There are errors in Section 4, i.e., the definition of quantum predicate terms should be repaired. There are also notational abuses

The general completeness problem of Hoare logic relative to the standard model $N$ of Peano arithmetic has been studied by Cook, and it allows for the use of arbitrary arithmetical formulas as assertions. In practice, the assertions would be simple arithmetical formulas, e.g. of a low level in the arithmetical hierarchy. In addition, we find that, by restricting inputs to $N$, the complexity of the minimal assertion theory for the completeness of Hoare logic to hold can be reduced. This paper further studies the completeness of Hoare Logic relative to $N$ by restricting assertions to subclasses of arithmetical formulas (and by restricting inputs to $N$). Our completeness results refine Cook's result by reducing the complexity of the assertion theory.

The nonstandard approach to program semantics has successfully resolved the completeness problem of Floyd-Hoare logic. The known versions of nonstandard semantics, the Hungary semantics and axiomatic semantics, are so general that they are absent either from mathematical elegance or from practical usefulness. The aim of this paper is to exhibit a not only mathematically elegant but also practically useful nonstandard semantics. A basic property of computable functions in the standard model $N$ of Peano arithmetic $PA$ is $\Sigma_1$-definability. However, the functions induced by the standard interpretation of while-programs $S$ in nonstandard models $M$ of $PA$ are not always arithmetical. The problem consists in that the standard termination of $S$ in $M$ uses the finiteness in $N$, which is not the finiteness in $M$. To this end, we shall give a new interpretation of $S$ in $M$ such that the termination of $S$ uses $M$-finiteness, and the functions produced by $S$ in all models of $PA$ have the uniform $\Sigma_1$-definability. Then we define, based on the new semantics of while-programs, a new semantics of Hoare logic in nonstandard models of $PA$, and show that the standard axiom system of Hoare logic is sound and complete w.r.t. the new semantics. It will be established, in $PA$, that the Hungary semantics and axiomatic semantics coincide with the new semantics of while-programs. Moreover, various comparisons with the previous results, usefulness of the nonstandard semantics, and remarks on the completeness issues are presented.