Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userQuantum CPOs
107
0
0.0
(
0
)
Added by
EPTCS
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Authors
Andre Kornell
Ask ChatGPT about the research
No Arabic abstract
We introduce the monoidal closed category qCPO of quantum cpos, whose objects are quantized analogs of omega-complete partial orders (cpos). The category qCPO is enriched over the category CPO of cpos, and contains both CPO, and the opposite of the category FdAlg of finite-dimensional von Neumann algebras as monoidal subcategories. We use qCPO to construct a sound model for the quantum programming language Proto-Quipper-M (PQM) extended with term recursion, as well as a sound and computationally adequate model for the Linear/Non-Linear Fixpoint Calculus (LNL-FPC), which is both an extension of the Fixpoint Calculus (FPC) with linear types, and an extension of a circuit-free fragment of PQM that includes recursive types.
rate research
Read More
We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIRs careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.
As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes of bugs from being introduced. There is a need for similar techniques in the quantum regime. Inspired by Hoare Type Theory in the classical paradigm, we propose Quantum Hoare Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions that serve as program specifications. In this paper, we introduce Quantum Hoare Type Theory (QHTT), present its syntax and typing rules, and demonstrate its effectiveness with the help of examples. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs. This is a work in progress.
Quantum computing holds a great promise and this work proposes to use new quantum data networks (QDNs) to connect multiple small quantum computers to form a cluster. Such a QDN differs from existing QKD networks in that the former must deliver data qubits reliably within itself. Two types of QDNs are studied, one using teleportation and the other using tell-and-go (TAG) to exchange quantum data. Two corresponding quantum transport protocols (QTPs), named Tele-QTP and TAG-QTP, are proposed to address many unique design challenges involved in reliable delivery of data qubits, and constraints imposed by quantum physics laws such as the no-cloning theorem, and limited availability of quantum memory. The proposed Tele-QTP and TAG-QTP are the first transport layer protocols for QDNs, complementing other works on the network protocol stack. Tele-QTP and TAG-QTP have novel mechanisms to support congestion-free and reliable delivery of streams of data qubits by managing the limited quantum memory at end hosts as well as intermediate nodes. Both analysis and extensive simulations show that the proposed QTPs can achieve a high throughput and fairness. This study also offers new insights into potential tradeoffs involved in using the two methods, teleportation and TAG, in two types of QDNs.
104 -
Angela Sara Cacciapuoti
, Marcello Caleffi
, Francesco Tafuri andn Francesco Saverio Cataliotti
2018
The Quantum Internet is envisioned as the final stage of the quantum revolution, opening fundamentally new communications and computing capabilities, including the distributed quantum computing. But the Quantum Internet is governed by the laws of quantum mechanics. Phenomena with no counterpart in classical networks, such as no-cloning, quantum measurement, entanglement and teleporting, impose very challenging constraints for the network design. Specifically, classical network functionalities, ranging from error-control mechanisms to overhead-control strategies, are based on the assumption that classical information can be safely read and copied. But this assumption does not hold in the Quantum Internet. As a consequence, the design of the Quantum Internet requires a major network-paradigm shift to harness the quantum mechanics specificities. The goal of this work is to shed light on the challenges and the open problems of the Quantum Internet design. To this aim, we first introduce some basic knowledge of quantum mechanics, needed to understand the differences between a classical and a quantum network. Then, we introduce quantum teleportation as the key strategy for transmitting quantum information without physically transferring the particle that stores the quantum information or violating the principles of the quantum mechanics. Finally, the key research challenges to design quantum communication networks are described.
Isomer search or molecule enumeration refers to the problem of finding all the isomers for a given molecule. Many classical search methods have been developed in order to tackle this problem. However, the availability of quantum computing architectures has given us the opportunity to address this problem with new (quantum) techniques. This paper describes a quantum isomer search procedure for determining all the structural isomers of alkanes. We first formulate the structural isomer search problem as a quadratic unconstrained binary optimization (QUBO) problem. The QUBO formulation is for general use on either annealing or gate-based quantum computers. We use the D-Wave quantum annealer to enumerate all structural isomers of all alkanes with fewer carbon atoms (n < 10) than Decane (C10H22). The number of isomer solutions increases with the number of carbon atoms. We find that the sampling time needed to identify all solutions scales linearly with the number of carbon atoms in the alkane. We probe the problem further by employing reverse annealing as well as a perturbed QUBO Hamiltonian and find that the combination of these two methods significantly reduces the number of samples required to find all isomers.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
