From 34ec732ba8c7660294fadae510f986135eba8c4d Mon Sep 17 00:00:00 2001
From: Niel de Beaudrap <niel.debeaudrap@gmail.com>
Date: Tue, 12 Feb 2019 12:50:04 +0000
Subject: [PATCH] First revision of S1.1 and Introduction page including the
glorious new vision
---
NEWPROPOSAL/FULLPROP.tex | 106 +++++++++++++++++++--------------------
1 file changed, 52 insertions(+), 54 deletions(-)
diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 45bef44..c80b86d 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -50,13 +50,23 @@
\REM{(publishable abstract, max. 1/2 page): Be precise and
concise. This summary will be used to select suited reviewers for
the proposal.}
+\newt{Very recent revisions for the new proposal are in violet}
-Recent investment in quantum technologies has paid off, and quantum computers are now here. Current and near-term quantum computers, known as noisy intermediate-scale quantum (NISQ) devices, have few qubits, short coherence times, and non-trivial gate error. In this regime, quantum software support -- in particular focussed towards compilation and optimisation -- is vital to the efficient use of scarce, noisy, hardware resources, and the development of implementable protocols that go beyond what is feasible classically.
-
-These NISQ computers are not so much single devices, but instead patchworks of components (including classical) which vary greatly between implementations such as silicon qubits, superconducting circuits, or ion traps. Programming such devices currently requires intimate knowledge of the hardware, which is a significant barrier to the realisation of usable, scalable quantum computers, as programs must be rewritten for every new device. High-level software descriptions of quantum algorithms must be translated to low-level control instructions for quantum hardware. However, whereas classical computers have had a roughly static concept of ``low-level instructions'' for decades, the analogous notion for quantum hardware is constantly changing and evolving to cope with the rapid progress in quantum technology. We face a situation where the ever-multiplying range of quantum computers has minimal software support.
+Recent investment in quantum technologies has paid off, and quantum computers are now here. Current and near-term quantum computers, known as noisy intermediate-scale quantum (NISQ) devices, have few qubits, short coherence times, and non-trivial gate error. In this regime, quantum software support -- in particular focussed towards compilation and optimisation -- is vital to the efficient use of scarce, noisy, hardware resources, and the development of implementable protocols that go beyond what is feasible classically.
-This project develops the \zx calculus of observables as a flexible intermediate language for quantum computation, and a core element in compilation for immediate use with NISQ devices. This intermediate language will be versatile enough to target a wide variety of hardware implementations, and simple enough to support any programming language. This project builds on recent significant formal and practical advances in completeness and optimisation of the \zx calculus. The former enables provably-correct program transformations for automatically adding error correction and performing hardware-guided optimisations, e.g. by preferring certain quantum gates over others or enforcing topological constraints. This project will develop, enrich (with annotations), and standardise the \zx language for quantum computation, integrate it into an effective stack of tools for compiling quantum programs, and develop new techniques for automated transformations that make quantum computations run better and faster.
+These NISQ computers are not so much single devices, but instead patchworks of components (including classical) which vary greatly between implementations such as silicon qubits, superconducting circuits, or ion traps. Programming such devices currently requires intimate knowledge of the hardware, which is a significant barrier to the realisation of usable, scalable quantum computers, as programs must be rewritten for every new device. High-level software descriptions of quantum algorithms must be translated to low-level control instructions for quantum hardware.
+\newt{Furthermore, whereas}
+classical computers have had a roughly static concept of ``low-level instructions'' for decades, the analogous notion for quantum hardware is constantly changing and evolving to cope with the rapid progress in quantum technology. We face a situation where the ever-multiplying range of quantum computers has minimal software support.
+\newt{%
+ We propose the development of ``deep quantum compilation'' technology, which is the concept of a compiler for quantum systems which can be used to develop large portions of the software stack, in a way which is modular in design but tightly integrated once compiled.%
+ A ``deep'' quantum compiler will be versatile enough to target a wide variety of hardware implementations, and simple enough to support any programming language.
+ This project builds on recent significant
+ To develop such a compiler, we will leverage the versatility and the power of the \zxcalculus, a tensor-based system for analysing quantum operations.
+ Recent formal and practical advances in completeness and optimisation of the \zxcalculus demonstrate a proof-of-principle of the possibility of developing a deep quantum compiler, including provably-correct program transformations for automatically adding error correction and performing hardware-guided optimisations.
+ Developing such a compiler will allow for the sound development of tightly integrated software stacks for quantum computers, enabling them to perform computations better and faster.
+}%
+
%The goal of this project is to develop the flexible intermediate for compilation and optimisation, which is necessary for the immediate-term practical implementation of post-classical protocols on noisy intermediate-scale quantum computers. %how many buzzwords can we get in this sentence
\REM{ OLDTEXT This project introduces \azx, a flexible intermediate language for
@@ -150,11 +160,13 @@ Describe the specific objectives of the project, which should be clear, measurab
\label{sec:summary:-}
\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.
+ We propose to develop \emph{deep quantum compilation technology}.
+ This consists of techniques for a compiler to translate high-level specifications of quantum programs to operations on a variety of quantum hardware platforms, automatically managing the resources and architectural constraints in doing so.
+ This allows the software stack to be developed and organised in a modular fashion for multiple platforms, and then compiled in an intelligently managed way to make the most of quantum hardware resources.
}
\\
-\textit{\bfseries\ttfamily\color{red!70!black} FIGURE NEEDS RE-DRAWING}
+\textit{\bfseries\ttfamily\color{red!70!black} REPLACE THE FOLLOWING WITH SOMETHING WHICH ILLUSTRATES OUR GLORIOUS VISION OF AN ALL-ENCOMPASSING COMPILER.
+IT MAY BE BEST THAT WE AVOID ANYTHING THAT SUGGESTS A GIANT OCTOPUS SPRAWLING OVER THE FACE OF THE EARTH.}
\vspace{-2mm}
\vspace{-1mm}
@@ -163,51 +175,48 @@ Describe the specific objectives of the project, which should be clear, measurab
\paragraph{Context:}
\label{sec:context}
-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, qsharp}.
\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.
+ Effective programming practise allows the programmer to design software without paying very close attention to the nature of the hardware.
+ In the context of quantum technologies, this is made difficult by the fact that hardware platforms are varied~\cite{PhysRevX.4.041041,Raussendorf-2001,KendonAncilla} \texttt{\bfseries \color{red!70!black}[double-check this list of references for suitability]}, have limited resources, and are evolving quickly.
+ Due to the overhead involved in making quantum computations fault-tolerant, different platforms will continue to be developed for different tasks (with and without error correction), even as quantum hardware technologies mature and demonstrate scalability.
+ The complications presented by limited resources and divergent architectures will likely persist for the forseeable future.
+ For classical programs, modern compiler toolchains such as LLVM\footnote{%
+ The LLVM Compiler Infrastructure, \url{http://llvm.org}}
+ decouple high-level programming from different hardware platforms, allowing for easy and customisable cross-compilation.
+ Building on recent developments in the theory and application of the \zxcalculus~\cite{BH-2017,NW-2017,JPV-2018,DKPdW-2019}, the opportunity exists to develop a more ambitious version of the LLVM concept for quantum computing, bringing forward the day that quantum computers can be exploited for practical application.
}
-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}
\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):
-\begin{itemize}
-\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}
-\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.
+ We will develop \emph{deep quantum compilation technology}: that is to say, techniques which may be used by a compiler to translate high-level quantum programs to low-level operations on quantum hardware platforms.
+ In doing so, it will intelligently manage all of the details involved in realising a quantum procedure on hardware, including
+ \begin{itemize}
+ \item
+ incorporating the architectural constraints of the hardware platform,
+ \item
+ optimising the use of hardware resources,
+ \item
+ and managing the realisation of error correction,
+ \end{itemize}
+ in a way which can be specified in a modular way but which is tightly integrated upon compilation.
+ To demonstrate this technology, we will develop a compiler from a high-level quantum programming language to hardware, for (i)~optically-coupled ion traps (NQIT)~\cite{PhysRevX.4.041041} and (ii)~quantum-dot devices (Grenoble)~\texttt{\bfseries \color{red!70!black}[do we have something here to cite?]}.
+ We will specifically pursue the development of deep quantum compilation technology by exploiting the versatility of the \zxcalculus, and further developing its application.
+}%
+This will greatly improve the software ecosystem for quantum computers:
+\newt{deep quantum compilation will allow future quantum devices to}
+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}
-
-\newt{%
+\textsf{\bfseries \color{red!70!black}%
+ [The following, up to \S1.3, has been modified from the original but has not yet incorporated the glorious new vision set forth in the preceding page.]}
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
@@ -215,18 +224,15 @@ is between a circuit description or a classical simulation.
%(\liquid in particular is tightly integrated with its simulator).
Neither language exposes an IR.
-\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}.}
+ 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.}
+ 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 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.
@@ -260,10 +266,8 @@ Here is an example of such a transformation:\vspace{-1mm}
%\cnotv[0.6] \rTo^*
\cnotvi[0.7]
\]~\\[-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},
@@ -325,18 +329,15 @@ quantum computers.
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]}
+Furthermore, our system allows transformations of tensor networks which cannot be expressed as equations between circuits.
+\texttt{\bfseries\color{red!70!black} [Add diagram illustrating an application of ZX which is not shackled to the circuit model, and text to refer to it]}
% 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}.
-\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
@@ -383,10 +384,9 @@ computation tasks.}
\paragraph{Ambition:}
\label{sec:ambition}
-\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.
-}
+
\REM{
Our central aim is to define, in \azx, (i)~a~formal tool to express formally verified code transformation and
@@ -415,12 +415,10 @@ 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.}
-\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}.
--
GitLab