Refinement calculus of quantum programs with projective assertions

• URL: http://arxiv.org/abs/2311.14215v1
• Date: Thu, 23 Nov 2023 22:12:57 GMT
• Title: Refinement calculus of quantum programs with projective assertions
• Authors: Yuan Feng, Li Zhou, Yingte Xu
• Abstract summary: This paper introduces a refinement calculus tailored for quantum programs. We first study the partial correctness of nondeterministic programs within a quantum. We also present their semantics in transforming a postcondition to the weakest liberal postconditions.
• Score: 5.151896714190243
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Refinement calculus provides a structured framework for the progressive and modular development of programs, ensuring their correctness throughout the refinement process. This paper introduces a refinement calculus tailored for quantum programs. To this end, we first study the partial correctness of nondeterministic programs within a quantum while language featuring prescription statements. Orthogonal projectors, which are equivalent to subspaces of the state Hilbert space, are taken as assertions for quantum states. In addition to the denotational semantics where a nondeterministic program is associated with a set of trace-nonincreasing super-operators, we also present their semantics in transforming a postcondition to the weakest liberal postconditions and, conversely, transforming a precondition to the strongest postconditions. Subsequently, refinement rules are introduced based on these dual semantics, offering a systematic approach to the incremental development of quantum programs applicable in various contexts. To illustrate the practical application of the refinement calculus, we examine examples such as the implementation of a $Z$-rotation gate, the repetition code, and the quantum-to-quantum Bernoulli factory. Furthermore, we present Quire, a Python-based interactive prototype tool that provides practical support to programmers engaged in the stepwise development of correct quantum programs.

Related papers

• Qrisp: A Framework for Compilable High-Level Programming of Gate-Based Quantum Computers [0.52197339162908]
  We introduce Qrisp, a framework designed to bridge several gaps between high-level programming paradigms and quantum hardware. Qrisp's standout feature is its ability to compile programs to the circuit level, making them executable on most existing physical backends.
  arXiv  Detail & Related papers  (2024-06-20T23:40:22Z)
• Near-Term Distributed Quantum Computation using Mean-Field Corrections and Auxiliary Qubits [77.04894470683776]
  We propose near-term distributed quantum computing that involve limited information transfer and conservative entanglement production. We build upon these concepts to produce an approximate circuit-cutting technique for the fragmented pre-training of variational quantum algorithms.
  arXiv  Detail & Related papers  (2023-09-11T18:00:00Z)
• QbC: Quantum Correctness by Construction [4.572433350229651]
  We propose Quantum Correctness by Construction (QbC), an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way.
  arXiv  Detail & Related papers  (2023-07-28T16:00:57Z)
• Semidefinite programming relaxations for quantum correlations [45.84205238554709]
  We discuss how the core idea of semidefinite relaxations can be adapted for a variety of research topics in quantum correlations. These topics include nonlocality, quantum communication, quantum networks, entanglement, and quantum cryptography.
  arXiv  Detail & Related papers  (2023-07-05T18:00:07Z)
• Verification of Nondeterministic Quantum Programs [1.9302781323430196]
  Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. Nondeterminism has also been introduced in quantum programming, and the termination of nondeterministic quantum programs has been extensively analysed.
  arXiv  Detail & Related papers  (2023-02-15T22:37:23Z)
• Differentiable Quantum Programming with Unbounded Loops [10.648855845619705]
  We provide the first differentiable quantum programming framework with unbounded loops. We introduce a randomized estimator for derivatives to deal with the infinite sum in the differentiation of unbounded loops. We showcase an exciting application of our framework in automatically identifying close-to-optimal parameters for several parameterized quantum applications.
  arXiv  Detail & Related papers  (2022-11-08T19:07:06Z)
• Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
  We propose circuit-oriented symmetry verification that are capable of verifying the commutativity of quantum circuits without the knowledge of the quantum state. In particular, we propose the Fourier-temporal stabilizer (STS) technique, which generalizes the conventional quantum-domain formalism to circuit-oriented stabilizers.
  arXiv  Detail & Related papers  (2021-12-27T21:15:35Z)
• Realization of arbitrary doubly-controlled quantum phase gates [62.997667081978825]
  We introduce a high-fidelity gate set inspired by a proposal for near-term quantum advantage in optimization problems. By orchestrating coherent, multi-level control over three transmon qutrits, we synthesize a family of deterministic, continuous-angle quantum phase gates acting in the natural three-qubit computational basis.
  arXiv  Detail & Related papers  (2021-08-03T17:49:09Z)
• QuaSiMo: A Composable Library to Program Hybrid Workflows for Quantum Simulation [48.341084094844746]
  We present a composable design scheme for the development of hybrid quantum/classical algorithms and for applications of quantum simulation. We implement our design scheme using the hardware-agnostic programming language QCOR into the QuaSiMo library.
  arXiv  Detail & Related papers  (2021-05-17T16:17:57Z)
• Composable Programming of Hybrid Workflows for Quantum Simulation [48.341084094844746]
  We present a composable design scheme for the development of hybrid quantum/classical algorithms and for applications of quantum simulation. We implement our design scheme using the hardware-agnostic programming language QCOR into the QuaSiMo library.
  arXiv  Detail & Related papers  (2021-01-20T14:20:14Z)
• On the Principles of Differentiable Quantum Programming Languages [13.070557640180004]
  Variational Quantum Circuits (VQCs) are predicted to be one of the most important near-term quantum applications. We propose the first formalization of auto-differentiation techniques for quantum circuits.
  arXiv  Detail & Related papers  (2020-04-02T16:46:13Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.