@@ -57,7 +57,7 @@ These NISQ computers are not so much single devices, but instead patchworks of c
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.
%The goal of this project is to develop the flexible intermediate representation 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
%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
quantum computation, which removes this obstacle by providing a
...
...
@@ -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.
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, 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.
}
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
\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
...
...
@@ -495,7 +449,9 @@ multiple options and to address high scientific and technological
risks.
}
\oldt{Our proposed \azx language is an advanced \textsc{zx}-style system
\benREM{I think this part is more or less OK to keep ``as it''.}
Our proposed \azx language is an advanced \textsc{zx}-style system
augmented with features needed for applications. The \zxcalculus
occupies a place in quantum computation similar to the
$\lambda$-calculus in classical computing: it provides a solid but
...
...
@@ -512,7 +468,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
...
...
@@ -525,7 +481,7 @@ Development of such techniques is a low-risk extension of earlier
work, and will be done early in the project
(\ref{task:algorithms},\ref{task:basic-opt}). Further, at this stage
a program can be translated to a fault-tolerant equivalent with
respect to a chosen error-correcting code.}
respect to a chosen error-correcting code.
% \REM{Can do useful stuff at this level! Some optimisation; ECC
% simple generic optimisations. e.g.
...
...
@@ -543,8 +499,7 @@ respect to a chosen error-correcting code.}
\oldt{The annotations of the second layer provide the basis of \emph{augmented
The annotations of the second layer provide the basis of \emph{augmented
rewrites}: program transformations which are guided by the
annotations to achieve particular goals, not expressible in the basic
tensor language. For instance, there is an efficient algorithm
...
...
@@ -557,14 +512,15 @@ We propose to generalise this concept to encompass other sorts of information wh
For example, we would develop a system which specifies both how to represent logical operations in a particular error correcting code, and how the operations are constrained in order to satisfy basic precautions to keep the realisation fault-tolerant (\ref{task:ECC}).
We may then attempt to re-write procedures, to minimise the number of operations subject to the constraints described by those annotations.
We may further elaborate such a system of annotations by a description of the constraints and the costs involved for operations within a particular hardware platform (\ref{task:runnable}).
For example, in
%%For example, in
% Other
%examples of annotations might include paths in the graph corresponding
%to the trajectories of physical qubits, or subgraphs corresponding to
%the primitive hardware operations and the time required to execute
%them. For
hybrid architectures like NQIT, the annotations will also
indicate the differing behaviour of the subsystems. Augmented
%%hybrid architectures like NQIT, the annotations will also
%%indicate the differing behaviour of the subsystems.
Augmented
rewrites will be used to find a runnable implementation of the
abstract tensor for the target platform, and to optimise resource use.
Early in the project, we will implement translations from existing
quantum programming languages~(\ref{task:trans1}). These will provide
examples and test cases, and allow comparative
evaluation.}% of the \azx system. %We will adapt an existing compiler to generate parameterised \azx terms (\ref{task:trans2}).
evaluation. % of the \azx system. %We will adapt an existing compiler to generate parameterised \azx terms (\ref{task:trans2}).
% Due to the fact that there exist ZX-based software, additional features were added to the language e.g.~`bang-boxes' which are formal incarnations of the ``..." occurring in the above equations.
...
...
@@ -608,7 +564,6 @@ evaluation.} % of the \azx system. %We will adapt an existing compiler to gener
% \REM{Risk assessment: which are easy, which are hard? Dependencies.}
\REM{WHY this is a good idea.}
...
...
@@ -659,9 +614,9 @@ various themes: the relation between \zx and other quantum computing representat
\subsubsection{A quantum compiler stack}
\label{sec:progr-lang-supp}
\oldt{In the quantum setting, several powerful high-level languages
(HLLs) such as Quipper~\cite{Alexander-S.-Green:2013fk} and \liquid
\cite{export:209634} have been proposed. As in the case of their
In the quantum setting, several powerful high-level languages
(HLLs) such as Quipper~\cite{Alexander-S.-Green:2013fk} and Q\#
\cite{qsharp} have been proposed. As in the case of their
classical counterparts, these HLLs are not designed to be run directly
on quantum hardware, rather their compilers typically output quantum
circuit descriptions.
...
...
@@ -675,48 +630,34 @@ general framework for compilation of HLLs to \azx.
Since most existing quantum HLLs can output circuit descriptions, and
since circuits can easily be represented in the \zxcalculus, we first
design a simple front end for the circuit language
QASM~\cite{Cross2017Open-Quantum-As} in
\ref{task:transQASM}. This will allow \azx terms to be produced from
virtually any extant quantum HLL, albeit rather naively.
Later, we will perform concrete front-end experiments using more
sophisticated existing HLLs, for example \emph{Quipper},
\liquid, or ProjectQ \cite{Steiger2016ProjectQ:-An-Op} during the
long running task~\ref{task:transHLL}.
This work package consists of a back-and-forth interaction between
HLLs and \azx, which is why many of its tasks span the entire lifetime
of the project. HLL development influences \azx by providing the
control structures and other constructs that must be represented at
\azx level. Conversely, \azx developments will influence HLL, as we
analyse how information and requirements from the back-end flow upward
in a meaningful way, and how this can be translated into compilation
flags and assertions/hints to the compiler within HLL programs.
A key research challenge of this work package consists in the
management of the {\em classical computation} and {\em classical
information} within quantum algorithms: What computation should
occur at the \azx-generation phase, and which classical parameters are
passed on to the \azx terms? To help answer this question we will
design a test suite (\ref{task:testBench}) to compare possible
solutions.
focus on a simple front end for the circuit language
QASM~\cite{Cross2017Open-Quantum-As} in \ref{task:testBench}. This
will allow \azx terms to be produced from virtually any extant quantum
HLL, albeit rather naively. Later, we will perform concrete front-end
experiments using more sophisticated existing HLLs, for example
\emph{Quipper}, Q\#~\cite{qsharp}, or ProjectQ
\cite{Steiger2016ProjectQ:-An-Op} during the
task~\ref{task:betterboxes}.
%
The open database of tests developed in \ref{task:testBench} will
serve as a measuring tool for the quality of the output. The database
will also be made available to the community for rating and testing
future compilers or optimisation techniques. To encourage interaction
from other research groups, and to support other languages, both our
interface and the \azx language will be made
public.}
\subsubsection{Representation and reasoning}
\label{sec:machines-models}
\REM{stuff about WP 2 here}
\oldt{Proposed and existing quantum devices differ along a variety of axes.
public.
%% OUTDATED
% This work package consists of a back-and-forth interaction between
% HLLs and \azx, which is why many of its tasks span the entire lifetime
% of the project. HLL development influences \azx by providing the
% control structures and other constructs that must be represented at
% \azx level. Conversely, \azx developments will influence HLL, as we
% analyse how information and requirements from the back-end flow upward
% in a meaningful way, and how this can be translated into compilation
% flags and assertions/hints to the compiler within HLL programs.
Proposed and existing quantum devices differ along a variety of axes.
At the most abstract level, the quantum circuit model and the
1-way model \cite{Raussendorf-2001} have different execution
concepts and primitive operations, despite their computational
...
...
@@ -726,10 +667,44 @@ restrictions on which qubits may interact directly.
%Looking more closely,
Primitive operations will require different amounts of time,
different qubit implementations have different failure
modes.\REM{noise,fidelitY} In a hybrid architecture like NQIT, these
properties will vary across the subsystems, with concomitant
implications for the execution of the desired program.
modes.\REM{noise,fidelitY}
Due to its novelty, we adopt an exploratory approach. Initially, and
in parallel, we study the circuit model (\ref{task:circuit-model}) and
the 1-way model (\ref{task:mbqc-model}) because these models are well
understood, stable, and have been extensively treated in the
\zxcalculus literature. We will use these examples to develop
prototypical \azx constructs expressing the relevant properties. This
consists in three tightly related tasks: decomposing the tensor
network into atomic operations; characterising runnability with
respect to the model by predicates in monadic second order logic; and
transforming the tensor network into an equivalent runnable version.
This experience will inform the later work in \ref{wp:theory} and
\ref{wp:usefulstuff}.
Although we will provide specific modules for the tasks described above, the
\azx system is intended to extensible, so we will also publish an open
API and specification language to simplify the task of adding new
architectures and error correcting schemes to the system
(\ref{task:backendapi}).
%% OUTDATED
%In a hybrid architecture like NQIT, these
%properties will vary across the subsystems, with concomitant
%implications for the execution of the desired program.
\subsubsection{Representation, reasoning, and resources}
\label{sec:machines-models}
\REM{stuff about WP 2 here}
\oldt{\benREM{This
paragraph needs refactoring, but I need Belen's input to make a
vaguely\\coherent new text}
Since the overall goal of the project is to produce a
\emph{retargetable} compiler, able to generate executables for
multiple architectures, these differing characteristics must be taken
...
...
@@ -742,47 +717,63 @@ characteristics and architectural constraints of various idealised and
realistic machines, and develop language features of \azx to express
these properties. The goal is two-fold: to facilitate
\emph{code-generation} for a given machine from an \azx term; and to
expose information needed by the \emph{optimiser}.
expose information needed by the \emph{optimiser}.}
Due to its novelty, we adopt an exploratory approach. Initially, and
in parallel, we study the circuit model (\ref{task:circuit-model}) and
the 1-way model (\ref{task:mbqc-model}) because these models are well
understood, stable, and have been extensively treated in the
\zxcalculus literature. We will use these examples to develop
prototypical \azx constructs expressing the relevant properties. This
consists in three tightly related tasks: decomposing the tensor
network into atomic operations; characterising runnability with
respect to the model by predicates in monadic second order logic; and
transforming the tensor network into an equivalent runnable version.
This experience will inform the later work in \ref{wp:theory} and
\ref{wp:usefulstuff}.
A key research challenge of this work package consists in the
management of the {\em classical computation} and {\em classical
information} within quantum algorithms: What computation should
occur at the \azx-generation phase, and which classical parameters are
passed on to the \azx terms? Task \ref{task:betterboxes} focuses on
the question of tests based on measurement results: how should they be
integrated within \azx?
%
While in the early stages of the project, it will already be quite
useful to study concrete diagrams of fixed size (e.g. a quantum
circuit on $N$ qubits for a previously-fixed $N$), in task
\ref{task:axioms}, we will extend \azx to support parametrised
families of diagrams (e.g. quantum circuits with $N$ qubits where $N$
can vary) mirroring the control structures present in a quantum
HLL. This will enable more sophisticated, generic optimisations to be
run in advance of needing any particular computational procedure.
The test suite designed in~\ref{task:testBench}
will be used to compare and choose amongst the possible solutions.
In the second phase we switch attention to real computers. The first
target is a classical simulator running on HPC hardware provided by
our industrial partner Bull. This will leverage existing expertise in
simulation, combined with new techniques for symbolic evaluation of
\azx terms. \ROUGH{Finally we study two concrete quantum computers
based on different technologies: superconducting circuits (Delft)
and optically linked ion traps (NQIT).} In both cases we will
interact strongly with the experimental groups working on these
models, who are either members of our consortium (S. Benjamin and
N. de Beaudrap for NQIT) or our advisory board (L. DiCarlo in Delft).
Since these architectures are dissimilar, tackling both is an ideal
demonstration of our approach. The completion of this phase will
allow quantum programs represented as \azx terms to be run on real
hardware.}
\subsubsection{Machine-independent optimisation}
\label{sec:repr-reas-azx}
\oldt{The formal mechanisms for transforming the \azx diagrams produced by
The formal mechanisms for transforming the \azx diagrams produced by
HLL compilers into optimised, physically implementable computations
are the theoretical core of this proposal, and developing effective
techniques for working with \azx diagrams are a prerequisite for our success.
techniques for working with \azx diagrams are a prerequisite for our
success. We forsee three stage in the compilation process of an \azx
term into a physical machine. The first two stages are
machine-independent (\ref{wp:theory}) while the last stage is machine
dependent (\ref{wp:usefulstuff}).
The tasks to be performed within WP3 and WP4 may be broadly described in terms of how the \azx compiler will transform \zx terms produced by the front-end to obtain instructions to be realised by a quantum computer (or software quantum simulator) at the back-end.
These stages are: (i)~an initial round of generic,
hardware-independent optimisations; (ii)~application of some choice of
strategy for error correction; (iii)~translation to a specialised
annotation system which represents the parameters and constraints of a
specific hardware implementation; and finally (iv)~another round of
optimisation within the constraints imposed by the error correction
and hardware models.
WP3 is devoted to Items (i) and (ii) while WP4 focuses on (iii) and (iv).
In addition to the development of the tools for these stages, WP4 will develop an interface for the specification of the annotation systems used in stages (iii) and~(iv) above, allowing for easy extension of the \azx compiler to arbitrary hardware systems and allowing \azx to act as a general-purpose quantum compiler.
The first stage of the compilation process represents a ``generic optimisation'' subroutine (\ref{task:basic-opt}), which may be applied to arbitrary \zx terms.
This subroutine will re-write \zx terms into ones with fewer resources in a broadly applicable sense, such as fewer total nodes or fewer nodes which realise non-Clifford transformations (for instance, corresponding to $T$ gates).
This may be developed independently of the results of WP1 or WP2 using existing techniques (as well as incorporating any further useful techniques developed in \ref{task:axioms} and~\ref{task:algorithms}).
The second stage of the compilation process is to take a generic \zx term expressing a computation on idealised quantum systems, and re-write it as a \zx term representing an equivalent transformation of error-corrected qubits (\ref{task:ECC}).
As well as the \zx terms to translate, this will take as input a specification the particular error correction code or other fault-tolerance construction to apply.
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.
...
...
@@ -799,13 +790,33 @@ presentations of the Clifford+T \zx-calculus and develop strategies
for effectively simplifying \zx-diagrams. These include Knuth-Bendix
completion and theory synthesis.
In task~\ref{task:axioms}, we will extend the
\zx-calculus in two dimensions. The first is to expand into complete
\zx-calculus in two respects. The first is to expand into complete
and universal qudit variations to work effectively beyond 2-level
systems, and the second is to gain a deeper understanding of the role
played by W-type tensors as they interact with the generators of the
\zx-calculus, which are themselves of GHZ-type.
While in the early stages of the project, it will already be quite useful to study concrete diagrams of fixed size (e.g. a quantum circuit on $N$ qubits for a previously-fixed $N$), in task \ref{task:betterboxes}, we will extend \azx to support parametrised families of diagrams (e.g. quantum circuits with $N$ qubits where $N$ can vary) mirroring the control structures present in a quantum HLL. This will enable more sophisticated, generic optimisations to be run in advance of needing any particular computational procedure.
Error correction should be performed automatically. We have extensive
experience in treating error correcting codes in the \zxcalculus
Similar techniques will enable translating from ``raw'' \azx terms to
error corrected / fault-tolerant versions of the same program;
additional annotations will be added to ensure that other program
transformations do not break the fault-tolerance.
We identify two kinds of optimisation. First, generic,
model-independent optimisations work on the raw tensor network,
typically by reducing its graph complexity, or by minimising the
number of non-Clifford operations in the graph. This draws on
\ref{task:algorithms} and could be applied before the target hardwaere
is known. Second, optimisations which take into
account the resource models of a specific machine, expressed through
annotations, cf.~\ref{task:annotate2}. This might be applied before
or after layout, depending on the circumstances. Layout will be handled
in a similar way to this second kind of optimisation, generalising
from \ref{task:delft-model} and \ref{task:NQIT-model}.
Although we will provide specific modules for the tasks described above, the
\azx system is intended to extensible, so we will also publish an open
API and specification language to simplify the task of adding new
architectures and error correcting schemes to the system
(\ref{task:backendapi}).
The tasks to be performed within WP4 may be broadly described in terms of how the \azx compiler will transform \zx terms produced by the front-end to obtain instructions to be realised by a quantum computer (or software quantum simulator) at the back-end.
These stages are: (i)~an initial round of generic, hardware-independent optimisations; (ii)~application of some choice of strategy for error correction; (iii)~translation to a specialised annotation system which represents the parameters and constraints of a specific hardware implementation; and finally (iv)~another round of optimisation within the constraints imposed by the error correction and hardware models.
In addition to the development of the tools for these stages, WP4 will develop an interface for the specification of the annotation systems used in stages (iii) and~(iv) above, allowing for easy extension of the \azx compiler to arbitrary hardware systems and allowing \azx to act as a general-purpose quantum compiler.
The first stage of the compilation process represents a ``generic optimisation'' subroutine (\ref{task:basic-opt}), which may be applied to arbitrary \zx terms.
This subroutine will re-write \zx terms into ones with fewer resources in a broadly applicable sense, such as fewer total nodes or fewer nodes which realise non-Clifford transformations (for instance, corresponding to $T$ gates).
This may be developed independently of the results of WP1 or WP2 using existing techniques (as well as incorporating any further useful techniques developed in \ref{task:axioms} and~\ref{task:algorithms}).
The second stage of the compilation process is to take a generic \zx term expressing a computation on idealised quantum systems, and re-write it as a \zx term representing an equivalent transformation of error-corrected qubits (\ref{task:ECC}).
As well as the \zx terms to translate, this will take as input a specification the particular error correction code or other fault-tolerance construction to apply.
The third stage of the compilation process attempts to map a \zx term into an equivalent \zx term which closely models the constraints of a target architecture (\ref{task:runnable}).
This represents the core of the compilation process, taking \zx terms representing a procedure in an abstract model of quantum computation such as circuits or MBQC patterns (with or without error correction), and mapping them into a form which conforms to the physical constraints of a specific hardware implementation.
Particular implementations are specified by a system of annotations provided by the development environment, consisting of an ``architecture-targeted annotation'' (or ArcTAn) system.
...
...
@@ -895,8 +891,9 @@ This will involve the development of a theory of re-writing techniques developed
By performing a final round of optimisations using a theory of rewrites which apply to all ArcTAn annotation systems, we aim to make possible a reduction in the resources used in any particular hardware platform without requiring the use of bespoke techniques for each target architecture.
Annotation systems representing the hardware implementation are to be provided by the development environment, using a standardised interface.
By providing public documentation for this interface~(\ref{task:backendapi}), we enable third-party developers to extend the functionality of the \azx compiler to arbitrary platforms, thus ensuring the suitability of the \azx compiler as part of a general-purpose quantum software development platform.}
By providing public documentation for this interface~(\ref{task:backendapi}), we enable third-party developers to extend the functionality of the \azx compiler to arbitrary platforms, thus ensuring the suitability of the \azx compiler as part of a general-purpose quantum software development platform.
\benREM{Missing discussion on the hardware: T4.1 and T4.2.}
\subsection{Interdisciplinary nature}
\label{sec:interd-nature}
...
...
@@ -1340,18 +1337,16 @@ In the first instance we make contact between \zx and standard circuit and measu
%%%
%%%%%%%WP 2
%%%
\begin{WP}{Representation and Reasoning in \zx}{1M}{36M}{wp:backends}
\begin{WP}{Representation, reasoning, and resources in \zx}{1M}{36M}{wp:backends}
\WPleaderPOL
\WPeffort{0}{0}{0}{0}{0}{0}
\begin{WPaim}
We build the theoretical foundations for \zx as an IR. This includes extending the capabilities of \zx to represent universal algorithms, control flows, and \ldots . We identify and develop annotations in \zx for relevant computational resources, which will then be used for subsequent machine (in)dependent optimisation protocols.
We build the theoretical foundations for \zx as an intermediate representation. This includes extending the capabilities of \zx to represent mixed states, qudit states, and control flows. We use \zx axiomatisations and automated theorem provers to extract out post-classical computing resources, which will be used both for further optimisation work, and for characterisation of quantum algorithmic speed-up.
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:axioms}]{Beyond qubits and stabilisers
(M1--M12; Responsible: 2; Involved: 1,3,5)}{%
We will exploit recently achieved completeness results for
\zxcalculus to get both convenient and powerful presentations for
Clifford+T and fully universal families of diagrams. We will
We will exploit further the recent completeness results to give representations for mixed state qubit quantum theory. We will
extend the \textsc{zx} tensor formalism from the qubit domain to
higher dimensions.
% and exploit the translation from \textsc{zx}- to \textsc{zw}-calculus.
...
...
@@ -1364,13 +1359,15 @@ We build the theoretical foundations for \zx as an IR. This includes extending t
of diagrams, e.g. for expressing and transforming regular families
of circuits.
}
\WPtask[\label{task:resources}]{Resources
\WPtask[\label{task:resources}]{Resources and axioms
(M1--M18; Responsible: 1; Involved: 2,3,5)}{%
Placeholder for stuff that's primarily Belen's.
We will exploit the three axiom sets for Clifford, Clifford+T, and universal qubit QM,
to identify and distill specific resources that are necessary to quantum speed-up. In particular, to focus on finding multiple resource elements (rather than simply magic states), and to characterise post-classical composition as a resource.
This includes developing \zx representations of contextuality, as a possible post-classical resource.
Further placeholder for stuff that's primarily Belen's.
We will use the existing graph re-writing and automated theorem proving tools of Quantomatic and PyZX to determine parts of the re-writing process that are difficult to compute classically. This will then be used to extract candidate subroutines for sources of quantum speed-up. Along with the previous task, these will be used to develop procedures for characterising if a \zx-represented algorithm demonstrates speed-up or not.
}
\end{WPtasks}
...
...
@@ -1947,7 +1944,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.}
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={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.},
