Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene
Algebra
- URL: http://arxiv.org/abs/2110.07018v2
- Date: Tue, 29 Mar 2022 03:27:57 GMT
- Title: Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene
Algebra
- Authors: Yuxiang Peng, Mingsheng Ying, Xiaodi Wu
- Abstract summary: We investigate the reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra.
Key features of KAT including the idempotent law and the nice properties of classical tests fail to hold in the context of quantum programs.
We propose Non-idempotent Kleene Algebra (NKA) as a natural alternative and identify complete and sound semantic models for NKA.
- Score: 11.078562853984211
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We investigate the algebraic reasoning of quantum programs inspired by the
success of classical program analysis based on Kleene algebra. One prominent
example of such is the famous Kleene Algebra with Tests (KAT), which has
furnished both theoretical insights and practical tools. The succinctness of
algebraic reasoning would be especially desirable for scalable analysis of
quantum programs, given the involvement of exponential-size matrices in most of
the existing methods. A few key features of KAT including the idempotent law
and the nice properties of classical tests, however, fail to hold in the
context of quantum programs due to their unique quantum features, especially in
branching. We propose Non-idempotent Kleene Algebra (NKA) as a natural
alternative and identify complete and sound semantic models for NKA as well as
their quantum interpretations. In light of applications of KAT, we demonstrate
algebraic proofs in NKA of quantum compiler optimization and the normal form of
quantum while-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where
tests model quantum predicates following effect algebra, and illustrate how to
encode propositional quantum Hoare logic as NKAT theorems.
Related papers
- Separable Power of Classical and Quantum Learning Protocols Through the Lens of No-Free-Lunch Theorem [70.42372213666553]
The No-Free-Lunch (NFL) theorem quantifies problem- and data-independent generalization errors regardless of the optimization process.
We categorize a diverse array of quantum learning algorithms into three learning protocols designed for learning quantum dynamics under a specified observable.
Our derived NFL theorems demonstrate quadratic reductions in sample complexity across CLC-LPs, ReQu-LPs, and Qu-LPs.
We attribute this performance discrepancy to the unique capacity of quantum-related learning protocols to indirectly utilize information concerning the global phases of non-orthogonal quantum states.
arXiv Detail & Related papers (2024-05-12T09:05:13Z) - 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) - Quantum variational learning for entanglement witnessing [0.0]
This work focuses on the potential implementation of quantum algorithms allowing to properly classify quantum states defined over a single register of $n$ qubits.
We exploit the notion of "entanglement witness", i.e., an operator whose expectation values allow to identify certain specific states as entangled.
We made use of Quantum Neural Networks (QNNs) in order to successfully learn how to reproduce the action of an entanglement witness.
arXiv Detail & Related papers (2022-05-20T20:14:28Z) - Theory of Quantum Generative Learning Models with Maximum Mean
Discrepancy [67.02951777522547]
We study learnability of quantum circuit Born machines (QCBMs) and quantum generative adversarial networks (QGANs)
We first analyze the generalization ability of QCBMs and identify their superiorities when the quantum devices can directly access the target distribution.
Next, we prove how the generalization error bound of QGANs depends on the employed Ansatz, the number of qudits, and input states.
arXiv Detail & Related papers (2022-05-10T08:05:59Z) - Qunity: A Unified Language for Quantum and Classical Computing (Extended
Version) [3.5348690973777006]
We introduce Qunity, a new quantum programming language.
Qunity treats quantum computing as a natural generalization of classical computing.
We show how Qunity can cleanly express several quantum algorithms.
arXiv Detail & Related papers (2022-04-26T15:34:22Z) - 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) - Qubit Regularization and Qubit Embedding Algebras [4.3799421495439175]
We show a systematic procedure to derive QEAs for the O(N) lattice spin models and the SU(N) lattice gauge theories.
A more complete understanding of the QEAs could be helpful in recovering the fixed points of the desired quantum field theories.
arXiv Detail & Related papers (2021-12-03T18:56:31Z) - 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) - On exploring practical potentials of quantum auto-encoder with
advantages [92.19792304214303]
Quantum auto-encoder (QAE) is a powerful tool to relieve the curse of dimensionality encountered in quantum physics.
We prove that QAE can be used to efficiently calculate the eigenvalues and prepare the corresponding eigenvectors of a high-dimensional quantum state.
We devise three effective QAE-based learning protocols to solve the low-rank state fidelity estimation, the quantum Gibbs state preparation, and the quantum metrology tasks.
arXiv Detail & Related papers (2021-06-29T14:01:40Z) - 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) - 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.