Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs

• URL: http://arxiv.org/abs/2205.01959v1
• Date: Wed, 4 May 2022 08:57:44 GMT
• Title: Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs
• Authors: Mingsheng Ying
• Abstract summary: A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties of quantum programs. In this paper, we introduce a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables.
• Score: 1.1878820609988696
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties (e.g. correctness) of quantum programs. Surprisingly, such a logic is missing in the literature, and the existing first-order Birkhoff-von Neumann quantum logic deals with only classical variables and quantifications over them. In this paper, we fill in this gap by introducing a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables. Examples are presented to show our logic is particularly suitable for specifying some important properties studied in quantum computation and quantum information. We further incorporate this logic into quantum Hoare logic as an assertion logic so that it can play a role similar to that of first-order logic for classical Hoare logic and BI-logic for separation logic. In particular, we show how it can be used to define and derive quantum generalisations of some adaptation rules that have been applied to significantly simplify verification of classical programs. It is expected that the assertion logic defined in this paper - first-order quantum logic with quantum variables - can be combined with various quantum program logics to serve as a solid logical foundation upon which verification tools can be built using proof assistants such as Coq and Isabelle/HOL.

Related papers

• BI-based Reasoning about Quantum Programs with Heap Manipulations [5.744265100221585]
  We provide well-founded semantics for a quantum programming language Qwhile-hp with heap manipulations. We develop a quantum BI-style logic that includes interpretations for separating implication. We then adopt this quantum BI-style logic as an assertion language to reason about heap-manipulated quantum programs.
  arXiv  Detail & Related papers  (2024-09-16T10:34:45Z)
• Simple Tests of Quantumness Also Certify Qubits [69.96668065491183]
  A test of quantumness is a protocol that allows a classical verifier to certify (only) that a prover is not classical. We show that tests of quantumness that follow a certain template, which captures recent proposals such as (Kalai et al., 2022) can in fact do much more. Namely, the same protocols can be used for certifying a qubit, a building-block that stands at the heart of applications such as certifiable randomness and classical delegation of quantum computation.
  arXiv  Detail & Related papers  (2023-03-02T14:18:17Z)
• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs [6.2147758224415055]
  Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. We show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic.
  arXiv  Detail & Related papers  (2022-06-28T05:49:55Z)
• On the Common Logical Structure of Classical and Quantum Mechanics [0.0]
  We show that quantum theory does satisfy the classical distributivity law once the full meaning of quantum propositions is properly taken into account. We show that the lattice of statistical propositions in classical mechanics follows the same structure, yielding an analogue non-commutative sublattice of classical propositions.
  arXiv  Detail & Related papers  (2022-06-21T18:31:53Z)
• Entanglement and coherence in Bernstein-Vazirani algorithm [58.720142291102135]
  Bernstein-Vazirani algorithm allows one to determine a bit string encoded into an oracle. We analyze in detail the quantum resources in the Bernstein-Vazirani algorithm. We show that in the absence of entanglement, the performance of the algorithm is directly related to the amount of quantum coherence in the initial state.
  arXiv  Detail & Related papers  (2022-05-26T20:32:36Z)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  This paper introduces a dynamic logic formalism for reasoning about information flow in composite quantum systems. We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness for the Teleportation protocol and for a standard Quantum Secret Sharing protocol.
  arXiv  Detail & Related papers  (2021-10-04T12:20:23Z)
• The Logic of Quantum Programs [77.34726150561087]
  We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems.
  arXiv  Detail & Related papers  (2021-09-14T16:08:37Z)
• Depth-efficient proofs of quantumness [77.34726150561087]
  A proof of quantumness is a type of challenge-response protocol in which a classical verifier can efficiently certify quantum advantage of an untrusted prover. In this paper, we give two proof of quantumness constructions in which the prover need only perform constant-depth quantum circuits.
  arXiv  Detail & Related papers  (2021-07-05T17:45:41Z)
• A Quantum Interpretation of Bunched Logic for Quantum Separation Logic [22.507329566323982]
  We develop a program logic where pre- and post-conditions are BI formulas describing quantum states. We exercise the logic for proving the security of quantum one-time pad and secret sharing.
  arXiv  Detail & Related papers  (2021-01-30T22:24:36Z)
• Secure Two-Party Quantum Computation Over Classical Channels [63.97763079214294]
  We consider the setting where the two parties (a classical Alice and a quantum Bob) can communicate only via a classical channel. We show that it is in general impossible to realize a two-party quantum functionality with black-box simulation in the case of malicious quantum adversaries. We provide a compiler that takes as input a classical proof of quantum knowledge (PoQK) protocol for a QMA relation R and outputs a zero-knowledge PoQK for R that can be verified by classical parties.
  arXiv  Detail & Related papers  (2020-10-15T17:55:31Z)
• Quantum Hoare logic with classical variables [3.1181601933418897]
  We propose a quantum Hoare logic for a simple while language which involves both classical and quantum variables. With novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs.
  arXiv  Detail & Related papers  (2020-08-15T23:56:18Z)

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.