From e4a06a5567761ddefcbbcc39d6cd516c27fec840 Mon Sep 17 00:00:00 2001
From: Niel de Beaudrap <niel.debeaudrap@gmail.com>
Date: Tue, 12 Feb 2019 00:47:10 +0000
Subject: [PATCH] Revisions of Sections 1.1 and 1.2, and deliberate
redefinition of \azx to something annoying to prompt a further redefinition
---
NEWPROPOSAL/FULLPROP.tex | 246 ++++++++++++++++-----------------------
NEWPROPOSAL/quantera.bib | 63 +++++-----
2 files changed, 136 insertions(+), 173 deletions(-)
diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 34bc479..7c713a8 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -135,6 +135,8 @@ Technology Flagship.
\section{EXCELLENCE \REM{(6 pages)}}
\label{sec:overview}
+\newt{Very recent revisions for the new proposal are in violet}
+
\subsection{Targeted breakthrough, baseline of knowledge and skills}
\label{sec:targ-breakthr-basel}
@@ -147,108 +149,85 @@ Describe the specific objectives of the project, which should be clear, measurab
\paragraph{Summary: }
\label{sec:summary:-}
-\oldt{Our goal is to develop a flexible intermediate representation
-for quantum software which enables formally verified program
-transformations, and based on this, to construct the back-end for a
-re-targetable optimising compiler for a variety of
-realistic quantum computer architectures.}\\
-\textit{FIGURE NEEDS RE-DRAWING}
+\newt{%
+ We propose to develop a flexible intermediate representation for quantum software, to enable formally verifiable transformations of circuits.
+ This will form the basis of a re-targetable optimising compiler for any practical quantum computer architecture based on quantum circuits.
+}
+\\
+\textit{\bfseries\ttfamily\color{red!70!black} FIGURE NEEDS RE-DRAWING}
\vspace{-2mm}
\vspace{-1mm}
\cgraph[0.65]{arch-diagram.pdf}\vspace{-5mm}
-
-
\paragraph{Context:}
\label{sec:context}
-\oldt{High-level programming languages (HLLs) increase programmer
-productivity and software reliability, provided that the HLL compiler
-can generate machine code which runs well on
-the intended hardware platform. Quantum algorithm designers have the
-choice of
-several powerful quantum programming languages %, in various paradigms
-\cite{Alexander-S.-Green:2013fk, Paykin2017a, Steiger2016ProjectQ:-An-Op, export:209634}.
-However, proposed implementations of quantum computers vary greatly due
-to differing underlying technologies (ion traps, superconducting
-circuits, optics) and architectural concepts (networked vs. hybrid, measurement
-based, ancilla driven)~\cite{PhysRevX.4.041041,Raussendorf-2001,KendonAncilla},
-and no language takes account of the specific characteristics of any
-given platform. Worse, the technology
-is evolving quickly, none of these characteristics are stable, and no
-consensus has yet emerged on the best choice. For classical programs,
-modern compiler toolchains such as LLVM\footnote{The LLVM Compiler
- Infrastructure, \url{http://llvm.org}}
-decouple the HLL from the machine by using an \emph{intermediate
- representation} (IR), which is independent of both. By translating
-to and from the IR, any HLL may be used on any platform. A quantum IR
-accommodating dissimilar architectures is needed
-to support software on rapidly shifting hardware.}
-
+High-level programming languages (HLLs) increase programmer productivity and software reliability --- provided that the HLL compiler can generate machine code which runs well on the intended hardware platform.
+Quantum algorithm designers have the choice of several powerful quantum programming languages~\cite{Alexander-S.-Green:2013fk, Paykin2017a, Steiger2016ProjectQ:-An-Op, export:209634}.
+\newt{%
+ However, these languages do not describe how to realise programs on specific hardware platforms, of which there are several, using different technologies (ion traps, superconducting circuits, optics) and architectural concepts (networked vs.\ hybrid, ancilla driven, measurement based)~\cite{PhysRevX.4.041041,Raussendorf-2001,KendonAncilla}.
+ Even at such a time as quantum hardware technology matures, we cannot be assured that exactly one platform will predominate for all quantum information processing applications.
+}
+For classical programs, modern compiler toolchains such as LLVM\footnote{%
+ The LLVM Compiler Infrastructure, \url{http://llvm.org}}
+decouple the HLL from the machine by using an \emph{intermediate representation} (IR), which is independent of both.
+By translating to and from the IR, any HLL may be used on any platform.
+A quantum IR accommodating dissimilar architectures is needed to support software on rapidly shifting hardware.
\paragraph{Targeted breakthrough:}
\label{sec:targ-breakthr}
-\oldt{We will define a universal intermediate representation language,
+\newt{%
+ We will define a versatile and universal intermediate representation language,
+}
called \azx, which is platform-agnostic but which facilitates program
-transformations appropriate
-to specific hardware. Specifically, \azx will provide the following (see \S\ref{sec:impl-2-pages} for more detail):
+transformations appropriate to specific hardware.
+Specifically, \azx will provide the following (see \S\ref{sec:impl-2-pages} for more detail):
\begin{itemize}
-\item An easy-to-generate universal language.
- \item Automated IR transformations for
- error correction, resource optimisation, and execution layout.
- \item A complete compilation pipeline from HLL to hardware for (i)
- superconducting transmon qubits (QuTech)
- \cite{Versluis2016Scalable-quantu} and (ii)
- optically-coupled ion traps (NQIT) \cite{PhysRevX.4.041041}.
+\item
+ \newt{An easily-specified and easily-generated universal language for quantum transformations.}
+\item
+ Automated IR transformations for error correction, resource optimisation, and execution layout.
+\item
+ A complete compilation pipeline from HLL to hardware for (i)~superconducting transmon qubits \oldt{(QuTech)~\cite{Versluis2016Scalable-quantu} and (ii)~optically-coupled ion traps (NQIT)~\cite{PhysRevX.4.041041}}.
\end{itemize}
-The theory, algorithms, and software architecture behind this will be
-flexible and extensible, thus permitting programming languages and
-architectures not explicitly included in the project scope to
-be supported. This will greatly improve the software
-ecosystem for quantum computers: by supporting \azx, future quantum
-devices may easily run existing programs, and future programming
-languages automatically gain support on a wide range of hardware.}
+\newt{%
+ The theory, algorithms, and software architecture behind this will be flexible and extensible.
+ This will permit programming languages and architectures not explicitly included in the project scope to be supported.}
+This will greatly improve the software ecosystem for quantum computers: by supporting \azx, future quantum devices may easily run existing programs, and future programming
+languages automatically gain support on a wide range of hardware.
\paragraph{Baseline of knowledge and skills:}
\label{sec:basel-knowl-skills}
-\oldt{The closest extant thing to a quantum IR is QASM
-\cite{Cross2017Open-Quantum-As}, a circuit description
-language. QASM is an output option for ProjectQ
-\cite{Hner2016A-Software-Meth}, and the input language for
-IBM's \emph{Quantum Experience}\footnote{This is a publicly accessible
- 5-qubit device; \url{http://research.ibm.com/quantum/}.}; the
-ProjectQ team describe a compilation process for
-quantum software involving possibly multiple IRs, but do not describe
-a specific one. State-of-the-art quantum programming languages such
-as Quipper \cite{Alexander-S.-Green:2013fk} and \liquid
-\cite{export:209634} support multiple targets; in practice the choice
+\newt{%
+ The closest extant thing to a quantum IR is QASM~\cite{Cross2017Open-Quantum-As}, a circuit description language.
+ QASM is the input language for IBM's quantum computing platforms, including the \emph{IBM Quantum Experience}\footnote{%
+ This is a publicly accessible 5-qubit device; \url{http://research.ibm.com/quantum/}.}.
+ QASM is an output option for ProjectQ \cite{Hner2016A-Software-Meth};
+ the ProjectQ team describe a compilation process for quantum software involving possibly multiple IRs, but do not describe a specific one.
+}
+State-of-the-art quantum programming languages such as Quipper~\cite{Alexander-S.-Green:2013fk}
+\newt{and Q\#~\cite{qsharp}}
+support multiple targets; in practice the choice
is between a circuit description or a classical simulation.
%(\liquid in particular is tightly integrated with its simulator).
Neither language exposes an IR.
-Our proposed language \azx is the successor to the \zxcalculus
-\cite{Coecke:2009aa}, a graphical tensor notation
-developed by members of this consortium during a decade
-of work on the mathematical foundations of quantum computing
-\cite{AbrCoe:CatSemQuant:2004,
+\newt{%
+ Our proposed IR is built on the \zxcalculus~\cite{Coecke:2009aa}, a graphical tensor notation developed by members of this consortium during a decade of work on the mathematical foundations of quantum computing \cite{AbrCoe:CatSemQuant:2004,
%Coecke:2009db, CDKW-lics:2012qy,
- Coecke2017Picturing-Quant}. The \zxcalculus can be viewed in two
-distinct ways: first, as a formal axiomatic theory which encodes the
-properties of complementary observables in categorical algebra;
-second, as a symbolic notation for tensor networks representing
-quantum states and linear operators. Terms in the \zxcalculus are labelled graphs;
-equations in the calculus are reified as a small number of graph
-rewrite rules.
-This equational theory is frequently more
-tractable than working explicitly with matrix representations. Very
-recently \cite{Jeandel2017A-Complete-Axio} members of our consortium
-have presented a version of the \zxcalculus which is \emph{complete}
-for the Clifford+T fragment of quantum mechanics, which means that for the first time
-there is a finite axiomatic theory which can prove every true
-statement about practical quantum computation, and just before submitting this proposal a version of the \zxcalculus which is complete for universal quantum computing i.e.~the Hilbert space based equational theory can be replaced with an entirely diagrammatic one \cite{NgWang}.\footnote{This result still needs some fine-tuning and cleaning-up, but the very fact that this can be done is an unexpected boost for the potential of the \zxcalculus.} This stunning achievement opens the door to many
+ Coecke2017Picturing-Quant}.}
+The \zxcalculus can be viewed in two distinct ways:
+\newt{%
+ either as a formal axiomatic theory which encodes the properties of complementary observables in categorical algebra; or as a symbolic notation for tensor networks representing quantum states and linear operators.}
+Terms in the \zxcalculus are labelled graphs; equations in the calculus are reified as a small number of graph rewrite rules.
+This equational theory is frequently more tractable than working explicitly with matrix representations.
+\newt{%
+ Recently, members of our consortium developed versions of the \zxcalculus which were complete for Clifford+T computations~\cite{Jeandel2017A-Complete-Axio,NW-2018} and for quantum computations including CNOTs and arbitrary single-qubit gates~\cite{NW-2017,JPV-2018}.
+ This means that one can formally prove every equality of quantum circuits in these gate models through the application of a small number of relatively simple rules for rewriting tensors.}
+This stunning achievement opens the door to many
new possibilities for optimisation and verification of quantum
computations.
@@ -259,23 +238,20 @@ computations.
%\REM{The closely related ZW-calculus \cite{Hadzihasanovic2015A-Diagrammatic-} provides a complete characterisation of qubit entanglement-classes.}
-The \zxcalculus has been extensively applied to
-quantum computation, and can easily describe computations
-in both the circuit and measurement-based models of quantum
+The \zxcalculus has been extensively applied to quantum computation, and can easily describe computations in both the circuit and measurement-based models of quantum
computation (MBQC)~\cite{Raussendorf-2001}.
% a proven track record in
%quantum computation, in particular treating error correction
%\cite{Horsman:2011lr,Chancellor2016Coherent-Parity}, and translating between
%architectures \cite{Duncan:2010aa}.
-Due to its great flexibility and expressive power, the \zxcalculus can be used to formulate and verify quantum error correcting codes
-\cite{Chancellor2016Coherent-Parity, Duncan:2013lr} and quantum algorithms
-\cite{Stefano-Gogioso2017Fully-graphical, Zeng2015The-Abstract-St}. Its graphical
-language is especially well-suited to systems which
-naturally have graph structure such as surface codes for topological
-cluster-states \cite{Horsman:2011lr} and MBQC \cite{Duncan:2012uq},
-where it has been used to translate
-\cite{Duncan:2010aa} between the 1-way model
-and the circuit model. Here is an expample of such a transformation:\vspace{-1mm} % (see Figure~\ref{fig:zx-mbqc-cnot}).
+Due to its great flexibility and expressive power, the \zxcalculus can be used to formulate and verify quantum error correcting codes \cite{Chancellor2016Coherent-Parity, Duncan:2013lr} and quantum algorithms \cite{Stefano-Gogioso2017Fully-graphical, Zeng2015The-Abstract-St}.
+\newt{Its graphical representation is especially well-suited to describe systems having a natural have graph structure.
+Examples include surface codes for topological cluster-states \cite{Horsman:2011lr}, and MBQC \cite{Duncan:2012uq}, where it has been used to translate \cite{Duncan:2010aa} between the 1-way model and the circuit model.}
+Here is an example of such a transformation:\vspace{-1mm}
+\\
+\textit{\bfseries\ttfamily\color{red!70!black} CONSIDER USING DIFFERENT FIGURE}
+\vspace{-2mm}%
+ % (see Figure~\ref{fig:zx-mbqc-cnot}).
\[
\cnoti[0.7] \rTo^*
\cnotii[0.6] \rTo^*
@@ -283,15 +259,11 @@ and the circuit model. Here is an expample of such a transformation:\vspace{-1mm
\cnotiv[0.6] \rTo^*
%\cnotv[0.6] \rTo^*
\cnotvi[0.7]
- \]\vspace{-3mm}
-
-Furthermore, techniques for automated
-reasoning in the \zxcalculus were developed for the interactive
-theorem prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-}
-which was used to formally verify quantum communication protocols and error
-correcting codes
-\cite{Chancellor2016Coherent-Parity,Duncan:2013lr}.
-\TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}}
+ \]~\\[-4mm]%
+\newt{
+ Furthermore, members of our consortium have also incorporated these formal reasoning techniques into software, including the interactive theorem prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which was used to formally verify quantum communication protocols and error correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr}) and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early demonstration of the capacity of the \zxcalculus to perform circuit optimisation.
+\TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}
+}
%%% cutting because repeated later
% It is strictly more powerful than the stabiliser
% formalism~\cite{Backens:2012fk},
@@ -318,11 +290,11 @@ correcting codes
\paragraph{Contribution to the theme addressed}
\label{sec:contr-theme-addr}
-\oldt{We specifically address the theme of \emph{Quantum Computation}. The
+We specifically address the theme of \emph{Quantum Computation}. The
goal of \azx is to make it easy to run quantum programs on any
available quantum device. This will speed new quantum devices and
architectures into use, and broaden the range of potential users of
-quantum computers.}
+quantum computers.
\subsection{Novelty, level of ambition and foundational character}
\label{sec:novelty-level-ambit}
@@ -349,29 +321,23 @@ quantum computers.}
\paragraph{Novelty:}
\label{sec:novelty}
-\oldt{\azx is a totally new way of representing computation.
-Tensor networks
-specify \emph{what} the program should do, augmented with separate
-instructions for \emph{how} the hardware should do it. Unlike
-sequences of gates, these tensor networks have no preordained causal
-structure beyond the global input and output. This gives the \azx
-system great flexibility with respect to time-space trade-offs, and
-will help to achieve optimal implementations on diverse architectures.
-Further, the language allows transformations of tensor networks which
-cannot be expressed as equations between circuits. Key examples
-include powerful normal-form theorems for Frobenius
-and Hopf algebras.
+\azx is a totally new way of representing computation.
+Tensor networks specify \emph{what} the program should do, augmented with separate instructions for \emph{how} the hardware should do it.
+Unlike sequences of gates, these tensor networks have no preordained causal structure beyond the global input and output.
+This gives the \azx system great flexibility with respect to time-space trade-offs, and will help to achieve optimal implementations on diverse architectures.
+\newt{Furthermore, our system allows} transformations of tensor networks which cannot be expressed as equations between circuits.
+\oldt{Key examples include powerful normal-form theorems for Frobenius and Hopf algebras.}
+\textsf{\bfseries\color{red!70!black} [I think that we need a better selling point here --- N]}
+
% to reduce its terms to minimal forms. This flexibility has been
% exploited in the \zxcalculus to convert between the circuit model and
% the MBQC model via intermediate steps not expressible in either model
% \cite{Duncan:2010aa,Duncan:2012uq}.
-A second indispensable novelty of our project, compared to existing
-program calculi, is that the equational theory is based on quantum
-mechanics rather than classical concepts. This formal underpinning
-implies that our program transformations are provably correct, and
-indeed will come with proofs of their correctness. This symbolic
-approach also avoids the dimensional explosion of explicit matrices.}
+\newt{%
+ Another novel and essential element of our project is that the basis of the \azx, the \zxcalculus, is a formal equational theory: this implies that our program transformations are provably correct, and indeed will come with proofs of their correctness.
+}
+This symbolic approach also avoids \newt{the immediate dimensional explosion} of explicit matrices.
\REM{This project rests on more than a decade of investigations into the
categorical structure of quantum mechanics. This project therefore has a uniquely
@@ -417,18 +383,10 @@ computation tasks.}
\paragraph{Ambition:}
\label{sec:ambition}
-\oldt{Developing a vertically integrated system from high-level programming
-languages to two different quantum computing architectures
-(\ref{task:delft-model}, \ref{task:NQIT-model}) is ambitious in its
-scale and reach, and has not been done before. We take a technically
-ambitious approach to quantum software, reconstructing a program's
-implementation from its specification and the characteristics of the
-target machine.
+\newt{%
+ Our goal is to develop a vertically integrated system to construct a program's implementation, from its specification in a high-level language, and the characteristics of the target machine, for two different quantum computing architectures (\ref{task:delft-model}, \ref{task:NQIT-model}).
+ This is very technically ambitious: but while it has never been done before, we believe it to be achievable on the basis of our earlier work.
}
-% However we believe, on the basis of our earlier work, that
-% this is achievable within the time frame of the project.
-
-
\REM{
Our central aim is to define, in \azx, (i)~a~formal tool to express formally verified code transformation and
@@ -457,19 +415,15 @@ of logical qubits.
\REM{More here. semantics of quantum programming languages is still very young, and already many dead ends. This project gives a unique opportunity for applications to drive theory.}
-\oldt{All other systems take the gate model of quantum computing as a given:
-this is entirely natural as it is the \emph{lingua franca} of quantum
-computation researchers. The project proposes a new foundation for
-quantum software, based on a flexible, powerful, tensor-based
-representation combined with mathematically rigorous semantics and
-formal verification. The \azx system will allow quantum hardware
-implementors to forget the gate model, present a simpler interface to
-the outside world, and let the compiler bridge the gap. This in turn
-will facilitate the development of new architectures and technologies
-for quantum computing. A key example, exploited in our collaboration
-with NQIT, is that lattice surgery operations on surface codes do not
-fit into the gate model, but have natural and simple representations
-in the \zxcalculus \cite{BH-2017}.}
+\newt{%
+ All other systems take the gate model of quantum computing as a given.
+ This is natural, as it is the \emph{lingua franca} of quantum computation researchers.
+ The project proposes a new foundation for quantum software, based on a flexible tensor-based representation, combined with mathematically rigorous semantics and formal verification.
+ The \azx system will allow the computer to do the heavy lifting of managing resources and mapping operations onto the quantum hardware, allowing both the developers of hardware and software to focus their attentions elsewhere.
+}
+This will facilitate the development of new architectures and technologies for quantum computing.
+A key example, exploited in our collaboration with NQIT, is that lattice surgery operations on surface codes do not fit into the gate model, but have natural and simple representations in the \zxcalculus \cite{BH-2017}.
+
\REM{
While the \zxcalculus is
@@ -512,7 +466,7 @@ to achieving our goal of supporting multiple targets.
% don't stand for anything either!
\azx will retain the mature and effective formal tensor language of
the \zxcalculus at its heart, ensuring semantic soundness, logical
-completeness \cite{Jeandel2017A-Complete-Axio,NgWang}, and allowing
+completeness \cite{Jeandel2017A-Complete-Axio,NW-2017}, and allowing
techniques from earlier work (cf.~\texttt{quantomatic}
\cite{Kissinger2015Quantomatic:-A-}) %, as well as new techniques developed as part of this project,
to be applied to \azx terms. This denotational kernel specifies the
@@ -782,7 +736,7 @@ are the theoretical core of this proposal, and developing effective
techniques for working with \azx diagrams are a prerequisite for our success.
Recent breakthroughs in the theory of the \zx-calculus
-\cite{Jeandel2017A-Complete-Axio,NgWang}, have shown that whenever two
+\cite{Jeandel2017A-Complete-Axio,NW-2017}, have shown that whenever two
\zxcalculus diagrams describe the same linear operator, then one can be
transformed into the other using just a finite set of local,
diagrammatic transformations.
@@ -1947,7 +1901,7 @@ and non-locality in categorical quantum mechanics. LiCS 2012. IEEE Computer Soci
% to 5 relevant publications, and/or products, services
% (incl. widely-used datasets or software), or other achievements
% relevant to the call content. }
- \textbf{Prof.\ Bob Coecke} pioneered categorical and diagrammatic methods for quantum computing (1), and \zxcalculus\ in particular (with Duncan) (2). He is/has supervised approx.~40 PhD students, which include Ng and Wang who recently proved universal completeness of the \zx-calculus \cite{NgWang}, and included Backens who proved stabiliser completeness \cite{1367-2630-16-9-093021}. He co-authored \em Picturing Quantum Processes \em (3), which presents diagrammatic methods for quantum computing to a broader audience.
+ \textbf{Prof.\ Bob Coecke} pioneered categorical and diagrammatic methods for quantum computing (1), and \zxcalculus\ in particular (with Duncan) (2). He is/has supervised approx.~40 PhD students, which include Ng and Wang who recently proved universal completeness of the \zx-calculus \cite{NW-2017}, and included Backens who proved stabiliser completeness \cite{1367-2630-16-9-093021}. He co-authored \em Picturing Quantum Processes \em (3), which presents diagrammatic methods for quantum computing to a broader audience.
\textit{\color{gray} \textbf{Publications:} (1) Samson Abramsky and ---. A categorical semantics of quantum protocols. In LICS 2004. IEEE Computer Society, 2004. (2) Bob Coecke and Ross Duncan. Interacting quantum observables: Categorical algebra and
diagrammatics. New J. Phys, 13(043016), 2011. (3) --- and A. Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017.}
diff --git a/NEWPROPOSAL/quantera.bib b/NEWPROPOSAL/quantera.bib
index 27c0222..a5fdc7e 100644
--- a/NEWPROPOSAL/quantera.bib
+++ b/NEWPROPOSAL/quantera.bib
@@ -168,7 +168,7 @@
Author = {Andrew W. Cross and Lev S. Bishop and John A. Smolin and Jay M. Gambetta},
Date-Added = {2017-03-05 21:01:08 +0000},
Date-Modified = {2017-03-05 21:03:10 +0000},
- Howpublished = {\url{https://github.com/IBM/qiskit-openqasm/blob/master/spec/qasm2.pdf}},
+ Howpublished = {\url{https://arXiv.org/abs/arXiv:1707.03429}},
Keywords = {QASM, quantum computing, programming language},
Month = {January},
Title = {Open Quantum Assembly Language},
@@ -3766,32 +3766,41 @@ well.},
Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8Qai4uLy4uLy4uLy4uLy4uL0RvY3VtZW50cy9SZWFkaW5nL1NjaWVuY2UvcGFwZXJzL0tlbGx5L1N0YXRlIHByZXNlcnZhdGlvbiBieSByZXBldGl0aXZlIGVycm9yIGRldGVjdGlvbi5wZGbSFwsYGVdOUy5kYXRhTxECUAAAAAACUAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzpiHAkgrAAAAIJRBH1N0YXRlIHByZXNlcnZhdGlvbiBiI0EzNEZDRi5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACjT8/RHQd8AAAAAAAAAAAABQAGAAAJIAAAAAAAAAAAAAAAAAAAAAVLZWxseQAAEAAIAADOmHjyAAAAEQAIAADRHPlsAAAAAQAcACCUQQAnAxkAJwMYACcDFwAKjkUACo5EAAJkfAACAGlNYWNpbnRvc2ggSEQ6VXNlcnM6AGt3YjEzMjE1OgBEb2N1bWVudHM6AFJlYWRpbmc6AFNjaWVuY2U6AHBhcGVyczoAS2VsbHk6AFN0YXRlIHByZXNlcnZhdGlvbiBiI0EzNEZDRi5wZGYAAA4AagA0AFMAdABhAHQAZQAgAHAAcgBlAHMAZQByAHYAYQB0AGkAbwBuACAAYgB5ACAAcgBlAHAAZQB0AGkAdABpAHYAZQAgAGUAcgByAG8AcgAgAGQAZQB0AGUAYwB0AGkAbwBuAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgBqVXNlcnMva3diMTMyMTUvRG9jdW1lbnRzL1JlYWRpbmcvU2NpZW5jZS9wYXBlcnMvS2VsbHkvU3RhdGUgcHJlc2VydmF0aW9uIGJ5IHJlcGV0aXRpdmUgZXJyb3IgZGV0ZWN0aW9uLnBkZgATAAEvAAAVAAIAD///AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAPsBAAEIA1wDXgNjA24DdwOFA4kDkAOZA54DqwOuA8ADwwPIAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAA8o=},
Bdsk-Url-1 = {http://dx.doi.org/10.1038/nature14270}}
-@article{export:209634,
- Abstract = {Languages, compilers, and computer-aided design tools will be essential for
- scalable quantum computing, which promises an exponential leap in our ability to
- execute complex tasks. LIQUi|> is a modular software architecture designed to
- control quantum hardware. It enables easy programming, compilation, and
- simulation of quantum algorithms and circuits, and is independent of a specific
- quantum architecture. LIQUi|> contains an embedded, domain-specific language
- designed for programming quantum algorithms, with F{\#} as the host language. It
- also allows the extraction of a circuit data structure that can be used for
- optimization, rendering, or translation. The circuit can also be exported to
- external hardware and software environments. Two different simulation
- environments are available to the user which allow a trade-off between number of
- qubits and class of operations. LIQUi|> has been implemented on a wide range
- of runtimes as back-ends with a single user front-end. We describe the
- significant components of the design architecture and how to express any given
- quantum algorithm.},
- Author = {Dave Wecker and Krysta M. Svore},
- Date-Added = {2015-02-06 16:40:20 +0000},
- Date-Modified = {2015-02-06 16:41:57 +0000},
- Eprint = {arXiv:1402.4467},
- Month = {February},
- Title = {LIQUi|>: A Software Design Architecture and Domain-Specific Language for Quantum Computing},
- Url = {http://research.microsoft.com/apps/pubs/default.aspx?id=209634},
- Year = {2014},
- Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QdS4uLy4uLy4uLy4uLy4uL0RvY3VtZW50cy9SZWFkaW5nL1NjaWVuY2UvcGFwZXJzL1dlY2tlci9MSVFVaXw+IEEgU29mdHdhcmUgRGVzaWduIEFyY2hpdGVjdHVyZSBhbmQgRG9tYWluLVNwZWNpZmljLnBkZtIXCxgZV05TLmRhdGFPEQJwAAAAAAJwAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADOmIcCSCsAAACcKFAfTElRVWl8PiBBIFNvZnR3YXJlIEQjOUMyMjQ0LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAJwiRNBRHfEAAAAAAAAAAAAFAAYAAAkgAAAAAAAAAAAAAAAAAAAABldlY2tlcgAQAAgAAM6YePIAAAARAAgAANBRAdEAAAABABwAnChQACcDGQAnAxgAJwMXAAqORQAKjkQAAmR8AAIAak1hY2ludG9zaCBIRDpVc2VyczoAa3diMTMyMTU6AERvY3VtZW50czoAUmVhZGluZzoAU2NpZW5jZToAcGFwZXJzOgBXZWNrZXI6AExJUVVpfD4gQSBTb2Z0d2FyZSBEIzlDMjI0NC5wZGYADgB+AD4ATABJAFEAVQBpAHwAPgAgAEEAIABTAG8AZgB0AHcAYQByAGUAIABEAGUAcwBpAGcAbgAgAEEAcgBjAGgAaQB0AGUAYwB0AHUAcgBlACAAYQBuAGQAIABEAG8AbQBhAGkAbgAtAFMAcABlAGMAaQBmAGkAYwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAdVVzZXJzL2t3YjEzMjE1L0RvY3VtZW50cy9SZWFkaW5nL1NjaWVuY2UvcGFwZXJzL1dlY2tlci9MSVFVaXw+IEEgU29mdHdhcmUgRGVzaWduIEFyY2hpdGVjdHVyZSBhbmQgRG9tYWluLVNwZWNpZmljLnBkZgAAEwABLwAAFQACAA///wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgEGAQsBEwOHA4kDjgOZA6IDsAO0A7sDxAPJA9YD2QPrA+4D8wAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAP1},
- Bdsk-Url-1 = {http://research.microsoft.com/apps/pubs/default.aspx?id=209634}}
+@inproceedings{qsharp,
+ title={Q\#: Enabling scalable quantum computing and development with a high-level domain-specific language},
+ author={Krysta M. Svore and Alan Geller and Matthias Troyer and John Azariah and Christopher Granade and Bettina Heim and Vadym Kliuchnikov and Mariia Mykhailova and Andres Paz and Martin Roetteler},
+ booktitle={Proceedings of the Real World Domain Specific Languages Workshop (RWDSL 2018)},
+ preprint={arXiv:1803.00652},
+ year=2018
+}
+
+@article{JPV-2018,
+ author={Emmanuel Jeandel and Simon Perdrix and Renaud Vilmart},
+ title={Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics},
+ year=2018,
+ preprint={arXiv:1801.10142}
+}
+
+@article{NW-2018,
+ author={Kang Feng Ng and Quanlong Wang},
+ title={Completeness of the ZX-calculus for Pure Qubit Clifford+T Quantum Mechanics},
+ year=2018,
+ preprint={arXiv:1801.07993}
+}
+
+@article{NW-2017,
+ author={Kang Feng Ng and Quanlong Wang},
+ title = {A universal completion of the ZX-calculus},
+ year=2017,
+ preprint={arXiv:1706.09877}
+}
+
+@article{DKPdW-2019,
+ author={Ross Duncan, Aleks Kissinger, Simon Pedrix, John van de Wetering},
+ title={Graph-theoretic Simplification of Quantum Circuits with the {ZX}-calculus},
+ year=2019,
+ preprint={arXiv:1902.03178}
+}
@article{Raphael-Dias-da-Silva:2013aa,
Abstract = {One of the main goals in quantum circuit optimisation is to reduce the number of ancillary qubits and the depth of computation, to obtain robust computation. However, most of known techniques, based on local rewriting rules, for parallelising quantum circuits will require the addition of ancilla qubits, leading to an undesired space-time tradeoff. Recently several novel approaches based on measurement-based quantum computation (MBQC) techniques attempted to resolve this problem. The key element is to explore the global structure of a given circuit, defined via translation into a corresponding MBQC pattern. It is known that the parallel power of MBQC is superior to the quantum circuit model, and hence in these approaches one could apply the MBQC depth optimisation techniques to achieve a lower depth. However, currently, once the obtained parallel pattern is translated back to a quantum circuit, one should either increase the depth or add ancilla qubits. In this paper we characterise those computations where both optimisation could be achieved together. In doing so we present a new connection between two MBQC depth optimisation procedures, known as the maximally delayed generalised flow and signal shifting. This structural link will allow us to apply an MBQC qubit optimisation procedure known as compactification to a large class of pattern including all those obtained from any arbitrary quantum circuit. We also present a more efficient algorithm (compared to the existing one) for finding the maximally delayed generalised flow for graph states with flow.},
--
GitLab