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

• Quantum Homogenization as a Quantum Steady State Protocol on NISQ Hardware [42.52549987351643]
  Quantum homogenization is a reservoir-based quantum state approximation protocol. We extend the standard quantum homogenization protocol to the dynamically-equivalent ($mathttSWAP$)$alpha$ formulation. We show that our proposed protocol yields a completely positive, trace preserving (CPTP) map under which the code subspace is correctable.
  arXiv  Detail & Related papers  (2024-12-19T05:50:54Z)
• Design and synthesis of scalable quantum programs [0.8007726207322294]
  We present a scalable, robust approach to creating quantum programs of arbitrary size and complexity. The quantum program is expressed in terms of a high-level model together with constraints and objectives on the final program. The technology adapts electronic design automation methods to quantum computing, finding feasible implementations in a virtually unlimited functional space.
  arXiv  Detail & Related papers  (2024-12-10T10:12:03Z)
• 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)
• Semidefinite programming relaxations for quantum correlations [42.72938925647165]
  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)
• 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.