FULLPROP.tex 155.66 KiB
\RequirePackage[l2tabu,orthodox]{nag}
\documentclass[11pt,a4paper]{article}
\usepackage{etex}
%%%% do rwd stuff %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pdfoutput=1
%\usepackage{rwd-drafting}
\usepackage[suppress]{rwd-drafting}
\input{margins.tex} % font and other formatting in here
\input{preamble.tex}
\usepackage{diagrams}
\input{figures/cnot.tex}
\begin{document}
\newcommand\projtitle{A Flexible Intermediate Representation for Quantum Software}
\newcommand\projacro{AZX}
\title{QuantERA Full Proposal}
\author{}
\date{}
\maketitle
\begin{center}
{\Huge \projacro }\\
{\LARGE \projtitle }
\end{center}
\REM{
{\Large IDEAS WHICH ARE MISSING}
\begin{itemize}
\item this is a new kind of formal verification -- ``runnable on
NQIT'' is a predicate about a program, expressed via graph matching
\item Also: it \emph{is} formal verification -- at the very least of
program equivalence
\item Such formal proofs are \emph{necessary} for quantum software due
to the enormous difficulties involved with testing it, theoretical,
practical and economic.
\end{itemize}
{\LARGE Do we actually mention that ZX knows quantum mechanics?}
}
\newpage
\REM{\textbf{Everything below this needs to fit under 4000
characters for the online submission system}}
\paragraph{Duration:} 36 months
\label{sec:duration}
\section*{Summary of the project}
\label{sec:abstract}
\REM{(publishable abstract, max. 1/2 page): Be precise and
concise. This summary will be used to select suited reviewers for
the proposal.}
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. Extant quantum
computers are not so much single devices, but instead patchworks of
components which vary greatly between implementations such as ion
traps, superconducting circuits, or quantum optical devices.
Programming such devices 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. We face a situation where the
ever-multiplying range of quantum computers has minimal software
support.
This project introduces \azx, a flexible intermediate language for
quantum computation, which removes this obstacle by providing a
common interface between the software and the hardware. This
intermediate language will be versatile enough to target a wide
variety of hardware implementations, and simple enough to support
any programming language. Further, \azx will expose a formal
algebraic structure based on an existing graphical formalism called
the \zxcalculus, which recently was proven to be complete: every equation that holds in Hilbert space QM can be derived in \zxcalculus. The latter 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 and standardise the \azx 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.
% \REM{ % OLD ABSTRACT REMOVED
% % problem to be solved
% Many current projects aim to develop a scalable quantum computer,
% using different underlying physical implementations, configured in a
% variety of architectures. Each model has it own particular
% characteristics, and each diverges from the idealised quantum
% circuit model used to describe quantum algorithms. This great
% diversity presents an obstacle to the uptake of quantum computing,
% since the programmer must work with low-level operations specific to
% one machine rather than a powerful and generic high-level
% programming language.
% % general strategy
% We will remove this obstacle by creating a flexible {\em
% intermediate representation} language for quantum software,
% together with translations from this intermediate language to a
% representative selection of scalable quantum computer architectures.
% Following the methodology used by modern compilers for classical
% software such as LLVM, the intermediate representation serves as a
% common interface between any programming language and any target
% hardware. Intermediate programs will be transformed, for example to
% optimise resource use or to add error correction.
% %\TODOb{Seems that most of this abstract is about a question, and only
% %last two lines about a candidate solution. That should be rebalanced.
% %Maybe this can instead be part of intro.}
% % specific approach
% Since the compiler must change the structure of the program without
% altering its meaning, the intermediate representation must be
% semantically well-founded and easy to reason about, and must take
% into account quantum phenomena like entanglement and no-cloning. We
% will employ a formal axiomatic system, the \zxcalculus, which
% faithfully represents quantum states and whose equational theory% justifies a wide range program transformations. In consequence, the
% optimised output program will come with a formal proof of its
% equivalence to the original high-level program.
% % expected benefits
% This project will produce a generic back-end for an optimising quantum
% compiler. Language designers can use it to generate efficient
% machine-level code for quantum algorithms. New translations from
% the intermediate representation to machine-level will be relatively
% easy to add, so new hardware can quickly run programs written in any
% high-level language.
% % By doing so, this project will offer a generic backend for a quantum
% % compiler. It will let quantum programming language designers focus
% % on the front-end part of the compiler (parsing and analysis of
% % code), and yet be able to offer efficient machine-level
% % implementation for the quantum programmers and algorithm designers
% % using their language. The chosen intermediate representation will
% % also make it easy to port the compilation chain to a new quantum
% % architecture, by concentrating on the translation of the
% % intermediate representation to the new hardware representation.
% }
\section*{Relevance to the topic addressed in the call}
\label{sec:relev-topic-addr}
\REM{(in particular specify here which part of the call text is
concerned by your project, max. 1/4 page):}
The project clearly has ``\emph{potential to initiate or foster new
lines of quantum technologies through collaborations exploring
advanced multidisciplinary science and/or cutting-edge engineering}'',
which is the overall objective of QuantERA. We specifically
address the \emph{Quantum Computation} area of the call. The
retargettable nature of the compiler supports \emph{new architectures
for quantum computation}, in particular technologically heterogeneous
implementations. The optimising aspect of the compiler will allow the
\emph{optimisation of error correction codes}, both at the
intermediate and machine level. The ability to compile multiple
high-level languages will promote the \emph{development of novel
quantum algorithms}. More generally, this project is an enabling
technology that multiplies the impact of all the target
outcomes of QuantERA, and prepares the stage for the Quantum
Technology Flagship.
\REM{interfaces between quantum computers and communication systems.???}
\newpage
\REM{
\begin{figure}
\REM{This table is actually elsewhere in the form. Included here to
make sure the names are right.}
\begin{center}
\begin{tabular}{|c|c|c|c|}\hline
Country & Institution & Group Leader & Other Personnel \\\hline
UK & University of Strathclyde & Ross Duncan & \emph{Post-doc}
\\\hline
& University of Oxford & Bob Coecke & Samson Abramsky \\
&&& Simon Benjamin \\
&&& Niel de Beaudrap\\
&&& Dominic Horsman\\
&&& Sam Staton \\
&&& Jamie Vicary\\
&&& \emph{Post-doc} \\\hline
France & Universit\'e de Lorraine & Emmanuel Jeandel & Simon Perdrix\\
&&&Beno\^it Valiron\\
&&& Renaud Vilmart\\
&&& \emph{Post-doc}\\\hline
% & CentraleSup\'elec & Beno\^it Valiron & \emph{Post-doc} \\\hline
& Bull* & Cyril Allouche & \\\hline The Netherlands & Radboud Universiteit Nijmegen & Aleks Kissinger &
Bart Jacobs\\
&&& \emph{Post-doc} \\\hline
\end{tabular}
\end{center}
\noindent * \emph{Industrial partner}
\end{figure}
}
\paragraph{Changes with respect to the pre-proposal, if any:}
\REM{The full proposal should be consistent with the pre-proposal. If
this is the case, mention it in one sentence. If not, explain and
justify the changes. If the changes involve changes in the
consortium composition, highlight them in a separate paragraph.}
Since the submission of the pre-proposal, consortium members Jeandel, Perdrix, and Vilmart have made a major breakthrough in the theoretical foundations of this project, namely proving Clifford+T completeness for the \zx-calculus. This is a very powerful result which enables us to set more ambitious goals for WP3 and WP4 than those stated in the pre-proposal.
Per EPSRC request, we have reduced the budget by 10\% in both UK sites
and by 15K EUR total in the French sites. This is made possible in
part due to the surprising result of Jeandel et
al. %: we no longer need to allocate
%resources toward proving
%completeness, as originally proposed.
We have made minor changes to the personnel of the project: Dominic
Horsman will contribute via the NQIT project at the Oxford site; at
Bull, T. Goubault de Brugi\`ere is replaced by Simon Martiel
Jean-No\"el Quintin. Neither of these changes has any budgetary
effect.
\newpage
\section{EXCELLENCE \REM{(6 pages)}}
\label{sec:overview}
\subsection{Targeted breakthrough, baseline of knowledge and skills}
\label{sec:targ-breakthr-basel}
\REM{
Describe the targeted breakthroughs of the project.
Describe the specific objectives of the project, which should be
clear, measurable, realistic and achievable within the duration of the
project.
\textbf{Describe how the science and technology contribute to the
establishment of a solid baseline of knowledge and skills for the
specific theme addressed.}
}
\paragraph{Summary: }
\label{sec:summary:-}
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.\vspace{-2mm}
\vspace{-1mm}
\cgraph[0.65]{arch-diagram.pdf}\vspace{-5mm}
\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 onthe 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.
\paragraph{Targeted breakthrough:}
\label{sec:targ-breakthr}
We will define a 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 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}.
\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.
\paragraph{Baseline of knowledge and skills:}
\label{sec:basel-knowl-skills}
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
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,
%Coecke:2009db, CDKW-lics:2012qy,
Coecke2017Picturing-Quant}. The \zxcalculus can be viewed in twodistinct 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
new possibilities for optimisation and verification of quantum
computations.
% and is complete for important subtheories such as the stablizer
% fragment \cite{1367-2630-16-9-093021} and single qubit Clifford+T
% equations \cite{Backens:2014aa}.
%\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
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}).
\[
\cnoti[0.7] \rTo^*
\cnotii[0.6] \rTo^*
\cnotiii[0.6] \rTo^*
\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.}
%%% cutting because repeated later
% It is strictly more powerful than the stabiliser
% formalism~\cite{Backens:2012fk},
%\begin{figure}[t]
% \vspace{-2mm}
% \centering
% \[
% \cnoti[0.7] \rTo^*
% \cnotii[0.6] \rTo^*
% \cnotiii[0.6] \rTo^*
% \cnotiv[0.6] \rTo^*
% %\cnotv[0.6] \rTo^* % \cnotvi[0.7]
% \]
% \vspace{-2mm}
% \caption{The \zxcalculus in action: translating from MBQC (left) to
% a quantum circuit (right)}
%\label{fig:zx-mbqc-cnot}
%\end{figure}
\paragraph{Contribution to the theme addressed}
\label{sec:contr-theme-addr}
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.
\subsection{Novelty, level of ambition and foundational character}
\label{sec:novelty-level-ambit}
\REM{Describe the advance your proposal would provide beyond the
state-of-the-art, and to what extent the proposed work is ambitious,
novel and of a foundational nature. \textbf{Your answer could refer
to the ground-breaking nature of the objectives, concepts
involved, issues and problems to be addressed, and approaches and
methods to be used.}
}
\BREM{
\begin{itemize}
\item Need to emphasise unique features in light of \liquid, which also claims compilation to hardware, circuit rewriting/optimisation, and error correction
\item \textbf{novel feature:} flexibility, via intermediate language
\item \textbf{novel feature:} formal basis (ZX-calculus, categorical semantics)
\item \textbf{novel feature:} multiple paradigms. Notably MBQC (both team members' expertise, and in methodology) and \textbf{lattice surgery} (high-level description of logical operations on error-corrected memories)
\item \textbf{foundational nature:} 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.
\end{itemize}
}
\paragraph{Novelty:}
\label{sec:novelty}
\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.
% 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.
\REM{This project rests on more than a decade of investigations into the
categorical structure of quantum mechanics. This project therefore has a uniquely
strong theoretical foundation, and provides us withinsights unavailable to other approaches.% Repeated later
}
\REM{more}
\REM{}
\REM{Formal proofs of everything. Formal basis (ZX-calculus, categorical semantics)}
\REM{Pure symbolic manipulation; no dimension explosion! (\liquid
handles up to 30 qubits -- aka 3 error corrected qubits!}
\REM{
However, as the RISC revolution in CPU design showed in the 1980s, there is no reason for
instruction sets to be optimised for human comprehension once
good compilers are available. \azx would provide a more
flexible, powerful, interface between quantum computers and the outside world.
}
\REM{
From a formal perspective, \azx could be
regarded as a formal semantics for quantum programming
languages. However, unlike other existing semantics such as the
category CPM %~\cite{cpm}
or the language of superoperators, this model
is purely algebraic, with a graph-like representation which does not involve exponentially-sized matrices. Finally, unlike
existing semantics, we believe that it is extendable to express
computations parametric on the size of the input (such as
\emph{e.g.}~parametric families of circuits).
}
\REM{Is the following foundational ?
Although not part of this proposal, the \azx approach could
open the door to using quantum simulators for some general quantum
computation tasks.}
\paragraph{Ambition:}
\label{sec:ambition}
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.
% 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
optimisation, (ii)~a~strictly more expressive superset of the existing semantics of programming languages, and (iii)~use this as an intermediate representation to provide a scalable solution for quantum software development, which is fully independent of the hardware. To our knowledge this is the first attempt of this kind: in view of the changing landscape of backends, defining a hardware-independent IR will be challenging.
}
\BREM{(The following has been moved here from the description of \ref{task:NQIT-model} to put it more approximately where it can be of use) ---
For NQIT, the most important aspect is the fact that the modular
architecture motivated using lattice surgery on surface codes for the
logical operations, and that these are in effect be red/green copies
and products. This will certainly make the ambition here much more
achievable.
Annotations for dealing with byproduct operations in real-time or
otherwise, particularly for magic states, is an early task to be dealt
with. It is possible that work on \azx\ might inform the way in which
NQIT networks its encoded memories together, if the problem of
resource management can be fruitfully solved with particular layoutsof logical qubits.
}
\REM{More here}
\paragraph{Foundational Character:}
\label{sec:foundational-nature}
\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.}
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}.
\REM{
While the \zxcalculus is
restricted to qubits, the structures it uses are totally generic
\cite{Duncan2016Interacting-Fro}, permitting \azx to handle qudits or codewords in a uniform manner.
}
\subsection{Concept and methodology}
\label{sec:concept-methodology}
\REM{
Describe and explain the overall concept and research approach
underpinning the project. Describe the main ideas, models or
assumptions involved. Identify any interdisciplinary considerations
and, where relevant, use of stakeholder knowledge.
\textbf{Describe any national or international research and innovation
activities which will be linked with the project, especially where
the outputs from these will feed into the project.}
Describe the methodology and explain its relevance to the objectives.
Describe the appropriateness of the methodology to narrow down
multiple options and to address high scientific and technological
risks.
}
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
austere theoretical foundation, without any niceties for practical
usage. The power of \azx comes from a second layer of
\emph{annotations} on the tensor graph, describing program parameters
and architectural constraints of a specific hardware configuration.
This two-level design separates the specification (graph layer) from
the implementation (annotation layer) of the program, and is the key
to achieving our goal of supporting multiple targets.
% (for ``\emph{annotated} \textsc{zx}'') % rwd - taking this because
% the previous sentence gives 3 possibilities for A... and Z and X
% 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
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 theprocess to be carried out, independent of the target platform. Many
important transformations can be performed at this platform
independent level --- without recourse to matrix representations of
the operations involved --- such as simplifying the tensor network,
reducing Clifford fragments to minimal forms, and reducing T-count.
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.
% \REM{Can do useful stuff at this level! Some optimisation; ECC
% simple generic optimisations. e.g.
% \begin{itemize}
% \item reduce T-count / gate count
% \item coalesce Cliffords
% \item Circuits: minimise depth
% \item MBQC : minimise rounds
% \end{itemize}
% }
% specifying how the tensor
% network may be realised. This consists
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
\cite{Mhalla:2008kx} to find the \emph{gflow} of a graph state; if the
state has a gflow then it supports deterministic 1-way computation
\cite{D.E.-Browne2007Generalized-Flo}. Annotating the graph with its
gflow provides guidance for a rewrite strategy which produces an
equivalent, space-optimal circuit \cite{Duncan:2010aa}.
We propose to generalise this concept to encompass other sorts of information which would inform how to transform (i.e.,~to re-write) a generic representation of a quantum computational procedure.
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
% 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
rewrites will be used to find a runnable implementation of the
abstract tensor for the target platform, and to optimise resource use.
The development
of the general theory of annotations and augmented rewrites
(\ref{task:annotate1}, \ref{task:annotate2}), algorithms for inferring
specific annotations (\ref{wp:backends}), and rewrite strategies which exploit them
(\ref{task:opt-machine}) form a major novel component of the project.%
%
% (have I implemented
% the correct process?) and layer (is the implementation
% possible/efficient/robust?). This separation
%
%
Concrete tensor networks have a fixed finite size, whereas algorithms
are described in parametric fashion, \eg varying according the
input size. To accommodate this we introduce a second class of
annotations to represent limited forms of iteration and recursion, yielding \emph{parametric} \azx terms. While the hardware-derived
annotations are inferred in a bottom-up fashion, the parametric
structure is produced top-down, based on the original HLL program. As
this information is typically erased by the circuit generation phase\cite{Alexander-S.-Green:2013fk,Cross2017Open-Quantum-As} of
compilation, we effectively move the boundary between \azx and the HLL
above the circuit-level. This is possibly the most challenging part
of the project (\ref{task:betterboxes}); however, we have experience of
similar constructs from the \texttt{quantomatic}
project~\cite{KZ:2015:aa, Kissinger2015Quantomatic:-A-}.
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}).
% 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.
% \REM{Summarise WPs in light of this setup}
% \REM{Interrelations of goals and separation of concerns}
% \REM{Risk assessment: which are easy, which are hard? Dependencies.}
\REM{WHY this is a good idea.}
%\TODOb{Nowhere it is explained what the A in AZX means.}
\BREM{
\begin{itemize}
% \item methodology centres around common language: AZX
% \item (\textbf{idea:} what about IZX, \textit{implemented} ZX?
% i.e. something more active/evocative than \textit{annotations})
% \item this has two layers (1) the ZX-graph layer, a technique for representing quantum processes, and (2) annotations which describe parameters as well as how process is implemented within a computational model
% \item (1) already done (cf. ten years of research!)
% \item (2) is guided in two ways: \textit{top-down} (capturing language features of Quipper) and \textit{bottom-up} (capturing hardware requirements)
\item a common language synchronises the project across sites, implementation details (e.g. platform, language, etc.), and goals (optimisation, EC, simulation)
\item development focuses around simple, modular tools, mitigating \textbf{risk} and increasing \textbf{agility} of the project as a whole
\item
\end{itemize}
}
\REM{
The front-end is responsible for translating a high-level programming
language to the IR. We will adapt the existing \emph{Quipper}
compiler \cite{Alexander-S.-Green:2013fk} for this purpose. % We will
% develop static analysis techniques like abstract interpretation
% \cite{Perdrix2008} or implicit computational complexity
% \cite{DALLAGO2010377} to optimise various resources. Such
% optimisations may be performed at the high-level or passed to the IR
% as annotations.
The front-end will later be adapted to generate the
parametric IR (see \ref{task:betterboxes}.)
}
\REM{These modules will be used to implement sophisticated
quantum algorithms which will serve as robust benchmarks
for the other WPs.
idea of separating program compile time from circuit compile time
(following the {\em Quipper} and {\liquid} architecture).
other objectives. Some program parameters and control flow features
of the programming language will be translated into the \azx\
representation.
}
The four major work packages of the project are structured into
various themes: the relation between \azx and high-level quantum
programming languages (\ref{wp:frontend}); diversemachine models in \azx (\ref{wp:backends}); sound theory
and algorithms for working with \azx terms (\ref{wp:theory}); and
practical compilation tasks for quantum software (\ref{wp:usefulstuff}).
\subsubsection{Programming Language Support}
\label{sec:progr-lang-supp}
% Since the advent of the ENIAC, programming language and compiler
% designers have enormously reduced the burden of transforming
% high-level algorithms into machine code. A key technique in this
% translation is to insert a lower-level \emph{intermediate
% representation} language (IR) between the human-readable program and
% the executable code. The IR form of the program can be further
% analysed and optimised before transforming to machine code.
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
classical counterparts, these HLLs are not designed to be run directly
on quantum hardware, rather their compilers typically output quantum
circuit descriptions.
Rather than designing a new programming language, we propose a quantum
IR, \azx. Unlike the languages mentioned above, \azx is not intended
to be written by humans\footnote{This said, the \zxcalculus has proved
a very useful notation for mathematical proofs.}, instead it will be
generated by a compiler front-end from programs written in existing
high-level languages. Therefore it is essential to provide a robust,
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.
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 %: this is the purpose of
(\ref{task:trans1}).
%\REM{This is aim probably too long, some of this should probably go somewhere else, and the tasks should probably be expanded?}
% As the features of \azx
% A quantum program written in one of these
% languages should ultimately be transformed into a series of low-level
% instructions for the hardware controlling a quantum device. As in the
% case of classical software,
% When formalized, IRs for quantum HLLs have so far been restricted to
% (generalization of) quantum circuits.
% In this project, we will employ
% the \azx language, an extension of the ZX calculus, as a more
% versatile and powerful IR in a quantum compilation chain.
% This architecture is the same as
% Quipper~\cite{Alexander-S.-Green:2013fk} and \liquid, except that
% those systems directly (and only) target quantum circuits rather than
% AZX.
% In this project, a HLL program will then first be turned into an
% \azx-generation phase. In this phase, various classical computation is
% carried out, as parameters are passed around, connecting together
% different program libraries and evaluating higher-order functions, but
% the quantum program is not actually run. The output of this phase is
% an \azx term, rather than the final result of the computational
% question. This \azx output, being first order and free from
% complicated library interactions, is an ideal intermediate language
% for quantum hardware, as in WP2 and WP4.
% The development of such front-ends has two main goals. First, it will
% serves as testbench to the other aspects of the project: how do the
% developed techniques scale? Concrete experiments with front-ends of
% existing HLLs (QASM \cite{Cross2017Open-Quantum-As}, \emph{Quipper}
% \cite{Alexander-S.-Green:2013fk},
% ProjectQ~\cite{Steiger2016ProjectQ:-An-Op}, \liquid) will provide
% measures of success. The second goal of this analysis is to help us
% understanding the general relationship between HLLs and \azx,
% providing a robust methodology for future quantum programming
% languages.
% An intermediate representation needs to match the need of high-level
% programs. The purpose of this work package is to ensure that all the
% features required by concrete implementations of quantum algorithms
% can be captured by \azx constructions. There will be a back-and-forth
% between this work-package and the other WPs to both strengthen the
% suitability of the \azx language as interface with HLLs, and provide a
% solid methodology for writing compilation front-ends of HLLs to \azx
% in general. For the latter, we will define an open interface to \azx,
% to permit other projects to use \azx as part of their software
% pipeline.
\subsubsection{Machines and Models}
\label{sec:machines-models}
\REM{stuff about WP 2 here}
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
equivalence. More realistic models might suffer from limitation to afixed number of qubits, a bounded total execution time, or
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.
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
into account. The ability to synthesise hardware-appropriate
implementations from abstract descriptions is one of the major novel
contributions of this project.
%
Towards this objective, in \ref{wp:backends} we model the performance
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}.
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}.
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{Representation and Reasoning in AZX}
\label{sec:repr-reas-azx}
\REM{stuff about WP 3 here}
\BREM{A suggestion: describe WP3 as a bridge between all of the other
WPs. It is unique in that every other WP either depends on or is
influenced by it}
\BREM{ RD: WP3 is the theoretical core; the basis that lets us go
beyond ad-hoc-ery and towards a genuinely reusable general purpose system.}
\BREM{Note the introduction of the `ArcTAn' acronym in the WP4 section below; this may be a helpful way to frame the overlap in activity between \ref{task:annotate1}, \ref{task:annotate2}, \ref{task:runnable}, and \ref{task:opt-machine}}
\REM{Something something Monadic Second Order logic something
something Courcelle's theorem.}
\BREM{Tasks:
\begin{itemize}
\item Reduction strategies, algorithms, and complexity
\item AZX as a programming language
\item Topological/temporal constraints
\item Fidelities and noise
\end{itemize}
}
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.
Recent breakthroughs in the theory of the \zx-calculus
\cite{Jeandel2017A-Complete-Axio,NgWang}, 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.
%
% namely the completeness theorem for Clifford+T
% \zx-diagrams~\cite{Jeandel2017A-Complete-Axio}, has shown that
% Clifford+T \zx-diagrams generalise Clifford+T quantum circuits, and
% provide a rich enough language to describe any quantum computation
% up to arbitrary precision. The completeness theorem states that,
% whenever two Clifford+T diagrams describe the same linear operator,
% then one can be transformed into the other using just a finite set
% of local, diagrammatic transformations.
%
% While a previous completeness
% result~\cite{1367-2630-16-9-093021} already showed the \zx-calculus is
% strictly more powerful than stabiliser formalism for quantum
% computation, this recent result shows it is indeed vastly more
% powerful.
%
However, completeness of the \zxcalculus is just the beginning of the
story for \azx.
%rather than the end. In particular, simply k
Knowing it is possible
\textit{in principle} to transform one computation (e.g. a quantum
circuit) into another one doesn't say anything about efficiency or our
ability to find effective optimisations. In
task~\ref{task:algorithms}, we will employ theoretical and automated
techniques drawn from rewrite theory to search for better
presentations of the Clifford+T \zx-calculus and develop strategies
for effectively simplifying \zx-diagrams. These include Knuth-Bendix
completion %, whereby terminating, non-confluent rewrite systems can be
%automatically `patched up' to produce unique normal forms
and %well as
theory synthesis. %, where redex-free graph enumeration is used to
%generate an exhaustive set of rules for simplifying all diagrams up to
%a given size.
In task~\ref{task:axioms}, we will extend the
\zx-calculus in two dimensions. 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.
Finally, we will construct a theoretical framework which mediates the
abstract rewrite theory of \zx-diagrams and real-world constraints
coming from quantum hardware. In task \ref{task:annotate1}, we will
extend the language of \azx to express topological constraints and
causal ordering. These could include a restriction to
nearest-neighbour interactions for 2-qubit operations on a fixed
lattice or enforcing a fixed ordering between two gates. We will then
develop the formal tools for rewriting \zx-diagrams in ways that
respect those constraints. Similarly, in task \ref{task:annotate2} wewill explore methods to annotate a \zx-diagram with quantitative
information such as timing, noise, or fidelity. In real-world systems, these
can vary vastly between qubits interacting in different ways
(e.g. neighbouring in ion trap vs. interactions mediated by optical
channel~\cite{PhysRevX.4.041041}) or stored in different physical
modes.
%(e.g. high-coherence/low-interaction memory modes vs.~low-coherence/high-interaction computational modes~\cite{Hyperfine}).
\REM{AK: ref \cite{Hyperfine} can go if necessary}
\subsubsection{Compiling Quantum Software with AZX}
\label{sec:comp-quant-softw}
An \azx term produced by the compiler front-end is, by design, an
abstract tensor network, perhaps annotated with some useful
information, but generally without any preconception of how it should
be executed on any particular machine. Translating such
abstractly-described procedures to code that can run on realistic
machines is a key objective for the project. WP4 is responsible for
developing the tools to do so. This work package represents the most
technically involved and multi-disciplinary component of the \azx
project, requires the integration of the theoretical work of
\ref{wp:theory} and generalisation from the specific machines
considered in \ref{wp:backends}, and will result in software forming
the basis of a general-purpose quantum compiler.
We identify three main tasks: to add suitable error protection to the
program; to optimise the program according to whichever resources are
most appropriate for the given machine; and to layout the program for
execution. Although we treat them separately, in practice these tasks
will interact in non-trivial ways, and their order need not be fixed.
Error correction should be performed automatically. We have extensive
experience in treating error correcting codes in the \zxcalculus
\cite{Duncan:2013lr,Chancellor2016Coherent-Parity,BH-2017,Garvie2017Verifying-the-S}.
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}).
\REM{
\BREM{[Remark on interaction on developing annotation systems with WP2 and WP3 as a part of warm-up activities?]}
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.
\BREM{[Link to \ref{task:annotate2}?]}
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.
ArcTAn systems will generalise the particular examples of implementation-oriented annotation systems developed in WP2, and will aim to encompass as many extant and forseeable quantum hardware platforms as possible, incorporating topological and time-ordering constraints as captured by the results of \ref{task:annotate1}.
\BREM{[Link to \ref{task:annotate2}?]}
The fourth and penultimate stage of the compilation process (prior to translation to the machine language of the target architecture) is a final round of optimisation, this time applied to \zx terms within the constraints of the specific choice of error correction strategy and machine resources specified by the input~(\ref{task:opt-machine}).
This will involve the development of a theory of re-writing techniques developed in \ref{task:annotate1} \BREM{[and \ref{task:annotate2}?]} to ArcTAn annotation systems.
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.
%\BREM{Old short version of WP4 description (to be incorporated into \S3.2):
%\begin{description}
%\item[(\ref{task:basic-opt}) Generic optimisations of \zx-terms,] using the \zxcalculus to optimise descriptions of computations at a high level, performed independently of any particular hardware implementation or approach to fault-tolerance.
%(Refer to connection to \ref{task:algorithms})
%
%\item[(\ref{task:ECC}) Application of error-correction technologies,] taking high-level \zx-terms and translating them into a form according to the constraints of an annotation system which represents a correct implementation of specific approaches to fault-tolerant quantum computation.
%
%\item[(\ref{task:runnable}) Translation of \zx-terms to target systems,] taking descriptions of procedures (with or without error correction) and translating them into a form according to the constraints of an annotation system which represents a particular hardware model.
%
%\item[(\ref{task:opt-machine}) Optimisation of \zx-terms subject to a machine model,] performing optimisations of the same sort which are envisioned by task \ref{task:basic-opt} within the confines of an annotation system for a particular hardware platform employing a particular approach to fault-tolerance.
%
%\item[(\ref{task:backendapi}) Specification of an API for back-end modules,] providing the \azx compiler with extendability to any hardware platform through a specification of the parameters of a given hardware platform.
%\end{description}}
}
\subsection{Interdisciplinary nature}
\label{sec:interd-nature}
\REM{Describe the research disciplines involved and the range of added value from interdisciplinarity, including measures for exchange, cross-fertilisation and synergy.}
As shown the schema at the beginning of \S\ref{sec:summary:-},
the ambitious vertical structure of this project requires a uniquely
diverse range of expertise: from \textbf{Software Engineering \& Formal Methods} at the high level, through \textbf{Quantum Computation} and logic at the mid-level, down to quantum \textbf{Systems Architecture} at the low-level. Just
as \azx itself is an intermediary, this project unites those working
in quantum information theory from logical and pure mathematical
perspectives with those working on practical error correction, quantum
hardware, and more generally programming language
design and system engineering. It thus provides a unique opportunity
for theoretical insight to inform future technology, and for
technological problems to drive future theory.
%Thus the project is inherently highly interdisciplinary. Our work will be informed by the physical aspects of quantum computing architectures, while offering high-level tools and methods which will be accessible to systems uses and application developers.
%Key technical inputs will draw on rewriting, compiler optimization, and architectures. We will also draw on technical work from quantum computation and information, and quantum foundations. These will be tensioned against the the need to develop well-engineered, robust and scalable tools and to address the key application issues.
%This work will therefore have numerous exciting possibilities for synergies and interactions with a number of areas within computer science and physics. By bringing advanced methods from Computer Science in rewriting, automated deduction and analysis into the realm of practical quantum error correction, quantum computational architectures and implementation it will provide a focal point where different communities can interact. More broadly, computer scientists working with related formal tools and methods will be motivated to contribute to quantum computation, while physicists working on quantum information will be exposed to advanced Computer Science methods, and learn how these can be applied in their field. The \azx formalism and its applications will be an attractive paradigm to many computer scientists, and contribute to the increasing use of diagrammatic formalisms in formal methods, software design and program analysis. Within physics, diagrammatic calculi already have significant impact in several fields, e.g. tensor networks in condensed matter physics, and diagrammatic formalisms in quantum foundations, and the project can advance this trend, providing methods which are rigorously founded and supported by sophisticated software tools.
We will promote these cross-disciplinary interactions by a number of our planned activities, including holding a summer school which will provide both introductory tutorials and more advanced material on the range of techniques and methods which will be used and developed in the project, in a form accessible to both computer scientists and physicists from a wide range of backgrounds. %This should be highly attractive to research students and early-career researchers, and help to promulgate the interdisciplinary ideas and applications which will be developed in the project within the next generation of researchers.
% While quantum technology is inherently interdisciplinary, our proposal bridges disciplines (\emph{e.g.}~formal logic and system architecture) which are normally far removed, to develop a practical software tool.
%
%The \zxcalculus was initially motivated by purely theoretical considerations.
%These included a perspective in which operations such as the controlled-NOT gate should be regarded as a composite of operations, none of which are unitary transformations on a fixed number of qubits.
%Such decompositions are not typically considered in the circuit model, but may prove useful to describe logical operations on error corrected quantum memories \cite{HFDM-2012,HND-2017}.
%The availability of software tools for such operations will inform important architectural choices to be made in major quantum technology projects in the near future.
%Conversely, the needs of those working on quantum technology projects will serve to inform quantum software tools, and the mathematical theory behind the development of those tools.
%
\BREM{
\begin{itemize}
\item everyone will claim CS meets physics here. What is unique for us? Pure mathematical/logical aspects?
\begin{itemize}
\item (Benoit proposes:) Formal methods! Nowadays nearly all
critical piece of software is backed up by formal techniques to guarantee safe execution, good properties, sound optimization,
etc. AZX aims at being a common base language for quantum
computation, with a sound semantics allowing easy resonning and
sound extensions to support existing and future needs in quantum
compilation.
\end{itemize}
\end{itemize}
}
\newpage
\section{IMPACT \REM{(3 pages)}}
\label{sec:impact-2-pages}
\subsection{Expected impacts}
\label{sec:expected-impacts}
\REM{Be specific, and provide only information that applies to the
proposal and its objectives. Wherever possible, use quantified
indicators and targets.
Describe how the project will contribute to the expected impacts (see
`Research Targeted in the Call' of the Call Announcement).
Describe the importance of the technological outcome with regard to
its transformational impact on technology and/or society.}
\BREM{These are the `expected impacts' from the Call Announcement, with my judgement on how relevant they are to us:
\begin{itemize}
\item Develop a deeper fundamental and practical understanding of systems and protocols for manipulating and exploiting quantum information; \textbf{(GOOD)}
\item Enhance the robustness and scalability of quantum information technologies in the presence of environmental decoherence, hence facilitating their real-world deployment; \textbf{(FAIR)}
\item Develop reliable technologies for the different components of quantum architectures; \textbf{(N/A)} \REM{Is this using ``technologies'' strictly in the hardware sense?''}
\item Identify new opportunities and applications fostered through quantum technologies, and the possible ways to transfer these technologies from laboratories to industries; \textbf{(GOOD)}
\item Enhance interdisciplinarity in crossing traditional boundaries between disciplines in order to enlarge the community involved in tackling these new challenges. \textbf{(GOOD)}
\end{itemize}
}
\azx significantly advances the state-of-the-art across four of the
five expected impacts.% the fifth is out of project scope.
\paragraph{Develop a deeper fundamental and practical
understanding of systems and protocols for manipulating and
exploiting quantum information ---\!\!}
This project will take practical insights into the workings of diverse quantum technologies, along with fundamental techniques in quantum information processing, and embody them as software in the \azx toolchain. By embodying this expertise in software, practitioners can employ push-button optimisations and fault-tolerant transformations of programs without a deep understanding of the underlying theoretical techniques, effectively making these techniques available to a broader audience.
% This will be available as a design and optimisation tool suite for practitioners in quantum computing, and a novel framework for understanding how information is processed in quantum protocols. \REM{This could be stronger. Push `common laguage' aspect here.}
The \azx language will connect both high-level (algorithmic) and low-level (physical) representations, enabling the specifics of individual devices to be translated into constraints on the design of protocols. For instance, causal and topological structure is a crucial restriction on what can be processed in networked computing, and incorporating this into \azx will allow novel and efficient protocol design.
The project also includes the ability to interface with current models of quantum computing (the circuit and one-way models), and will enable new hybrid procedures to be developed that include elements of both (as well as potentially new forms of information processing represented in \azx).
The result of this project will be a step-change in our ability to describe how different quantum technologies store and manipulate quantum information, and to design protocols that use their specific abilities.
% \REM{fundamental shit here?}
%\REM{
%This will also advance our understanding of how to effectively reason
%%explosive matrix representations.}
\paragraph{Enhance the robustness and scalability of quantum
information technologies in the presence of environmental
decoherence ---\!\!}
\azx will provide a robust and scalable intermediate representation
for quantum programs, which will help minimise the resource
requirements in quantum technologies. \azx is also a practical tool to manage and track the resources required to
realise operations on different hardware platforms.
The annotation layer of \azx can model environmental noise and error
rates of the target platform, allowing the compiler to make provisions to minimise
decoherence as the program runs. In particular, the annotation layer of \azx can be used for
fine-grained resource management for lower levels of error correction
as well as idealised quantum memories, allowing integration of
compilation and protection of coherence. \azx will enhance the development of error correction that is tailored to specific devices.
Individual noise models and error propagation will be encoded in the language through the annotations,
which can then be used for optimisation of error correction procedures. Using \azx as a design tool, specific error correction protocols can be developed for different devices, customised to the different noise models. These models will be flexible as the devices get larger, ensuring scalability of robust devices. Networked scalability can be optimised for, as well as different topologies, by encoding timing and spacial constraints in the language.
As \azx will be a common representation, hybrid devices can also be optimised for. Error correction or mitigation strategies can be developed across multiple devices acting in tandem.
Modelling error correction in \azx will thus enable the design of new error correction procedures, optimisation of existing ones, and give a mutually-intelligible language for error correction theorists and device technologists.
\paragraph{Identify new opportunities and applications fostered
through quantum technologies, and the possible ways to transfer
these technologies from laboratories to industries ---\!\!}
%doing cool stuff with cool stuff
The retargetable \azx system will make it easy to support new quantum
devices, thus making the latest developments
in quantum technology available to all academic and industrial users,
and maximising the return on investment in quantum computing. Our
consortium includes an industrial partner (Bull) to help ensure
the industrial relevance of our work.
We also have further industrial figures on the advisory panel.
With \azx as a common intermediate language, high-level quantum languages and
protocols can be designed without needing to know the underlying hardware. This will streamline the
production of quantum software, opening it up to individuals and companies with limited
prior knowledge of quantum computing.
Quantum hardware will also be more accessible, both in academia and industry. Individual developers will
not need to know the entire architecture, as different elements can be specified fully in \azx
and then integrated into a large or hybrid device.
This will accelerate the widespread commercial and academic development and exploitation of quantum technology.
% and programming languages
% will become more easily transferred
% accelerating the widespread exploitation of
% quantum technology.
% to different hardware platforms,
% and accessible to both academia and industry.
\paragraph{Enhance interdisciplinarity in crossing traditional
boundaries between disciplines in order to enlarge the community
involved in tackling these new challenges ---\!\!}
%The inherently interdisciplinary nature of this project will bring a larger community to bear solving problems during the lifetime of the project. The development of the \azx language and compiler stacks themselves will also open up further challenges as the project progresses (and beyond) that are accessible to broader communities.
\azx will connect the entire range of knowledge involved in building quantum technologies, from experimental and theoretical Physics, through to quantum computing theory, and on to formal methods of Computer Science. All of these are needed to develop the language and its applications. Developing \azx is a fundamentally interdisciplinary task, and the resultant language will itself be a common method of communication between different disciplines. This opens the prospect of an acceleration in the development of quantum algorithms in a way which can then be easily ported to many different hardware platforms. % that will enable them all to co-ordinate in the further development of quantum technologies.
For example, algorithm and protocol designers will not need to interface directly with quantum technologies: the \azx layer does all the compilation and optimisation necessary. This will allow the
integration of quantum computing into mainstream Computer Science, and so the easy importing of tools (for example, techniques for optimisation or verification) that have been developed over many years.
By aiding the development of intuitively accessible programming languages, \azx will also make quantum technologies accessible to a broader range of users and developers. End-users outside quantum physics and computer science will be able to build protocols for use in their own field that do not require them to understand the physical action of the hardware.
The advent of quantum computation, and the diverse set of skills needed to bring an idea from algorithm to implementation, has shown the limitations of traditional subject boundaries. The breadth of expertise of this consortium, and its thematic focus on developing a common language and methodology from quantum technologies will help overcome these limitations within the project and in the wider community.
%Quantum technologies as a field show the limitation of traditional subject boundaries. The breadth of expertise on this project shows what is needed to build these technologies, and will act as a model of an interdisciplinary project to the wider community.
% Most potential users of quantum algorithms are not experts in the
% implementation of quantum devices.
% \azx would simplify the task of designing compilers for quantum HLLs, making the development of quantum algorithms more accessible to experts in other fields.
% This opens the prospect of an acceleration in the development of quantum algorithms in a way which can then be easily ported to many different hardware platforms.
\subsection{Dissemination, exploitation of results, communication}
\label{sec:diss-expl-results}
\REM{Provide a plan for disseminating and exploiting the project results beyond the project itself.
Results include any data produced in the framework of the project. If
applicable, describe how data curation and distribution can be ensured
beyond the project duration.
Describe the proposed communication measures for promoting the project
and its findings during the period of the project. Measures should be
with clear objectives. They should be tailored to the needs of
different target audiences, including groups beyond the project's own
community.
Where relevant, include measures for public/societal engagement on
issues related to the project.
}
\BREM{
\begin{itemize}
\item OSS development and github
\item Bull
\item blog, social, blablah?
\item Close co-operation with the NQIT project, leading to immediate exploitation of results
\item what are `measures for public/societal engagement'?
\end{itemize}
}
\paragraph{Dissemination.\!\!}
\label{sec:dissemination}
The primary means of dissemination will be by publishing our results
in leading journals and conferences, with a strong preference for open access
venues. (We note that in computer science, the highest impact
publication venues are conferences with published proceedings.) We
will target:
\begin{itemize}
\item Specialist quantum information venues: \emph{Quantum Information
and Computation} (QIC), \emph{Quantum Information Processing}
(QIP), \emph{Theory of Quantum Computation} (TQC), and \emph{Quantum
Physics and Logic} (QPL).
\item Mainstream computer science venues: the \emph{Journal of the
ACM} (JACM), \emph{Logic in Computer
Science} (LiCS), \emph{Principles of Programming Languages}
(POPL), \emph{Automata, Logic and Programming} (ICALP), \emph{Tools
and Algorithms for the Construction and Analysis of Systems}
(TACAS).
\item Mainstream physics journals: \emph{Physical Review Letters} (PRL),
\emph{Physical Review A} (PRA), the \emph{New Journal of Physics} (NJP), and
\emph{Communications in Mathematical Physics} (CMP), and the recently
established open access journal \emph{Quantum}.
\end{itemize}
The consortium members have a strong record of publishing in these
leading venues. Other venues will targeted opportunistically in order
to achieve the most timely publication of our results.
We plan three annual workshops, which will
be open to any interested parties. The final workshop will include a
school aimed at PhD students and potential end-users in industry. We
allocate significant budget for student bursaries to maximise
participation.
\paragraph{Exploitation of results.\!\!}
We propose several direct and indirect routes to exploitation of our
results. Firstly, our consortium includes an industrial partner
(Bull) and members of the NQIT project (Abramsky, Benjamin, de
Beaudrap). With Bull, our work will be incorporated into state of the
art products for simulation of quantum systems. With NQIT, we will
provide a programming framework for the networked quantum computer
developed as part of that project. As part of this we will present
the project results at the semi-annual NQIT Industry Forum events andthe UK Quantum Technologies annual showcase. To further this aim, our
postdoc in Oxford will spend 10--20\% of their time working closely
with the NQIT project. In both cases, our work can be exploited
directly by end-users.
In addition, we have also recruited a board of advisers (see below)
including the European leaders in scalable quantum devices. These
experts will participate in our annual workshops to help define
requirements and ensure that our work can be used by their projects.
The DiCarlo group (Delft) and Rigetti have shown particular interest
in exploiting our work to assist with supporting the superconducting
quantum devices they are developing.
Finally, we commit to produce public APIs (see
\ref{del:frontendapi} and \ref{del:backendapi})
for the \azx system which will allow any programming language to
generate code using our system, and make it easy to add support for
future hardware targets. This will enable other projects to
integrate \azx into their system. To further advance this aim, the
software tools developed by our project will be released on an
open-source basis with a permissive license (See \S~\ref{sec:cons-agre}.)
\paragraph{Communication.\!\!}
%Beyond open access publishing and open source software,
To communicate of our work to a wider audience, and to take advantage
of wide public interest in quantum technology, we will perform a
variety of outreach activities. Firstly, we will adopt ``open
lab-book'' research, publishing work-in-progress on a project wiki,
and articles aimed at a general audience on a project
blog.\footnote{The success of \emph{Graphical linear algebra}
(\href{http://graphicallinearalgebra.net}{\color{blue} graphicallinearalgebra.net}, 217K visitors since 2015) demonstrates there is a clear audience for such works.}
To allow end-users to experiment with \azx, Bull will
provide an HPC simulator with a publicly accessible front end, which
will also be incorporated into the project website.
Beyond online self-publishing we will also pitch articles to magazines
aimed at a general audience in several languages. We will
specifically target:
\begin{itemize}
\item English: \emph{Communications of the ACM}, \emph{IEEE Computer},
\emph{Physics Today}, \emph{Nautilus}, \emph{Quanta}, \emph{Aeon},
\emph{Ars Technica}, \emph{New Scientist}.
\item French: \emph{La Recherche}, \emph{Pour la Science}, and
\emph{Interstices}.
\item Dutch: \emph{Kijk Magazine}, \emph{Quest}, and the dutch edition
of the \emph{New Scientist}.
\end{itemize}
Several of members of the consortium have had their work featured in
these publications before. In addition, the \azx system itself will
also be routinely presented in any industrial or public engagement
events which touch on the software tools used by NQIT.
% Budget
% has been allocated to maintain this service beyond the project
% time-line.
% \BREM{%
% Some vectors for dissemination as a result of collaboration with NQIT:
% Bristol quantum conference (academics e.g.\ working physicists, and industry)
% \item Any industry outreach in which NQIT demonstrates compiler / software emulation products \\ (ad hoc at the moment but likely to become more important with time; we've had four meetings with firms in June 2017 alone, and people outside of academia have already been shown ZX calculus diagrams to people working outside of academia in this context)
% An attempt to form this into prose is as follows: \par
% }
% Our results will also be communicated to other quantum information
% specialists, to industrial participants, and to the general public, as
% a result of our close cooperation with the NQIT project.
% The resources of the \azx\ project and the NQIT project will be
% complementary with respect to the development and communication of
% compiler technologies: the \azx\ project assembles a consortium with
% greater depth and breadth of expertise to the problem of compilation
% and optimisation tools, while the NQIT project has an established
% platform to reach the broader quantum information community,
% interested members of industry, and the general public.
\paragraph{Advisory Board:\!\!}
\label{sec:advsiory-board}
In order to ensure the maximum impact, and to complement the expertise
present in the consortium, we have recruited a board of
advisors who will consult with the project. The board includes
several leading European researchers working on scalable quantum
devices; their input will help ensure that our software stack is able
to support real devices, and they form a ready base of
users for the final products. The board comprises:
\begin{itemize}
\item Leonardo DiCarlo (QuTech\,/\,Delft),
\item Jonathan Pritchard (Strathclyde),
\item Peter Selinger (Dalhousie),
\item Andreas Wallraff (ETH Z\"urich),
\item Philip Walther (Vienna),
\item Will Zeng (Rigetti Quantum Computing).
\end{itemize}
Letters of support from the board members are attached at the end of
this document.
% At
% the time of writing the confirmed board members are:
% \REM{TBC: Krysta Svore (Microsoft).}
% Winfried Hensinger (Sussex), Said no.
% Simon Benjamin (NQIT / Oxford) -- on the project
% \BREM{\begin{itemize}
% \item Note the role of advisory board in ensuring relevance
% \item IR will be easy to generate -- other may write their own front end.
% \item Widening access to quantum computation
% \item Advertise our SCHOOL to industry people as well.
% \item Bull will provide a public web-accessible interface to the
% HPC simulator where people may run their programs.
% \end{itemize}}
\newpage
\section{IMPLEMENTATION}
\label{sec:impl-2-pages}
\subsection{Work plan \REM{(2 pages)}}
\label{sec:work-plan-work}
\REM{Provide a brief presentation of the overall structure of the work plan.
Clearly define the intermediate targets.
Provide a timing of the different work packages and their components
(Gantt chart or similar).
Provide a graphical representation of the work packages components
showing how they inter-relate (Pert chart or similar).
}
The work plan has four major scientific work packages, each focusing
on a different \emph{theme} within the project. The work packages
will proceed in parallel, and all will have at least some activities
throughout the length of the project. (There is also a fifth
work package grouping administrative and organisational activities.)
\begin{description}
\item[\ref{wp:frontend}] is focussed on translating from HLLs into \azx, reflecting higher level programming constructs into \azx, and
building a test suite of programs.
\item[\ref{wp:backends}] is about modelling the properties of
different machines in \azx, and translating \azx to hardware.
\item[\ref{wp:theory}] develops the theory behind \azx and algorithms
to realise the logical ideas.
\item[\ref{wp:usefulstuff}] applies these advances to the
creation of useful quantum software, specifically focusing on
optimisation and error correction.
\end{description}
Each work package is divided into more specific tasks, each of which
is designed to deliver a particular piece of the project: some are
theoretical results, some are software functions. Broadly speaking,
the tasks are sequenced in order of technical difficulty so that
experience gained on earlier tasks can be applied to the more
difficult ones. There are strong interactions between the tasks, and
early outputs of each WP will be used in later outputs of other WPs.
(Details about the tasks are found in \S~\ref{sec:work-packages}.)
\begin{figure}[th]
\centering
\makebox[\textwidth][c]{\input{ganttchart.tex}}
\caption{Approximate timings and durations of tasks (months)}
\label{fig:gantt}
\end{figure}
The project is a single integrated whole, so there are many linkages
between the work packages; these are displayed in
Figure~\ref{fig:pert}. As discussed in
\S~\ref{sec:manag-struct-milest}, only some of these linkages are true
dependencies, where later tasks rely on results of earlier ones. On the other hand, many tasks can influence and enhance each other as they run in parallel.
Our work plan consists of a balance of short tasks with concrete software deliverables (e.g. \ref{task:transQASM} and \ref{task:HPC-sim-model}) and longer term, more ambitious and open-ended tasks (e.g. \ref{task:algorithms} and \ref{task:opt-machine}) which can offer significant, but less predictable, step-changes in the state of the art.
Except for \ref{task:transQASM}, the tasks of \ref{wp:frontend} are
long and thin. That is, they are intended to work in parallel with the other WPs, with new features being integrated as they are developed.
The early tasks of \ref{wp:frontend} and \ref{wp:backends} are quite
practical and don't require much preparation to begin. They will provide
useful experience for the later tasks.
The first two tasks of \ref{wp:theory} build on a significant existing body of results and techniques for the \zx-calculus and rewrite theory in general. Hence, they can begin straight away. This will provide an ample source of theoretical work to do until the more implementation-oriented tasks \ref{task:circuit-model} and \ref{task:mbqc-model} provide enough examples and use cases to feed into tasks \ref{task:annotate1} and \ref{task:annotate2}.
The more challenging machine models of \ref{task:delft-model} and
\ref{task:NQIT-model} are scheduled to begin in parallel with the more challenging theoretical tasks in WP3, anticipating a great deal of back-and-forth interaction between these two aspects of the project.
% delayed until sufficient theory has been
% developed to attempt them.
\ref{wp:usefulstuff} requires integrating and generalising many of the
ideas of \ref{wp:backends} and \ref{wp:theory}, so it is mostly
scheduled toward the end of the project.
\begin{figure}[h]
\centering
\input{pertchart.tex}
\caption{Dependencies and interactions between tasks}
\label{fig:pert}
\end{figure}
The allocation of staff to work packages is discussed in
\S~\ref{sec:consortium-as-whole} and \S\ref{sec:descr-cons}.
However, because of the integrated nature of the project, and the high
degree of past collaboration among the consortium members, most tasks
receive attention from the personnel of several sites. This degree of
collaboration is a strong point of this project.
\newpage\subsection{Work Packages \REM{1page per WP}}
\label{sec:work-packages}
\begin{WP}{Programming language support}{1M}{36M}{wp:frontend}
\WPleaderLOR
\WPeffort{0}{7}{32}{5}{3}
\begin{WPaim}
This WP provides multiple \emph{compiler front-ends}. We design the
framework of interaction between high-level languages (HLL) and the
\azx intermediate representation. We show how to compile several
languages to \azx, and investigate efficient representations of
quantum algorithms in \azx. We also discuss how best to annotate
\azx terms to reflect high-level constructs given by the programmer,
and the possibility of reflecting \azx annotation back to the HLL.
Crucially, this WP provides a source of examples to be used in other
parts of the project. Aside from \ref{task:transQASM}, the tasks are
extended in time, absorbing features from other parts of the project
as they are ready. \end{WPaim}
\begin{WPtasks}
%
%
\WPtask[\label{task:transQASM}]{Basic compilation from QASM (M1--M6;
responsible 3; involved 2,4,5)}{%
Provide a simple compilation from quantum circuits (presented in
QASM) to \azx terms. This translation will first target the
pure \zxcalculus while the \azx language is developed. There are
several possible way of the handling of classical bits: this task
implements all of them, and their relative appropriateness will be
analysed in the context of the other WPs.
%
}
%
\WPtask[\label{task:transHLL}]{Compilation from HLL (M6--M36;
responsible 3; involved 2,4,5)}{%
Based on the expertise gained from \ref{task:transQASM}, we will
develop native\footnote{\emph{Native} here meaning ``not via a
circuit translation.''} drivers for Quipper, {\liquid}, and
possibly other languages. As well as achieving one of the key
goals of the project, this task will also make it possible to test
the {\azx} framework on real, possibly very large instances of
programs. This task will progressively incorporate new features
of the \azx language as they are developed,
especially in concert with \ref{task:betterboxes}.
%
}
%
\WPtask[\label{task:trans1}]{Open API for AZX terms (M1--M36;
responsible 3; involved 2,4,5)}{%
Develop an open API for the description of \azx terms. While
largly technical, it is nonetheless essential as it will be used
as interface to express the benchmarks of
Task~\ref{task:testBench} to feed to the other WPs. The API will
first be built upon the existing JSON representation for the
\zxcalculus. It will be expanded with the features of \azx as they
become available. This task is tightly linked with
\ref{task:betterboxes}.
%
}
%
\WPtask[\label{task:testBench}]{Open test-suite (M3--M36;
responsible 3; involved 2,4,5) }{%
Devise a test-suite of concrete instances of circuits and
algorithms to rate success of other WPs. The tests will rate
various aspects of algorithms, such as controls, manipulation of
classical wires, scalability, depth of circuits, topologies of
resources, {\em etc}. The test suite will be continually expanded
as the project progresses.
%
}
\end{WPtasks}\begin{WPdeliverables}
\WPdeliverable[\label{del:earlyapi}]{M6}{Preliminary front-end for QASM, and initial \azx API}
%
\WPdeliverable{M12}{Preliminary benchtests of circuits and algorithms}
%
\WPdeliverable{M18}{Initial front-end for Quipper -- Updated API
and test suite}
%
\WPdeliverable{M30}{Advanced front-end for Quipper and one other
HLL -- updated API}
%
\WPdeliverable[\label{del:frontendapi}]{M36}{Finalized API, test-suite and front-ends}
\end{WPdeliverables}
\end{WP}
\REM{\emph{Leader:} Valiron.
\emph{Others:} Allouche, Goubault de Brugiere, Jacobs, Marchand, Staton.}
\newpage
\begin{WP}{Machines and models}{1M}{36M}{wp:backends}
\WPleaderOxf
\WPeffort{11}{27}{12}{18}{12}
\begin{WPaim}
We produce characterisations of idealised and realistic target
architectures to guide program transformations. For each target we
will (i) Model which operations are possible on the target and what
architectural limitations are in effect; and (ii) Devise
target-appropriate annotations for \azx, and cost models to use for
optimisation. Task are sequenced in increasing sophistication.
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:circuit-model}]{Idealised quantum circuits
(M1--M9; Responsible 2; Involved: 1,3,4)}{%
Translate an \azx term to an equivalent quantum circuit with ideal
gates. This will require algorithms for discovering a suitable
causal ordering on the \azx term, and for decomposing it into
parts that represent individual gates. We will also consider
circuits with constrained width, depth and/or layout. The output
format will be QASM \cite{Cross2017Open-Quantum-As}, suitable to
run on a simulator.}
\WPtask[\label{task:mbqc-model}]{Idealised
1-Way Quantum Computation (M1--M12; Responsible 3; Involved: 1,2)}{%
Translate an \azx term to a runnable 1WQC
\cite{Raussendorf-2001} with ideal measurements and state
preparation. Since every term of the \zxcalculus can be trivially
translated to a one-way program, this task focusses on finding
\emph{deterministic} programs, subject to constraints on the size
and topology of the underlying graph states, and limits on the
number of measurement rounds. The output
language will be the Measurement Calculus \cite{DanosV:meac}.}
\WPtask[\label{task:HPC-sim-model}]{Classical HPC simulator (M9--M24;
Responsible 4; Involved: 1,3,5)}{%
Using the HPC facility provided by Bull we will
construct a high performance classical simulator for \azx
evaluation. This will combine existing techniques for the
simulation of quantum circuits with symbolic manipulation of \azx
terms and numerical tensor contraction.}
\WPtask[\label{task:delft-model}]{QuTech superconducting circuits (M13--M30 Responsible: 5;
Involved: 1,2)}{
In collaboration with the DiCarlo group (Delft/QuTech), we will design an output module which generates code for a realistic model of
superconducting quantum computers, including qubit losses and leakage, gate
timings, and circuit layout. Collaboration with Rigetti Computing is also possible at this stage. Output language to be defined in collaboration with hardware experts at Delft/Rigetti.}
\WPtask[\label{task:NQIT-model}]{NQIT networked ion traps (M13--M36 Responsible: 2;
Involved: 1,5)}{
We will model the NQIT device and extract specific annotations for
\azx that describe key elements of the architecture. This will
include qubit layout within traps, network connectivity, and timing
and fidelity of entanglement links. A suitably annotated \azx term
will then be translated to an executable sequence of hardware instructions -- output language to be defined in collaboration with
NQIT.
%
% \BREM{(Earlier ``Initial Thoughts'' moved to \S1) Design an output module which generates code for a realistic model of a hybrid system, consisting of small quantum modules (\eg,~consisting of ion traps) which can form entanglement links over a specified network of connections.
% Initial thoughts (to be massaged into something more focused)
% --- the hybrid architecture may be less important for us as
% something to emphasise; more important for us is the choice of
% logical operations on encoded memories via lattice surgery, which
% will in effect be red/green copies and products. (We are receptive
% to new results for resource optimisation at lower levels, but it
% is less clear to us how fruitful this will be.) Annotations for
% dealing with byproduct operations in real-time or otherwise,
% particularly for magic states, is an early task to be dealt
% with. It is possible that work on \azx\ might inform the way in
% which NQIT networks its encoded memories together, if the problem
% of resource management can be fruitfully solved with particular
% layouts of logical qubits.}
}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable{M12}{Module for generation of QASM code from \azx terms.}
\WPdeliverable{M15}{Module for generation of 1WQC code from \azx terms}
\WPdeliverable{M24}{Module for simulation of \azx on classical HPC
cluster.}
\WPdeliverable{M30}{Module for code generation for superconducting circuit
architectures.}
\WPdeliverable{M36}{Module for code generation for NQIT.}
\end{WPdeliverables}
\end{WP}
\REM{\emph{Leader}: Abramsky.
\emph{Others}: Allouche, Benjamin, De Beaudrap, Goubault de Brugiere,
Kissinger, Marchand, Perdrix.
}
\newpage
\begin{WP}{Representation and Reasoning in AZX}{M1}{M36}{wp:theory}
\WPleaderOxf
\WPeffort{19}{28}{20}{0}{13}
\begin{WPaim}
We build the theoretical foundations for the \azx system. We
devise novel, flexible, and powerful language constructs to
express computational and structural properties of \azx terms.
Hand-in-hand with this effort, we develop practical logical and
algorithmic techniques for transforming computations and reasoning
about their properties, to support the advanced features required
by \azx, in particular to support \ref{wp:usefulstuff}.
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:algorithms}]{Reduction strategies, algorithms,
and complexity (M1--M24; Responsible: 5; Involved: 1,2,3)}{%
Develop new strategies for simplifying \textsc{zx}-style tensor
networks and reducing to (pseudo-)normal forms, with the help of
automated techniques such as Knuth-Bendix completion and
graphical theory synthesis. Implement these strategies in
software and give bounds on computational complexity.
}
\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
extend the \textsc{zx} tensor formalism from the qubit domain to
higher dimensions.
% and exploit the translation from \textsc{zx}- to \textsc{zw}-calculus.
}
\WPtask[\label{task:betterboxes}]{Control in AZX
(M1--M18; Responsible: 1; Involved: 2,3,5)}{%
Support simple control flow at the level of \azx, making it a more suitable target for compiling from a high-level language. In
particular, add support for repetition and recursive definitions
of diagrams, e.g. for expressing and transforming regular families
of circuits.
}
\WPtask[\label{task:annotate1}]{Topological and causal constraints
(M13--M24; Responsible: 2; Involved: 1,3,5)}{%
Extend \azx language and tools to express and enforce: (1) topological
constaints, such as nearest-neighbour connectivity of qubits and
(2) causal/temporal constraints, such as sequential ordering of
measurements and classically-controlled operations.
}
\WPtask[\label{task:annotate2}]{Quantitative Properties (M13--M24;
Responsible: 2; Involved: 1,3,5)}{%
Extend \azx language and tools to account for several kinds of
numerical annotations, e.g.~timing data related to performing
operations, gate fidelities, channel fidelities, and decoherence
over time. Allow these to vary by location and develop
techniques to maximise exploitation of resources with varying
fidelities. Provide formal methods to propagate these
quantities from local to global properties.
}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable{M12}{A complete axiomatic quDit tensor language}
\WPdeliverable{M18}{\azx language constructs for basic control
flow, repetition and recursion}
\WPdeliverable{M24}{A library of general-purpose techniques and
algorithms for simplifying \azx terms}
\WPdeliverable{M24}{An extended \azx language which expresses
topological and quantitative properties, with associated
reasoning techniques}
\end{WPdeliverables}
\end{WP}
\REM{\emph{Leader:} Coecke.
\emph{Others:} de Beaudrap, Duncan, Jacobs, Jeandel, Kissinger,
Perdrix, Valiron, Vilmart.}
% in two ways:
% to describe the classical control parameters in quantum programs, and to
% accommodate annotations for machine models and cost models for optimization, bridging between %We will also further improve our understanding of the ZX-calculu
% s, aiming towards a complete set of rules, and built analogues for arbitrary dimensions.
\newpage
\begin{WP}{Compiling Quantum Software with AZX}{1M}{36M}{wp:usefulstuff}
\WPleaderNij
\WPeffort{15}{22}{18}{5}{21}
\begin{WPaim}
We will develop a range of techniques for transforming
``abstract'' \azx terms produced from a high-level program in ways
which will be required by any practical compiler. Examples include:
resource optimisation, adding error-correction, and execution
layout. The final result will be a ``practical'' \azx term which
can be handed off to an appropriate code generator. These tasks
represent the fusion of the theoretical work of
\ref{wp:theory} and the study of real machines in
\ref{wp:backends}, and make full use of the annotation system of \azx.
% procedures to translate a ``logical'' (language and
% platform-independent) \azx representation of a program, and
% produce a robust ``practical'' \azx representation which takes
% into account (i)~constraints imposed by specific error correction
% techniques, and (ii)~optimisations to reduce the resources
% required in a particular setting, using the annotation system for
% \zx terms.
\end{WPaim}
\begin{WPtasks} \WPtask[\label{task:basic-opt}]{Generic optimisations of ZX-terms
(M12--M24; Responsible: 3; Involved: 1,4,5)}{%
Use the results of task~\ref{task:algorithms} to develop
procedures to optimise \zx-terms, in a way which is applicable
for families of circuits (e.g.~Clifford, Clifford+T, CNOT+T,
...) as well as measurement-based quantum computations,
independently of any particular hardware implementation or
approach to fault-tolerance and minimising different possible
metrics (such as total size, tree-width, or number of
non-Clifford subterms such as T-gates).
% \BREM{
% %Perform generic optimisations that are independent of specific
% %annotations or machine model.
% Translate the results from task \ref{task:algorithms} into practical optimisation techniques for families of circuits (e.g.~Clifford, Clifford+T, CNOT+T, ...) as well as measurement-based quantum computations. Produce optimised computations that will serve as the inputs of the various model and annotation dependent transformations. Among the possible optimisation one can reduce the size of the AZX terms, but also its tree-width, or the size of the non Clifford subterms (similar to reduce the T-gate count for quantum circuits).}
% %For example: gate count ; ZX- Normal form ;
% % minimisation.
%%%% \REM{Distinguish the latter ideas from WP3 stuff somehow?}
}
%%
\WPtask[\label{task:ECC}]{Application of Error-Correction
(M1--M24; Responsible: 5; Involved: 1,2)}{%
Develop algorithms which rewrite abstract tensor networks to
equivalent tensors in codeword space of a chosen
error-correcting code. This may be combined with additional
constraints from the annotation system, representing the
implementation of a specific approach to fault-tolerant
quantum computation, which is provided by the development
environment.
%\BREM{
% Develop a specification system for constraints of fault-tolerant realisations of computations, in order to specify how to transform a ``logical'' \azx term to a fault-tolerant version of the same program in a specified error correcting code/scheme.}
}
%%%
%% \WPtask[\label{task:compile}]{ (M18--M24; Responsible: 5; Involved: 1,2,?)}{%
%% Design algorithms to compile from an abstract \azx\ representation of a program to one which conforms to the constraints of a particular system of annotations (e.g.~specifying a particular error correction technology or hardware platform).
%% }
%%%
\WPtask[\label{task:runnable}]{Formatting for target systems
(M15--M30; Responsible: 2; Involved: 1,3,5)}{%
Develop algorithms which, given a collection of constraints
representing a machine model
(c.f.~\ref{task:annotate1}, \ref{task:annotate2}), re-writes \azx terms
to a form which can be executed on that machine model.
%\BREM{ Develop a specification system for the operations and constraints of a hardware system, in order to specify how to transform a ``logical'' \azx term to a procedure to realise that transformation on a specific machine.}
}
%%
\WPtask[\label{task:opt-machine}]{Model-guided optimisation
(M21--M36; Responsible: 5; Involved: 1,2,3)}{%
Develop procedures to optimise \zx-terms subject to a machine
model, within the confines of
an annotation system for a particular hardware platform
employing a particular approach to fault-tolerance, informed by
techniques from \ref{task:annotate1} and~\ref{task:annotate2}.
%\BREM{ Develop software to perform optimisations of \azx terms subject to the constraints of a hardware specification and error correction technology (e.g.~based on timing, gate set/fidelity, and topological constraints).}
}
\WPtask[\label{task:backendapi}]{Back-end API (M24--M36 Responsible: 5; Involved: 1,2,3,4)}{%
Open specification of an API for back-end modules, facilitating third-party development of specifications of target architectures, providing the \azx compiler with extendability to arbitrary hardware platforms.
% \BREM{
% Define open API for back-end modules.}
}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable{M24}{Algorithms and heuristics for optimising \azx
terms, including minimisation of T gate count}
\WPdeliverable{M24}{Routines for adding error-correction to \azx
programs}
\WPdeliverable{M30}{General purpose layout engine}
\WPdeliverable{M36}{Optimising compiler for \azx, suitable for compiling to NQIT and/or QuTech architecture}
\WPdeliverable[\label{del:backendapi}]{M36}{API for back-end
modules, including specification language for architectures.} \end{WPdeliverables}
\end{WP}
\REM{\emph{Leader:} Kissinger.
\emph{Others:} Abramsky, de Beaudrap, Duncan, Jeandel, Perdrix,
Staton, Vilmart.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% WP admin and comms
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{WP}{Administation and Communications}{M1}{M36}{wp:admin}
\WPleaderStrath
\WPeffort{3}{3}{2}{1}{2}
\begin{WPaim}
This work package collects general administrative activities and
the organisation of the project meetings. All meetings will be
organised as open scientific workshops, co-located where possible
with a relevant conference.
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:admin}]{Project administration (M1--M36;
responsible 1; involved 2,3,4,5)}{Global administration and
project coordination.}
\WPtask[\label{task:website}]{Creation and maintenance of project
website (M1--M36; responsible 1; involved 2,3,4,5)}{As part of
our commitment to open science, we will create and maintain a
unified website for the project, including latest scientific
works, downloadable software, end-user documentation, and
popularising articles aimed at a general audience.}
\WPtask[\label{task:wkshopone}]{Kick off meeting (M1--M2;
responsible 2; involved 1)}{Project workshop to define
state of the art, establish plans for the next year.}
\WPtask[\label{task:wkshoptwo}]{Midpoint meeting (M17--M18;
responsible 5; involved 1)}{Project workshop to disseminate
initial results, evaluate progress and determine next steps.}
\WPtask[\label{task:wkshopthree}]{Final meeting and school (M33--M36;
responsible 3; involved 1,5)}{Project workshop and school to disseminate
project results.}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable{M2}{Website up and running}
\WPdeliverable{M3}{First workshop}
\WPdeliverable{M18}{Second workshop}
\WPdeliverable{M36}{Final workshop and school}
\end{WPdeliverables}
\end{WP}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\input{old-wps.tex}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
\paragraph{Work package overview}
\label{sec:work-pack-overv}
\begin{center}
\begin{tabular}{|p{0.2\textwidth}|c|c|c|c|c|c|}
\hline
\textbf{Partner}
& \ref{wp:frontend}
& \ref{wp:backends}
& \ref{wp:theory}
& \ref{wp:usefulstuff}
& \ref{wp:admin}
& \textbf{TOTAL} \\\hline
1. Strathclyde & 0 & 11 & 19 & 15 & 3 & 48 \\\hline
2. Oxford & 7 & 27 & 28 & 22 & 3 & 87 \\\hline3. LORIA & 32 & 12 & 20 & 18 & 2 & 84 \\\hline
4. Bull & 5 & 18 & 0 & 5 & 1 & 29 \\\hline
5. Nijmegen & 3 & 12 & 13 & 21 & 2 & 51 \\\hline
\textbf{TOTAL} & 47 & 83 & 83 & 75 & 11 & 299 \\\hline
\end{tabular}
\end{center}
\REM{(total effort per WP and partner in person.months)}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
\subsection{Management structure, milestones, risk assessment \REM{(2 pages)}}
\label{sec:manag-struct-milest}
\REM{Describe the organisational structure and the decision-making.
\textbf{including a list of milestones (template provided). A
milestone is a major and visible achievement. It should be SMART:
Specific, Measurable, Attainable, Relevant, Time-bound.}
Explain why the organisational structure and decision-making
mechanisms are appropriate to the complexity and scale of the
project.}
\paragraph{Coordinator}
\label{sec:overall}
Coordination between sites and between work packages will be overseen
by R. Duncan at the Strathclyde site, which will also handle the
overall administration of the project.
\paragraph{Sites}
\label{sec:sites}
The project will be managed by a senior scientist from each site:
C. Allouche (Bull), B. Coecke (Oxford), R. Duncan (Strathclyde),
E. Jeandel (LORIA), and A. Kissinger (Nijmegen). They will track
global progress to ensure milestones are reached, and facilitate
collaboration across tasks at their individual sites. They will be in close contact throughout the project to assure coherence and concurrence of the activities at the different sites.
\paragraph{Work packages}
\label{sec:work-packages-1}
Each work package will be lead by a responsible PI who will coordinate
research activity between sites to ensure that deliverables are met,
achieve WP-specific objectives, and organise collaboration meetings as
needed.
\textbf{\ref{wp:frontend}}: B. Valiron (LORIA),
\textbf{\ref{wp:backends}}: S. Abramsky (Oxford),
\textbf{\ref{wp:theory}}: B. Coecke (Oxford),
\textbf{\ref{wp:usefulstuff}}: A. Kissinger (Nijmegen),
\textbf{\ref{wp:admin}}: R. Duncan (Strathclyde).
\paragraph{Software Integration}
\label{sec:software-integration}
Responsibility for the overall software architecture and integration
of components will be shared between C.~Allouche (Bull), A.~Kissinger
(Nijmegen), and
B.~Valiron (LRI), who make the technical decisions regarding
interfacing of modules and global design.
\paragraph{Monitoring and advisory board}
\label{sec:monit-advis-board}
Every six months there will be a meeting of both the work package leaders
and the site leaders, either electronically (\eg via Skype) or at a
project event. At these meetings progress towards research objectives
will be evaluated, and any new opportunities will also be discussed. These
meetings will be organised by the coordinator.
To assist in monitoring and evaluating progress, we have recruited a
board of external advisors who are both experts and potential
end-users of the project. The advisory board consists of:
Leonardo DiCarlo (QuTech\,/\,Delft University of Technology),
Jonathan Pritchard (University of Strathclyde),
Peter Selinger (Dalhousie University),
Andreas Wallraff (ETH Z\"urich),
Philip Walther (University of Vienna), and
Will Zeng (Rigetti Computing).
The entire project and advisory board (see \S\ref{sec:impact-2-pages})
will meet once a year to evaluate progress, set priorities, and plan
next steps.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{List of milestones}
\label{sec:list-milestones}
The milestones of the project are conceptually simple: at each
milestone we will deliver a functioning piece of software. With each
milestone, we add more, and more advanced, functionality. By
delivering the software incrementally, we follow best practice in the
industry: by regularly integrating parts from all work packages, we
reduce risk and improve communication across the consortium.
\begin{center}
\makebox[\textwidth][c]{
\begin{tabular}{|c|c|c|l|}
\textbf{Milestone} &
\textbf{Delivery Month} &
\textbf{WP involved} &
\textbf{Title} \\\hline
%
\ms \label{ms:qasmqasm}&
9 &
\ref{wp:frontend},\ref{wp:backends}, &
Minimal QASM$\rightarrow$QASM circuit optimiser\\\hline
%
\ms \label{ms:quippermbqc}&
18&
All&
Quipper$\to$MBQC compilation pipeline\\\hline
%
\ms \label{ms:simbackend}&
24&
All&
Simulator back-end with parametric \azx support\\\hline
%
\ms \label{ms:delftbackend}&
30&
All&
Integrate Delft back-end\\\hline
%
\ms \label{ms:nqitbackend}&
36&
All&
Integrate NQIT back end\\\hline
\end{tabular}}
\end{center}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{Critical risks for implementation}
\label{sec:crit-risks-impl}
\REM{Describe any critical risks, relating to project implementation, that
the stated project's objectives may not be achieved. Detail any risk
mitigation measures.\textbf{Please provide a table with critical risks identified and mitigating actions (template provided).}
}
The project is overall quite high-risk, in the sense that what we
propose is in the most part entirely novel, and might fail. The
rewards for success would be correspondingly great. However, we have
designed the project to survive the failure of may (or even most) of
its tasks and still deliver value.
We mix low and high risk activities. Success in low
risk activities (\ref{task:trans1}, \ref{task:basic-opt}, \ref{task:ECC},
%\ref{task:axioms}, THIS IS NOT REAALY LOW RISK
\ref{task:circuit-model}, \ref{task:mbqc-model})
will still deliver significant progress towards our overall objective.
\ref{wp:backends} is the most critical; here we mitigate the risk by
(i) developing experience on easier objectives before addressing more
demanding ones and (ii) consulting our board of advisors to foresee
problems. Due to its high dependence on other tasks, we consider
\ref{wp:usefulstuff} to be highest risk.
\begin{center}
\begin{tabular}{|p{0.25\textwidth}|c|c|p{0.4\textwidth}|}
\textbf{Description of risk}
& \textbf{Likelihood}
& \textbf{WPs involved}
& \textbf{Proposed mitigation measures}\\\hline
%
Can't hire suitable post-docs&
Low&
All&
We have already identified several suitable candidates for each role.
\\\hline
%
NQIT or Delft machine info unavailable or not detailed enough&
Low&
\ref{wp:backends}&
(i) We have members of the consortium from NQIT, and letters of
support from DiCarlo who agrees to help. (ii) We can approach other
members of our board of advisors, or other friendly
experimentalists. (iii) We can target an more abstract model of the
machine \\\hline
%
Some desired technique or algorithm isn't found&
High&
All&
All tasks where this is a risk have been structured as a collection of
related goals; if some part doesn't succeed then the finished system
will be will have fewer features, or worse performance. However it's
very unlikely that an entire task will fail in a way that jeopardises
the project. \\\hline
%
Software integration issues&
Medium&
All&
(i) We will establish a common API in \ref{del:earlyapi} to allow
loose coupling of the software components (ii) We appoint the most
experienced software developers in the consortium (Allouche,
Kissinger, Valiron) to act as ``integration triumvirate'' and ensure
the global design is good. (iii) As noted above, we will integrate
often and deliver new features more than once a year.
\\\hline
\end{tabular}
\end{center}
\newpage
\subsection{Consortium as a whole} %\REM{(1 page)}
\label{sec:consortium-as-whole}
%%\REM{The individual members are described in section 3.5, there is no
% need to repeat that information there.
%Describe the consortium. How will it match the project's objectives
%and bring together the necessary expertise? How do the members
%complement one another?
%In what way does each of them contribute to the project? Show that
%each has a valid role and adequate resources in the project to fulfil
%that role.
%If applicable, describe the industrial/commercial involvement in the
%project and explain why this is consistent with and will help to
%achieve the specific measures which are proposed for exploitation of
%the results of the project.
%}
The members of the consortium are chosen to provide the best
combination of skills to deliver this project, having been the pioneers of the fields that provide the foundations for this project, namely the invention of \zxcalculus\ and its further development, and also having developed applications of \zxcalculus to quantum technologies. Many members also have a long history of collaboration. They also contributed greatly to community building. Several members are part of are part of the NQIT Quantum Technologies Hub.\footnote{nqit.ox.ac.uk} We now provide details on each of these.
Expertise on the
theoretical aspects underpinning the project is provided by the project leader Duncan and
Oxford site leader Coecke who jointly invented the \zxcalculus\ \cite{Coecke:2009aa}. Kissinger,
Perdrix, Horsman and De Beaudrap and many of their students are experts in its further development and
use, for example in translation between different computational models \cite{Duncan:2010aa, Horsman:2011lr}, error-correction \cite{Chancellor2016Coherent-Parity} and lattice surgery \cite{BH-2017}. Abramsky and Coecke are pioneers of high-level methods for
quantum computing more generally. Duncan, Kissinger and Vicary have pioneered automation of diagrammatic reasoning ({\tt quantomatic} and {\tt Globular} respectively), which also will play a key role in this project.
We include pioneers in quantum
programming languages (Valiron) and important contributors to the
theory of MBQC (Perdrix, de Beaudrap, Benjamin, and Duncan) and
quantum circuits (Jeandel). The consortium includes experts in
classical simulation (Allouche), quantum error correction (Horsman, Benjamin), and in quantum architecture (Benjamin,
de Beaudrap), whose expertise is bolstered by the members of our
world-leading advisory board.
We include experienced co-ordinators of
large multi-site projects (Abramsky, Benjamin, Coecke, Jacobs), and in particular, Benjamin and Coecke have led large-scale project in quantum computing.
Of utter importance is the alignment with Networked Quantum Information Technologies Hub (NQIT) at the Oxford site, which means that several members of the consortium have already direct expertise with interacting with quantum hardware (Benjamin, de Beaudrap, Horsman). The NQIT is the largest of the four Hubs in the UK National Quantum Technology Programme, a 270 GBP million investment by the UK government to establish a quantum technology industry in the UK. %We are working towards building a quantum computer demonstrator, the Q20:20 engine, which demonstrates a networked, hybrid light-matter approach to quantum information processing.
Concretely, the most important aspect is the fact that the modular architecture motivated using lattice surgery on surface codes for the logical operations, and that these are in effect \zx-operations \cite{{BH-2017}}. This will certainly make the ambition here much more achievable.
\REM{From cyril to address industrial/commericial}
Bull brings expertise in high performance simulation as well as
industrial guidances in software. \REM{more}
The consortium has also been instrumental in community building, for example with the QPL conference series which now attracts well over 100 participants every year and approx.~75 paper submissions on foundational and structural research in the area of quantum computing. It also has organised several schools e.g.~the QiCS School\footnote{www.cs.ox.ac.uk/people/bob.coecke/QICS$\underline{\ }$School.html} and the CAP Spring School,\footnote{www.cs.ox.ac.uk/ss2014/} and a substantial talks archive is maintained.\footnote{www.youtube.com/user/OxfordQuantumVideo}
\newpage
\subsection{Description of the consortium \REM{(1 page each)}}
\label{sec:descr-cons}
\REM{Describe expertise and role in the project for each partner
(templates provided). The information provided here will be used to
judge the operational capacity. Use the following templates for the
coordinator, the other partners requesting funding, and partners not
requesting funding if any. If the project relies on input to be
provided by a third party, append a letter of commitment at the end
of the proposal}
%%%% Strathclyde
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 1} & University of Strathclyde\\
Project Coordinator & Department of Computer and Information
Sciences
\end{tabular}
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Expertise:} Strathclyde University is one of the UK's leading technological universities, and is a member of all four of
the UK's Quantum Technology hubs, collecting world leading
expertise in all areas of quantum information. In the Computer
and Information Science department, the Mathematically Structured
Programming group contains internationally recognised leaders in
the areas of programming language design and implementation (Conor
McBride, Robert Atkey) and in categorical semantics (Neil Ghani,
Clemens Kupke). In the Physics department, which was ranked No.~1
in the UK in REF 2014, the Optics Division contains numerous
leading academics and researchers across all areas of theoretical
and experimental quantum technology, including Andrew Daley, John
Jeffers, Stefan Kuhr, Daniel Oi, Marco Piani, Jonathan Pritchard,
and Luca Tagliacozzo. This unique range of expertise across all
areas of project the makes Strathclyde an ideal site to host an
interdisciplinary project like \azx.
\textbf{\dr Ross Duncan} is Lecturer in Computer and Information
Sciences, having previously held personal research awards as
Charg\'e de Recherche (Universit\'e Libre de Bruxelles) and
\textsc{epsrc} Postdoctoral Fellow (University of Oxford). He is
the co-inventor of the \zxcalculus (with B. Coecke)
(1), and made key contributions to its theory
(2,3) and its
application to quantum computation
(4). He initiated the %Duncan:2012uq
\texttt{Quantomatic}
project\footnote{\url{http://quantomatic.github.io}} and pioneered
its use for the formal verification of quantum error correcting
codes (5). He has % Duncan:2013lr,
organised many major events, most recently \emph{Quantum Physics
and Logic 2016}, and is co-organiser of the workshop series
\emph{Quantum Information Scotland}, and \emph{Categories Logic
and Physics}.
\textit{\color{gray} \textbf{Publications:} (1) B. Coecke and ---. Interacting quantum observables: Categorical algebra and
diagrammatics. New J. Phys, 13(043016), 2011. (2) --- and K. Dunne. Interacting Frobenius algebras are Hopf. In LiCS 2016, ACM Transactions, 2016. (3) Bob Coecke, ---, Aleks Kissinger, and Quanlong Wang. Strong complementarity
and non-locality in categorical quantum mechanics. LiCS 2012. IEEE Computer Society Press, 2012. (4) --- and Simon Perdrix. Rewriting measurement-based quantum computations with generalised flow. In ICALP 2010, Springer LNCS 6199. (5) Liam Garvie and ---. Verifying the smallest interesting colour code with quantomatic. In Proceedings of QPL 2017, to appear.}
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Role in Project:}
As the coordinating site, Strathclyde will handle the overall
management of the project. With expertise in the \zxcalculus, and
graphical rewriting generally, Duncan will be involved in all the
work packages, especially \ref{wp:theory}, and tasks
\ref{task:mbqc-model} and \ref{task:ECC}. The postdoc employed at
Strathclyde will focus on \ref{wp:theory} (15 months),
\ref{wp:usefulstuff} (12 months) and \ref{wp:backends} (9 months).
\end{minipage}
}
\newpage
%%%% Oxford
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 2} & University of Oxford\\
& Department of Computer Science
\end{tabular}
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Expertise:} The now well over 50 members Quantum Group at the Department of Computer Science, founded and led by Abramsky and Coecke has been the world-leading group in the development of high-level computer science methods for quantum computing. It is also the birthplace of \zxcalculus, where most of the completeness result where proven, and where {\tt quantomatic} was mostly developed. Previously they coordinated the FP6 FET Open STREP QICS. The group is part of the NQIT Quantum Technologies Hub and has hosted 8 long-term EPSRC fellowships in the area of Quantum Computing. The Computer Science Department at Oxford is currently ranked within the world top 3.
% \REM{blah blah blah blah}
% \REM{Expertise of the organisation related to the project
% objectives. For the principal investigators give a brief CV,
% including gender, highlighting research experience; and list up
% 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.
\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.}
\textbf{Prof.\ Samson Abramsky} is Christopher Strachey Professor of Computing and a Fellow of the Royal Society. He pioneered high-level methods for quantum computing (see (1) above). He received the IEEE LiCS test of time award, is a fellow of the ACM for his pioneering work in computing and was awarded the BCS Lovelace Medal in 2013.
\textbf{Prof.\ Simon Benjamin} is Professor of Quantum Technologies and Associate Director and head of the ``Architectures'' WP of the NQIT Quantum Technologies Hub. He is an expert in design and architecture of quantum hardware.
%, that is tolerant of the imperfections which first generation quantum technologies will inevitably have.
\textit{\color{gray} \textbf{Publications:} (1) Architectures and materials for robust and scalable quantum technologies, Nature Comm.~4, 1756. (2) N. H. Nickerson, J. F. Fitzsimons, and ---. Freely scalable quantum technologies using cells of 5-to-50 qubits with very lossy and noisy photonic links. Phys. Rev. X, 4:041041, 2014.}
\textbf{Dr.\ Sam Staton} is Associate Professor and Royal Society University Research Fellow specialised in programming languages, and has expertise in quantum programming languages.
\textbf{Dr.\ Jamie Vicary} is a Senior Research Fellow specialised in graphical reasoning and automation thereof, in particular having produced the Globular software, an online proof assistant for higher-dimensional rewriting (\href{http://globular.science}{\color{blue} http://globular.science}).
\textbf{Dr.\ Dominic Horsman} is a visiting researcher at Oxford and co-inventor of the well-known lattice surgury technique for fault-tolerant computation. He has contributed greatly to applications of \zx-calculus, including the study of non-circuit quantum computational models, error-correction, and lattice surgery. \textit{\color{gray} \textbf{Publications:} (1) Surface code quantum computing by lattice surgery. ---, Fowler, Devitt, Van Meter New Journal of Physics 14 (12), 123011.} \textbf{Dr.\ Niel de Beaudrap} is a post-doctoral researcher involved in the NQIT project. He developed the first efficient algorithms to recover annotation systems to re-write MBQC procedures to the unitary circuit model. \textit{\color{gray} \textbf{Publications:} (1)~---\,. Finding flows in the one-way measurement model. Phys.\,Rev.\,A~77 (022328), 2008.}
% (2) Horsman and de Beaudrap. The ZX calculus is a language for surface code lattice surgery. QPL 2017, to appear. (3) de Beaudrap. Finding flows in the one-way measurement model. Phys.\,Rev.\,A~77 (022328), 2008.
%(2) ---. Quantum picturalism for topological cluster-state computing. New J. Phys., 13(095011), 2011. (3) N. Chancellor, A. Kissinger, S. Zohren, and ---. Coherent parity check construction for quantum error correction. arXiv:1611.08012, 2016. }
%\vspace{1mm}
\hrulefill\vspace{1mm}
\textbf{Role in Project:}
As the group where \zxcalculus\ originated \cite{Coecke:2009aa}, Oxford will continue the fundamental further development of the calculus. Oxford is also the central institution in the NQIT project, which is the largest national quantum computation hardware project in the United Kingdom.
The participation of researchers involved with NQIT, and their
interaction with quantum technologies specialists in Oxford and
elsewhere in Europe, will bring to the \azx project a wealth of
expertise in quantum hardware technology projects. The Oxford postdoc
will split their time equally between
\ref{wp:backends}, \ref{wp:theory}, and \ref{wp:usefulstuff},
including spending 10--20\% of their time working closely with
the NQIT project.
\end{minipage}
}
\newpage
%%%% LORIA + LRI
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 3} & Universit\'e de Lorraine / CNRS / INRIA\\
& LORIA (UMR 7503) \\
& LRI (UMR 8623) ({\small Universit\'e Paris-Sud / CNRS })
\end{tabular}
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Expertise:}
LORIA (UMR 7503) is a research unit common to the CNRS, the University of Lorraine and Inria. % -- is the French acronym for the "Lorraine Research Laboratory in Computer Science and its Applications".
Its missions mainly deal with fundamental and applied research in computer sciences. Bolstered by the 500 people working in the lab, LORIA is today one of the biggest research units in Lorraine, and one of the biggest computer science labs in France.
The Inria project team Carte, led by Prof. Emmanuel Jeandel is expert in models of quantum computation, quantum information theory and in particular \zx-calculus.
% Beno\^it Valiron (Assistant Prof. CentraleSup\'elec / LRI) will be associated with
%new CR1
% \REM{blah blah blah blah}
% \REM{Expertise of the organisation related to the project
% objectives. For the principal investigators give a brief CV,
% including gender, highlighting research experience; and list up
% to 5 relevant publications, and/or products, services
% (incl. widely-used datasets or software), or other achievements
% relevant to the call content. }
\textbf{Emmanuel Jeandel} is Professor at Universit\'e de
Lorraine, leader of the Inria project team Carte. He did a PhD in
quantum computing, he is also an expert in dynamical systems (tiling, cellular automata). He contributed to the development of the \zx-calculus (2) %(cyclotomic supplementarity)
and, together with Simon Perdrix and Renaud Vilmart, also at LORIA, they recently proved the completeness of the \zx-calculus for a universal Clifford+T fragment of quantum mechanics (3).
\textit{\color{gray} \textbf{Publications:} (1) ---. Universality in Quantum Computation. In ICALP 2004, Springer LNCS 3142. (2) ---, S. Perdrix, R. Vilmart, and Q. Wang. ZX-calculus: Cyclotomic supplementarity and incompleteness for Clifford+T quantum mechanics. MFCS 2017. (3) ---, S. Perdrix, and R. Vilmart. A complete axiomatisation of the ZX-calculus for Clifford+T quantum mechanics. arXiv:1705.11151, 2017.}
%\medskip
\textbf{Simon Perdrix} is researcher at CNRS (CR1), having previously held positions at LIG (Grenoble) as a charge de recherche, and at OUCS (Oxford), LFCS (Edinburgh) and PPS (Paris) as Postdoc. He is an expert of \zx-calculus introducing several new axioms to the language (1,2,3). He is also an expert of measurement-based quantum computing, introducing in particular a graphical characterisation of determinism in the model (4,5). He leads the Quantum Computation French network (GT IQ at CNRS GdR IM) and is board of the CNRS Quantum Technology network (GdR IQFA). %He has been PI of several projects (PEPS, Region Lorraine), and led work-packages in ANR and EU STREP projects. In 2016, he has been elected scientific secretary of section 6 at CoNRS. Section 6 is in charge, among other expertise duties, of hiring, promoting, and evaluating CNRS researchers in computer science.
\textit{\color{gray} \textbf{Publications:} (1) R. Duncan and ---. Graph states and the necessity of Euler decomposition. In CiE 2009, Springer LNCS 5635. (2) --- and Q. Wang. Supplementarity is Necessary for Quantum Diagram Reasoning. In MFCS 2016. LIPIcs, Dagstuhl, Germany, 2016. (3) R. Duncan and ---. Rewriting measurement-based quantum computations with generalised flow. In ICALP 2010, Springer LNCS 6199. (4) D. E. Browne, E. Kashefi, M. Mhalla, and ---. Generalized flow and determinism in measurement-based quantum computation. New J. Phys, 9(250), 2007. (5) M. Mhalla and ---. Finding optimal flows efficiently. In Automata, Languages and Programming, In ICALP 2008, Springer LNCS 5125.}
%\medskip
% \textbf{Beno\^it Valiron} (Assistant Prof. CentraleSup\'elec) obtained his Ph.D. In Mathematics at the University of Ottawa (Canada) in 2008. He is currently assistant professor at CentraleSup\'elec and researcher at LRI (laboratoire de recherche en informatique), Orsay. His research topics on interests include quantum computation, semantics of programming languages and models of computations. %He authored 8 journal articles, 1 book chapter and 11 international workshop and conference papers. He is currently co-supervising 1 Ph.D. Student.
\textbf{Beno\^it
Valiron} (Assistant Prof. CentraleSup\'elec) from LRI (UMR 8623)
is also included within the LORIA site.
He obtained his Ph.D. In Mathematics at the University of Ottawa (Canada) in 2008. He is currently assistant professor at CentraleSup\'elec and researcher at LRI (laboratoire de recherche en informatique), Orsay. His research topics on interests include quantum computation, semantics of programming languages and models of computations, he is in particular co-inventor of the Quipper language. %He authored 8 journal articles, 1 book chapter and 11 international workshop and conference papers. He is currently co-supervising 1 Ph.D. Student.
\textit{\color{gray} \textbf{Publications:} (1) A. S. Green, P. L. Lumsdaine, N. J. Ross, P. Selinger, and ---. Quipper: A scalable quantum programming language. PLDI 2013.
(2) A. Scherer, ---, S.-C. Mau, Scott Alexander, E. van den Berg and T. E. Chapuran. Concrete resource analysis of the quantum linear-system algorithm used to compute the electromagnetic scattering cross section of a 2D target. Quantum Information Processing 16:60, 2017
(3) ---, N. J. Ross, P. Selinger, D. S. Alexander and Jonathan M. Smith. Programming the Quantum Future. Communications of the ACM, Vol. 58 No. 8, 2015.
(4) M. Pagani, P. Selinger, ---. Applying quantitative semantics to higher-order quantum computing. In POPL 2014.}
%\medskip
% \textbf{Renaud Vilmart}, PhD student supervised by E. Jeandel and S. Perdrix, has greatly contributed to make the \zx-calculus complete for Clifford+T quantum mechanics.
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Role in Project:} LORIA will develop the front-end compilation of HLLs into \azx terms.
As one of the main contributors to the \zxcalculus and expert of 1WQC, LORIA will also play a key role in the development of \azx taking into account the different models of computation.
The site provies expertise both in quantum programming
languages and in the \zxcalculus.
The postdoc at LORIA
will spend half of their time on \ref{wp:frontend}, and divide the remaining time equally between the other WPs.
\end{minipage}
}
\newpage
%%%% Bull
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 4} & Bull\\
& ATOS Quantum Lab
\end{tabular}
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Expertise:}
Bull SAS, part of ATOS group, is the European industrial leader in
HPC and Big Data. It has extensive expertise of machine learning,
in particular in the context of high performance computing. It has
also a strong expertise in Quantum Computing, with a dedicated
team of 10 FTE, with activities relevant to the project : quantum
software, optimization of quantum circuits, high performance
simulation of quantum algorithms, theoretical physics.
\textbf{Cyril Allouche, PhD}, is the director of Quantum Computing R\&D of
Atos. An industrial member of the High Level Steering Committee of
the Quantum Flagship, he had strongly contributed to the
definition of Pillar 3, "compute". Relevant product is the "Atos
Quantum Learning Machine", first commercial product dedicated to
quantum programming and high performance simulation of quantum
algorithms
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Role in Project:}
With their expertise in high-performance computing Bull, will
focus on the HPC simulation of \azx terms (~\ref{task:HPC-sim-model}) however they will also contribute to
the front end (\ref{wp:frontend}) and compilation techniques
(\ref{wp:usefulstuff}). With expertise in building large scale
software Bull will also contribute the definition of the APIs that
the \azx toolchain will use.
\end{minipage}
}
\newpage
%%% Radboud Nijmegen
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 5} & Radboud Universiteit Nijmegen\\
& Institute for Computing and Information Sciences
\end{tabular}
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Expertise:} Situated within the largest digital security group in the Netherlands (51 members), the Radboud Quantum Group offers strong expertise in the formal mathematical structures underpinning both quantum theory and classical programming languages. It consists of two full-time academics, one postdoc, and six PhD students. The Quantum Group furthermore maintains active relationships with the security group as a whole, including prominent members of the classical and post-quantum cryptography communities (e.g. Joan Daemen, co-author of the renowned AES cipher; and Peter Schwabe, whose post-quantum key exchange protocol NewHope was recently trialled by Google\footnote{Nick Stratt. Google is working to safeguard chrome from quantum computers. The Verge, July 2016.}).
\textbf{Dr Aleks Kissinger} is an Assistant Professor of Quantum Structures and Logic in Radboud's Institute for Quantum and Information Sciences (iCIS). For the past 10 years, he has been instrumental in the development of the diagrammatic approach to quantum theory, notably developing the theory of classical and quantum interaction for general process theories~(1), classification of strong complementarity, and the ZW calculus~(2). He also co-authored the canonical textbook for the field~(3). Since 2006, he has also lead development on the Quantomatic tool~(4), which serves as the platform for the software and automated techniques in this proposal.
\textit{\color{gray} \textbf{Publications:} (1) B. Coecke, C. Heunen, and ---. Categories of quantum and classical channels. Quantum Information Processing, 15(12), 2016. (2) B. Coecke and ---. The compositional structure of multipartite quantum entanglement. In Proceedings of ICALP, 2010. Springer LNCS 6199. (3) B. Coecke and ---. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017. (4) Quantomatic: A Proof Assistant for Diagrammatic Reasoning. Proceedings of Conference on Automated Deduction (CADE) 2015. Springer LNCS 9195. \href{http://quantomatic.github.io}{\color{blue} quantomatic.github.io}}
\medskip
\textbf{Prof Bart Jacobs} is a Professor of Software Security and Correctness at Radboud, the holder of an ERC Advanced Grant in Quantum Computation, Logic, and Security, and a member of the National Cybersecurity Council. He has won several prestigious awards including the 2012 Huibregtsen award for Science and Society, the SURF Security and Privacy Award 2017, and is a recipient of the Dutch order of chivalry: Officer of Orange-Nassau. He has made major contributions to the formal theory of computation, including prominent textbooks on type theory~(1) and coalgebra~(2). He furthermore pioneered a new approach to modelling the logic of probabilistic and quantum systems, initiating the field of Effectus Theory~(3).
\textit{\color{gray} \textbf{Publications:} (1) ---. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999. (2) ---. Introduction to Coalgebra. Towards Mathematics of States and Observations. Cambridge University Press, 2017. (3) ---. New directions in categorical logic, for classical, probabilistic and quantum logic. Logical Methods in Computer Science, Vol. 11, 2015.}
\medskip
% \REM{Expertise of the organisation related to the project
% objectives. For the principal investigators give a brief CV,
% including gender, highlighting research experience; and list up
% to 5 relevant publications, and/or products, services
% (incl. widely-used datasets or software), or other achievements
% relevant to the call content. }
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Role in Project:}
The Radboud site will coordinate all aspects of the project
dealing with automation and tool development, focussed primarily in WP4. It will furthermore contribute strongly to WPs 2 and 3, and in the case of WP2, will serve as an important point of contact with the extensive quantum hardware groups working within the Netherlands, notably the
DiCarlo group in Delft. The \textit{postdoc} working at this site will focus on the development of automated tools and techniques for quantum program transformation and engage with nearby quantum hardware groups to target short- and long-term applications of those techniques.
\end{minipage}
}
\newpage
\subsection{Consortium agreement principles \REM{1/2 page max} }
\label{sec:cons-agre}
\REM{(partner's rights and duties)}
\REM{(IPR management)}
The consortium commits strongly to Open Science. All scientific works
produced in the course the project will be made available to the
general public free of charge. All articles will be published in Open
Access venues.
We aim at making our software available to the widest community so, with
one exception, all APIs and source code for the software artefacts
produced during the project will be freely available to the public,
under a permissive Open Source license (\eg the BSD
license\footnote{\url{https://opensource.org/licenses/BSD-3-Clause}}.)
However, the use of Bull HPC (see \S\ref{sec:sign-facil-large})requires proprietary Bull technologies for the
HPC simulation back-end module (\ref{task:HPC-sim-model}). This
module will not be open source. However, we will also provide a
generic reference implementation of this module, which will be
open source.
\subsection{Significant facilities and large equipment available to
the consortium to perform the project \REM{1/2 page max}}
\label{sec:sign-facil-large}
Bull (Partner 4) will provide high performance computing
(HPC) facilities which will be accessible by VPN to all project
participants. The available HPC facilities include:
\begin{itemize}
\item One Atos bullion in-memory x86 server, 384 cores and 16 Tbytes RAM
\item Nvidia P100 GPUs, as required.
\item Altera Stratix FPGA boards, as required.
\end{itemize}
%\BREM{TBC: ask Simon B.\ about access to NQIT's computing facilities at Oxford (Niel speculates that this would be available for NQIT related work at the very least)}
% --- The above is commented out instead of removed for the moment, but it appears that this is something we would have to budget for and so cannot be taken for granted. (NdB)
\subsection{Link with ongoing projects \REM{1/2 page max}}
\label{sec:link-with-ongoing}
\begin{itemize}
\item \textbf{Oxford}: we have a very strong
connection to the NQIT project, the United Kingdom's largest quantum
hardware technology project. Benjamin is the leader of the NQIT
``Architectures'' work-package, and is an Associate Director of the
NQIT project as a whole. Abramsky and de~Beaudrap work on the
``Quantum/classical interface and emulation'' workpackage of NQIT,
and are responsible for guiding the development of a compiler for
the NQIT architecture. This gives the \azx\ project unique access
to the expertise and information regarding the NQIT, and will help
to ensure that the activities of the \azx project are directed at
goals which are of direct practical relevance to practical quantum
computational platforms.
% \BREM{Very close collaboration / overlap with NQIT, which is
% interested in co-operating in the development of \azx\ as a
% practical optimising compiler technology that will fits very
% tightly with the planned approach to error-corrected memories}
\item \textbf{Oxford}: we have a connection with the \pounds2M Quantum
Causal Structures JTF grant (with Coecke as PI), which includes the
study of causal aspect of quantum computing.
\item \textbf{Oxford}: ongoing work on quantum and
probabilistic programming languages, funded through a Royal Society
University Research Fellowship (Principled Foundations of
Programming Languages, Staton), an EPSRC Project (EP/N007387/1:
Quantum Computation as a Programming Language, Staton) and a grant
from the Korean Government (Staton). That ongoing work is currently
on the theoretical side of quantum programming languages and their
semantics, and this proposal adds a new direction because it bridges
the gap towards practice.
\item \textbf{Strathclyde:} the Carnegie Trust awarded a PhD
Scholarship to Mr Joseph Collins for the project ``Infinite
Dimensional Categorical Quantum Mechanics''. This contributes to
the later parts of \ref{task:axioms}.
\item \textbf{Radboud}: ERC advanced grant ``Quantum Computation,
Logic, and Security'' (QCLS) held by Jacobs. This 5-year 2.5M euro
project will conclude during year 1 of the \azx project. Main
outcomes: a new mathematical formalism, \emph{effectus theory}, that
covers Boolean, probabilistic, and quantum computation in a single
framework and an associated Python tool EfProb for modelling
probabilistic and quantum systems. The accrued tools and expertise
will greatly enhance our effectiveness in providing concrete tools
related to WP3 and WP4.
\end{itemize}
\newpage
\subsection{Financial plan (1 page)}
\label{sec:financial-plan}
\REM{The resources to be committed for each project partner have to be
described in the Electronic Submission System by the
coordinator. These resources include: Personnel, Consumables,
Equipment, Travel, Subcontracting, Provisions, Licensing fees,
other. Justify them here. Both the justification and the information
in the system will be communicated to the Evaluation Panel.}
\paragraph{Personnel}
\label{sec:personnel}
This is a large and multifaceted project, which will require
significant work to deliver. A full-time post doc at each academic
site is needed, under supervision of the site lead. In addition, At
all the academic sites there is a large amount of time donated to the
project by senior scientists with relevant expertise. At Bull, our
industrial partner, several engineers will contribute to the project.
\begin{itemize}
\item \emph{Post-doctoral researchers}: We request 36 months of salary
for post-docs at Strathclyde, Oxford, LORIA, and Nijmegen. They
will be hired as soon as possible by the site leads at each site.
\item \emph{Coordinator}: We request 10\% contribution the
Duncan's salary at Strathclyde to cover the time spent managing
the project. This is reduced from 20\% upon negotiation with
Stratclyde. (Duncan will contribute an additional 8.4 months of
time as a researcher, see below.)
\item \emph{Principle investigators and other named staff}: Spread
across the four academic sites, more than 110 person-months of time
will be contributed by the named staff on the project, all of which
is supported by other sources. This means that almost 40\% of the
research effort of the project is funded from elsewhere.
\item \emph{PhD Students}: at LORIA, Renaud Vilmart will contribute
approx 9 months to the project; this is funded from other sources.
\item \emph{Engineers}: At Bull, we request 29 person-months for
research engineers, familiar with Bull's HPC systems, and
experienced in making commercial software products. They will be
essential in achieving our planned impacts.
\end{itemize}
\paragraph{Workshops}
\label{sec:workshops}
Project workshops serve a key role in intra-project communication,
dissemination, and outreach. We plan one workshop each year, in
Oxford, Nijmegen, and Nancy respectively. Our entire advisory board
will be invited to these workshops, which increases the cost beyond
the usual expenses of venue hire and speakers' expenses. We have
budgeted \euro 6.5k for the first one\footnote{Included in the
Oxford site's consuambles budget.} (which is planned to be smaller) and
\euro 12k for the second and third.
\paragraph{Travel and subsistence}
\label{sec:travel-subsistence}
Since many of the personnel have expertise relevant to more than one
work package, we request substantial budget for travel, for quantERA
reporting meetings, for formal project meetings, smaller more frequent
WP meetings, and also to present our work at conferences.
\paragraph{Equipment}
\label{sec:equipment}
\begin{itemize}\item We request 25\% of the cost of new server blades to upgrade our
dedicated HPC facility. This facility will be available to the
entire project via VPN, and will be used across several tasks, most
crucially for \ref{task:HPC-sim-model}.
\item We also request laptop computers for each of the postdocs, and
replacement laptops for some staff at LORIA. These are necessary
because of the frequent need to travel and work at another site
and/or present work at conferences or workshops.
\end{itemize}
\subsection{Ethical issues \REM{1/2 page}}
\label{sec:ethical-issues}
\REM{Describe any foreseeable ethical issue that may arise during the
course of the research project. Describe all mitigation strategies
employed to reduce ethical risk, and justify the research
methodology with respect to ethical issues.}
No ethical issues foreseeable.
\newpage
\REM{max 30 references - OK AT THE MOMENT SINCE KEVIN-ROSS ONLY IN COMMENTS}
\bibliographystyle{plain}
\bibliography{quantera}
\end{document} %%% -- uncomment to throw away notes
\newpage
\ROUGH{
\section{NOTES}
There are many proposals for the implementation of a practical quantum
computer, using diverse , and based on various These
implementations have radically different operating and
constraints from each other, and also diverge sharply from the
idealised circuits used to describe quantum algorithms. This
diversity presents an obstacle to the adoption of quantum computing
since each platform will require its software to be written
specifically for it, in terms of its own low-level machine language,
rather than using a powerful high-level languages. At the other end of
the spectrum, programming language designers usually stays at the
logical circuit level when designing their compiler. In consequence,
quantum programmers willing to go for hardware must be machine
specialists, limiting the possible exploitation of quantum computing.
Several quantum programming languages exist which
allow programmers to define algorithms in a high level way, but which
take no account of the characteristics of the underlying hardware. In
this project we will close this gap.
focus
on the front-end part of the compiler (parsing and analysis of
code), and yet be able to offer The chosen intermediate representation will
also make it easy to port the compilation chain to a new quantum
architecture, by concentrating on the translation of the
intermediate representation to the new hardware representation.
We will produce an \emph{intermediate representation} for quantum
software which will be independent of the high-level language and the
target hardware, and which will allow a variety of program
transformations such as optimisation and adding error-correction.
This language will be based on the \zxcalculus \cite{Coecke:2009aa}
, which has already been
used for similar things.
\paragraph{Quipper to ZX}
\label{sec:quipper-zx}
The Quipper language already exists and is pretty good. Thanks to
Selinger and his team there is also a good library of large scale
quantum algorithms written in Quipper. Let's take advantage of this
by writing a new back-end for the Quipper compiler. It can already
generate quantum circuit diagrams, and we know how to translate
circuits to \zx, so this should be easy. This can be used to generate
test cases to support the main activities of the project.
\paragraph{ZX to architecture}
\label{sec:zx-architecture}
The \zxcalculus can represent anything, including many things which
are not physical, or which may have no correspondence something
runnable on a given architecture. In this task we devise criteria for
(i) recognising when a ZX term corresponds to something runnable and
(ii) rewriting the term to something which can be directly translated
into the machine model. We already have two abstract machine models:
circuits and the one-way machine. Our quantum architecture partners
will help develop models which reflect more realistic hardware. Where
possible we'll actually generate ``machine code'' for these machines
(including HPC simulators).
\paragraph{Useful Magic 1: Fault Tolerance}
\label{sec:useful-magic-1}
Given the ZX term corresponding to some algorithm, we produce a
fault-tolerant version based on some error correcting code.
There has already be some work on \zxcalculus and error correcting
codes, so the basics are in place. Harder steps are to prove that the
fault-tolerant version is equivalent to the original, and establish
criteria for what transformations we can do to the fault tolerant
version without breaking the fault tolerance.
\paragraph{Useful Magic 2: optimisation}
\label{sec:useful-magic-1}
Devise tactics which rewrite a given ZX term to minimise various
metrics associated with a given machine model: e.g. T-count for
circuits, classical depth for MBQC etc. Our quantum architecture
people will help come up with suitable metrics for realistic
hardware. The \zxcalculus has some powerful normal form results which
will facilitate this. (But see the point above.)
\paragraph{ZX 2020}
\label{sec:zx-with-t}
The \zxcalculus is known not to be complete in its full generality,
nor for the Clifford + T fragment. Selinger and Bian have recently
given a complete equational presentation for the Clifford + T group.
We extend the \zxcalculus to contain this equational theory and
implement a decision procedure for equality of terms. This will make
the ZX-calculus complete enough for government work.
\paragraph{Programming constructs in ZX}
\label{sec:progr-constr-zx}
The ZX calculus has the !-box, a graphical version of the Kleene
Star. This is useful, but it's not enough to represent everything of
interest in a compact form. We will add new graph patterns to the
language to handle iteration and/or recursion, at least in limited
form. (Compare the two-stage compilation of Quipper -- the graph
patterns would be used to encode ``parameters'' in the Quipper
terminology). TO go along with this we will develop induction
principles so that we can do proofs about ZX-terms using these
constructs.
\paragraph{Quantomatic++}
\label{sec:quantomatic++}
The intention is that the results described above will be realised as
running code rather than papers. The existing Quantomatic tool may
serve as a starting point for this. Relative to the current
quantomatic we require several extensions to support new ZX features,
but also an important improvement in performance to support reasoning
with very large graphs.
}
\end{document}