A tutorial introduction to quantum circuit programming in dependently
typed Proto-Quipper
- URL: http://arxiv.org/abs/2005.08396v2
- Date: Sat, 12 Dec 2020 18:31:19 GMT
- Title: A tutorial introduction to quantum circuit programming in dependently
typed Proto-Quipper
- Authors: Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
- Abstract summary: We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types.
We show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits.
- Score: 1.5274311118568713
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short,
an experimental quantum circuit programming language with linear dependent
types. We give several examples to illustrate how linear dependent types can
help in the construction of correct quantum circuits. Specifically, we show how
dependent types enable programming families of circuits, and how dependent
types solve the problem of type-safe uncomputation of garbage qubits. We also
discuss other language features along the way.
Related papers
- Circuit Width Estimation via Effect Typing and Linear Dependency (Long
Version) [1.3597551064547502]
We present Proto-Quipper-R, a circuit description language endowed with a linear dependent type-and-effect system.
We show that our approach is expressive enough to verify realistic quantum algorithms.
arXiv Detail & Related papers (2023-10-29T18:10:31Z) - Category Theory for Quantum Natural Language Processing [0.0]
This thesis introduces quantum natural language processing (QNLP) models based on an analogy between computational linguistics and quantum mechanics.
The grammatical structure of text and sentences connects the meaning of words in the same way that entanglement structure connects the states of quantum systems.
We turn this abstract analogy into a concrete algorithm that translates the grammatical structure onto the architecture of parameterised quantum circuits.
We then use a hybrid classical-quantum algorithm to train the model so that evaluating the circuits computes the meaning of sentences in data-driven tasks.
arXiv Detail & Related papers (2022-12-13T14:38:57Z) - A Complete Equational Theory for Quantum Circuits [58.720142291102135]
We introduce the first complete equational theory for quantum circuits.
Two circuits represent the same unitary map if and only if they can be transformed one into the other using the equations.
arXiv Detail & Related papers (2022-06-21T17:56:31Z) - Analysis of arbitrary superconducting quantum circuits accompanied by a
Python package: SQcircuit [0.0]
Superconducting quantum circuits are a promising hardware platform for realizing a fault-tolerant quantum computer.
We develop a framework to construct a superconducting quantum circuit's quantized Hamiltonian from its physical description.
We implement the methods described in this work in an open-source Python package SQcircuit.
arXiv Detail & Related papers (2022-06-16T17:24:51Z) - LOv-Calculus: A Graphical Language for Linear Optical Quantum Circuits [58.720142291102135]
We introduce the LOv-calculus, a graphical language for reasoning about linear optical quantum circuits.
Two LOv-circuits represent the same quantum process if and only if one can be transformed into the other with the rules of the LOv-calculus.
arXiv Detail & Related papers (2022-04-25T16:59:26Z) - On Dynamic Lifting and Effect Typing in Circuit Description Languages
(Extended Version) [0.0]
We introduce a generalization of the paradigmatic-calculus Proto-Quipper-M, itself modeling the core features of the quantum circuit description language Quipper.
The extension, called Proto-Quipper-K, is meant to capture a very general form of dynamic lifting.
arXiv Detail & Related papers (2022-02-15T18:33:41Z) - Resource Optimisation of Coherently Controlled Quantum Computations with
the PBS-calculus [55.2480439325792]
Coherent control of quantum computations can be used to improve some quantum protocols and algorithms.
We refine the PBS-calculus, a graphical language for coherent control inspired by quantum optics.
arXiv Detail & Related papers (2022-02-10T18:59:52Z) - 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) - QUANTIFY: A framework for resource analysis and design verification of
quantum circuits [69.43216268165402]
QUANTIFY is an open-source framework for the quantitative analysis of quantum circuits.
It is based on Google Cirq and is developed with Clifford+T circuits in mind.
For benchmarking purposes QUANTIFY includes quantum memory and quantum arithmetic circuits.
arXiv Detail & Related papers (2020-07-21T15:36:25Z) - Linear Dependent Type Theory for Quantum Programming Languages [1.7166794984161973]
Modern quantum programming languages integrate quantum resources and classical control.
They must be linearly typed to reflect the no-cloning property of quantum resources.
High-level and practical languages should also support quantum circuits as first-class citizens.
arXiv Detail & Related papers (2020-04-28T13:11:06Z) - PBS-Calculus: A Graphical Language for Coherent Control of Quantum
Computations [77.34726150561087]
We introduce the PBS-calculus to represent and reason on quantum computations involving coherent control of quantum operations.
We equip the language with an equational theory, which is proved to be sound and complete.
We consider applications like the implementation of controlled permutations and the unrolling of loops.
arXiv Detail & Related papers (2020-02-21T16:15:58Z)
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.