% !TEX TS-program = pdflatexmk
\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{Compilation and optimisation for near-term quantum computing using the ZX calculus}
\newcommand\projacro{Co-Op ZX}
\title{QuantERA Full Proposal}
\author{}
\date{}
\maketitle
\begin{center}
{\Huge \projacro }\\
{\LARGE \projtitle }
\end{center}
\newpage
\textit{Title page will be replaced with file Front-Page\\
\oldt{Text from previous proposal in blue}}
\newt{Very recent revisions for the new proposal are in violet}
\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}
%currently 2510 characters
\REM{(publishable abstract, max. 1/2 page): Be precise and
concise. This summary will be used to select suited reviewers for
the proposal.}
Recent investment in quantum technologies has paid off, and quantum computers are now here. Current and near-term quantum computers, known as noisy intermediate-scale quantum (NISQ) devices, have few qubits, short coherence times, and non-trivial gate error. In this regime, quantum software support -- in particular focussed towards compilation and optimisation -- is vital to the efficient use of scarce, noisy, hardware resources, and the development of implementable protocols that go beyond what is feasible classically.
These NISQ computers are not so much single devices, but instead patchworks of components (including classical) which vary greatly between implementations such as silicon qubits, superconducting circuits, or ion traps. Programming such devices currently requires intimate knowledge of the hardware, which is a significant barrier to the realisation of usable, scalable quantum computers, as programs must be rewritten for every new device. High-level software descriptions of quantum algorithms must be translated to low-level control instructions for quantum hardware.
\newt{Furthermore, whereas}
classical computers have had a roughly static concept of ``low-level instructions'' for decades, the analogous notion for quantum hardware is constantly changing and evolving to cope with the rapid progress in quantum technology. We face a situation where the ever-multiplying range of quantum computers has minimal software support.
\newt{%
We propose the development of ``deep quantum compilation'' technology, which is the concept of a compiler for quantum systems which can be used to develop large portions of the software stack, in a way which is modular in design but tightly integrated once compiled.
A ``deep'' quantum compiler will be versatile enough to target a wide variety of hardware implementations, and simple enough to support any programming language.
To develop such a compiler, we will leverage the versatility and the power of the \zxcalculus, a tensor-based system for analysing quantum operations.
Recent formal and practical advances in completeness and optimisation of the \zxcalculus demonstrate a proof-of-principle of the possibility of developing a deep quantum compiler, including provably-correct program transformations for automatically adding error correction and performing hardware-guided optimisations.
Developing such a compiler will allow for the sound development of tightly integrated software stacks for quantum computers, enabling them to perform computations better and faster.
}%
%The goal of this project is to develop the flexible intermediate for compilation and optimisation, which is necessary for the immediate-term practical implementation of post-classical protocols on noisy intermediate-scale quantum computers. %how many buzzwords can we get in this sentence
\REM{ OLDTEXT This project introduces \azx, a flexible intermediate language for
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.}
\section*{Relevance to the topic addressed in the call}
\label{sec:relev-topic-addr}
%currently 1274 characters
\REM{(in particular specify here which part of the call text is
concerned by your project, max. 1/4 page):}
The project clearly comprises ``\textit{transformative research}'' that explores ``\textit{collaborative advanced interdisciplinary science and/or cutting-edge engineering with the potential to initiate or foster new lines of quantum technologies}'', which is the key overall objective of QuantERA.
We include several ``\textit{excellent young researchers}'', including from Poland, along with well-established figures at all levels in the project, and partner with Cambridge Quantum Computing, a clearly ``\textit{ambitious high-tech SME}''.
In particular we address the \textit{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}". Machine-dependent optimisation work will contribute to the ``\textit{development of devices to realise multiqubit algorithms}". More generally, this project is an enabling
technology that multiplies the impact of all the target
outcomes of QuantERA and the Quantum
Technology Flagship.
\REM{ FROM CALL DOCUMENT:
The QuantERA consortium has created a common funding instrument to support European research projects enabling long-term research in the area of Quantum Technologies.
Through this instrument, the national/regional funding organisations of the QuantERA consortium contribute to the Quantum Flagship agenda1. By launching joint European calls for research projects, they can support more diverse research communities, who are able to tackle the most challenging and novel research directions.
QuantERA projects should be of a FET-like nature and contribute to the development of the European research and innovation in Quantum Technologies. The transformative research done in QuantERA should explore collaborative advanced interdisciplinary science and/or cutting-edge engineering with the potential to initiate or foster new lines of quantum technologies and help Europe grasp leadership early on in promising future technology areas.
**warning this paragraph is patronising bullshit, fuck this "spreading research excellence" western-euro superiority nonsense:
To spread research excellence throughout Europe, QuantERA projects are encouraged to include partners from the widening countries participating in the call: Bulgaria, Croatia, Czech Republic, Hungary, Latvia, Lithuania, Poland, Portugal, Romania, Slovakia, Slovenia and Turkey.
To build leading innovation capacity across Europe and connect with industry, QuantERA projects are encouraged to involve key actors that can make a difference in the future, for example excellent young researchers, ambitious high-tech SMEs etc.
3. Quantum computation
Development of devices to realise multiqubit algorithms; demonstration and optimisation of error correction codes; interfaces between quantum computers and communication systems.
Development of novel quantum algorithms; demonstration of quantum speed-up; new architectures for quantum computation.
}
\REM{ OLDTEXT 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.
}
\newpage
\section{EXCELLENCE \REM{(6 pages)}}
\label{sec:overview}
\newt{Very recent revisions for the new proposal are in violet}
\subsection{Targeted breakthrough, baseline of knowledge and skills}
\label{sec:targ-breakthr-basel}
\REM{
Describe the targeted breakthroughs of the project.
Describe how the science and technology contribute to the establishment of a solid baseline of knowledge and skills for the specific theme addressed.
Describe the specific objectives of the project, which should be clear, measurable, realistic and achievable within the duration of the project.
}
\paragraph{Summary: }
\label{sec:summary:-}
\newt{%
We propose to develop \emph{deep quantum compilation technology}.
This consists of techniques for a compiler to translate high-level specifications of quantum programs to operations on a variety of quantum hardware platforms, automatically managing the resources and architectural constraints in doing so.
This allows the software stack to be developed and organised in a modular fashion for multiple platforms, and then compiled in an intelligently managed way to make the most of quantum hardware resources.
}
\\
\textit{\bfseries\ttfamily\color{red!70!black} REPLACE THE FOLLOWING WITH SOMETHING WHICH ILLUSTRATES OUR GLORIOUS VISION OF AN ALL-ENCOMPASSING COMPILER.
IT MAY BE BEST THAT WE AVOID ANYTHING THAT SUGGESTS A GIANT OCTOPUS SPRAWLING OVER THE FACE OF THE EARTH.}
\vspace{-2mm}
\vspace{-1mm}
\cgraph[0.65]{arch-diagram.pdf}\vspace{-5mm}
\paragraph{Context:}
\label{sec:context}
\newt{%
Effective programming practise allows the programmer to design software without paying very close attention to the nature of the hardware.
In the context of quantum technologies, this is made difficult by the fact that hardware platforms are varied~\cite{PhysRevX.4.041041,Raussendorf-2001,KendonAncilla} \texttt{\bfseries \color{red!70!black}[double-check this list of references for suitability]}, have limited resources, and are evolving quickly.
Due to the overhead involved in making quantum computations fault-tolerant, different platforms will continue to be developed for different tasks (with and without error correction), even as quantum hardware technologies mature and demonstrate scalability.
The complications presented by limited resources and divergent architectures will likely persist for the forseeable future.
For classical programs, modern compiler toolchains such as LLVM\footnote{%
The LLVM Compiler Infrastructure, \url{http://llvm.org}}
decouple high-level programming from different hardware platforms, allowing for easy and customisable cross-compilation.
Building on recent developments in the theory and application of the \zxcalculus~\cite{BH-2017,NW-2017,JPV-2018,DKPdW-2019}, the opportunity exists to develop a more ambitious version of the LLVM concept for quantum computing, bringing forward the day that quantum computers can be exploited for practical application.
}
\paragraph{Targeted breakthrough:}
\label{sec:targ-breakthr}
\newt{%
We will develop \emph{deep quantum compilation technology}: that is to say, techniques which may be used by a compiler to translate high-level quantum programs to low-level operations on quantum hardware platforms.
In doing so, it will intelligently manage all of the details involved in realising a quantum procedure on hardware, including
\begin{itemize}
\item
incorporating the architectural constraints of the hardware platform,
\item
optimising the use of hardware resources,
\item
and managing the realisation of error correction,
\end{itemize}
in a way which can be specified in a modular way but which is tightly integrated upon compilation.
To demonstrate this technology, we will develop a compiler from a high-level quantum programming language to hardware, for (i)~optically-coupled ion traps (NQIT)~\cite{PhysRevX.4.041041} and (ii)~quantum-dot devices (Grenoble)~\texttt{\bfseries \color{red!70!black}[do we have something here to cite?]}.
We will specifically pursue the development of deep quantum compilation technology by exploiting the versatility of the \zxcalculus, and further developing its application.
}%
This will greatly improve the software ecosystem for quantum computers:
\newt{deep quantum compilation will allow future quantum devices to}
easily run existing programs, and future programming languages automatically gain support on a wide range of hardware.
\paragraph{Baseline of knowledge and skills:}
\label{sec:basel-knowl-skills}
\newt{%
Several powerful high-level languages (HLLs) have been proposed for quantum programs, such as Quipper~\cite{Alexander-S.-Green:2013fk} and \Qsharp~\cite{qsharp}.
As with classical HLLs, these languages are not designed to be run directly on quantum hardware: instead, their compilers typically output quantum circuit descriptions, which are not tailored well to run on any particular hardware platform.
}%
\newt{%
Our proposal is to develop an analogue of the LLVM compiler system, for quantum computation.
The LLVM compiler system is a modularised collection of libraries for hardware realisation and optimisation for classical programming, providing the functionality which is expected of a well-designed modern compiler.
An analogue of LLVM for quantum systems would have to manage resources in spite of fundamentally quantum obstacles, such as the no-cloning theorem; and to be useful in the near term, it would also have to account for noise and the resources required for error correction, in addition to the functionality of the sort provided by LLVM.
}
\newt{%
One way to realise a comparable compiler technology for quantum computers is to use the \zxcalculus~\cite{Coecke:2009aa}, which is a formal system for transforming quantum procedures in a way that preserves meaning.
The \zxcalculus is the product of a decade of work by members of this consortium
on the mathematical foundations of quantum computing \cite{AbrCoe:CatSemQuant:2004,
%Coecke:2009db, CDKW-lics:2012qy,
Coecke2017Picturing-Quant}, and can be viewed in two distinct ways: either (i)~as a formal axiomatic theory which encodes the properties of complementary observables in categorical algebra, or (ii)~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.
Recently, members of our consortium developed versions of the \zxcalculus which were complete for Clifford+T computations~\cite{Jeandel2017A-Complete-Axio,NW-2018} and for quantum computations including CNOTs and arbitrary single-qubit gates~\cite{NW-2017,JPV-2018}.
This means that one can formally prove every equality of quantum circuits in these gate models through the application of a small number of relatively simple rules for rewriting tensors.
This stunning achievement opens the door to many
new possibilities for optimisation and verification of quantum
computations.}
% 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.}
\newt{
The \zxcalculus %has been extensively applied to quantum computation, and
is powerful and flexible, and can easily describe computations in both the circuit and measurement-based models of quantum computation (MBQC)~\cite{Raussendorf-2001}.
%Due to its great flexibility and expressive power, the \zxcalculus can be used to
and 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 representation is especially well-suited to describe systems having a natural have graph structure.
Examples include surface codes for topological cluster-states \cite{Horsman:2011lr}, and MBQC \cite{Duncan:2012uq}, where it has been used to translate \cite{Duncan:2010aa} between the 1-way model and the circuit model.}
Here is an example of such a transformation:\vspace{-1mm}
\\
\textit{\bfseries\ttfamily\color{red!70!black} CONSIDER USING DIFFERENT FIGURE}
\vspace{-2mm}%
% (see Figure~\ref{fig:zx-mbqc-cnot}).
\[
\cnoti[0.7] \rTo^*
\cnotii[0.6] \rTo^*
\cnotiii[0.6] \rTo^*
\cnotiv[0.6] \rTo^*
%\cnotv[0.6] \rTo^*
\cnotvi[0.7]
\]~\\[-4mm]%
\newt{%
Members of our consortium have demonstrated how to use these formal reasoning techniques into software, including}
the interactive theorem prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which was used to formally verify quantum communication protocols and error correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr}) and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early demonstration of the capacity of the \zxcalculus to perform circuit optimisation.
\TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}
%%% cutting because repeated later
% It is strictly more powerful than the stabiliser
% formalism~\cite{Backens:2012fk},
%\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}.
\newt{%
Our goal is to develop tools to facilitate running 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}
\newt{%
Using the \zxcalculus to manage resources in quantum hardware is a totally new application of the \zxcalculus, and a totally new way to realise computations on quantum hardware.
Unlike sequences of gates, the tensor networks which are the terms of the \zxcalculus have no preordained causal structure beyond the global input and output.
This provides us with great flexibility with respect to time-space trade-offs, and will help to achieve optimal implementations on diverse architectures.
}%
Furthermore, our system allows transformations of tensor networks which cannot be expressed as equations between circuits.
\texttt{\bfseries\color{red!70!black} [Add diagram illustrating an application of ZX which is not shackled to the circuit model, and text to refer to it]}
% to reduce its terms to minimal forms. This flexibility has been
% exploited in the \zxcalculus to convert between the circuit model and
% the MBQC model via intermediate steps not expressible in either model
% \cite{Duncan:2010aa,Duncan:2012uq}.
\newt{%
In addition to these benefits, the \zxcalculus is a sound and complete formal system for transforming quantum procedures, so that each program transformation which our compiler system would realise will be provably correct, and indeed comes with a proof of its correctness.
At the same time, the way that the \zxcalculus represents quantum procedures avoids the immediate dimensional explosion associated with explicit matrices, so that it will in many cases be more efficient than any other automated technique for reasoning about quantum procedures.
}
\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 with
insights 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}
\newt{%
Our goal is to develop technology for a ``deep compiler'' for quantum computing systems:
\begin{itemize}
\item
one which allows for the modular design of the quantum software stack, allowing programmers to write at a high level for any hardware and any quantum error correcting technology;
\item
but such that upon compilation, the result is a tightly integrated piece of software, which is well-tailored to the specific resources, architecture, control systems, and hardware of a specific platform.
\end{itemize}
\texttt{\bfseries \color{red!70!black}[refer to specific platforms here (NQIT + Grenoble)?]}
This is very technically ambitious: but while it has never been done before, we believe it to be achievable on the basis of our earlier work.
}
\REM{
Our central aim is to define, in \azx, (i)~a~formal tool to express formally verified code transformation and
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 layouts
of 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 natural, as it is the \emph{lingua franca} of quantum computation researchers.
The project proposes a new foundation for quantum software, based on a flexible tensor-based representation, combined with mathematically rigorous semantics and formal verification.
\newt{%
The deep quantum compilation technology which we develop
}%
will allow the computer to do the heavy lifting of managing resources and mapping operations onto the quantum hardware, allowing both the developers of hardware and software to focus their attentions elsewhere.
This will facilitate the development of new architectures and technologies for quantum computing.
A key example, exploited in our collaboration with NQIT, is that lattice surgery operations on surface codes do not fit into the gate model, but have natural and simple representations in the \zxcalculus \cite{BH-2017}.
\REM{
While the \zxcalculus is
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 \newt{quantum compiler technology}, which we call the \dzxc (``\emph{deep ZX compilation}'') system, 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.
\newt{%
The \dzxc system will augment this basic formal system with 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.
\newt{%
The \dzxc system}
will retain the mature and effective formal tensor language of
the \zxcalculus at its heart, ensuring semantic soundness, logical
completeness \cite{Jeandel2017A-Complete-Axio,NW-2017},
\newt{%
and allowing us to leverage techniques from earlier work (cf.~\texttt{quantomatic}~\cite{Kissinger2015Quantomatic:-A-} and~\texttt{PyZX}~\cite{DKPdW-2019}).} %, as well as new techniques developed as part of this project,
This denotational kernel specifies the
process 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}.
\newt{%
The \dzxc system
}%
would 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,
\newt{%
the \dzxc system could encorporate
}%
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}).
\newt{%
This would enable the \dzxc system
}%
to re-write procedures, to minimise the number of operations subject to the constraints described by those annotations.
\newt{%
The \dzxc system would be modular, and allow for several different systems of annotations, for different hardware platforms or constraints one might impose on a computation.
One such system of annotations would be to describe
}%
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.
\newt{%
To accommodate this, the \dzxc system would incorporate
}%
a second class of annotations to represent limited forms of iteration and recursion, yielding
\newt{%
\emph{parametric} \zx terms.}
While the hardware-derived annotations are inferred in a bottom-up fashion, the parametric structure is produced top-down, based on the original
\newt{%
high-level quantum procedure provided as input.}
% --- The following commented out as I'm not sure what it means or if it contributes to the meaning of the proposal:
% 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-}.
\texttt{\bfseries \color{red!70!black} [apropos to refer to PyZX here?]}
Early in the development of
\newt{%
the \dzxc system,
}%
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.}
%\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 \zx and other quantum computing representations (\ref{wp:frontend}); necessary theoretical developments of \zx (\ref{wp:backends}); optimisation strategies independent of implementations (\ref{wp:theory}); using enriched \zx to compile and optimise for specific quantum devices.(\ref{wp:usefulstuff}).
\subsubsection{A quantum compiler stack}
\label{sec:progr-lang-supp}
\newt{%
Several powerful high-level languages (HLLs) have been proposed for quantum programs, such as Quipper~\cite{Alexander-S.-Green:2013fk} and \Qsharp~\cite{qsharp}.
}%
\newt{%
As with classical HLLs, these languages are not designed to be run directly on quantum hardware: instead, their compilers typically output quantum circuit descriptions, which are not tailored well to run on any particular hardware platform.
Our proposed \dzxc system would represent an interface between multiple different HLLs for quantum procedures, and various quantum hardware platforms.
This system would use terms of the \zxcalculus as an internal representation of the procedure as it undergoes optimisations and translations to fit a particular hardware architecture.
This representation would not be required from or exposed to the user,\footnote{This said, the \zxcalculus has proved a very useful notation for mathematical proofs.}
but would 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 \zx terms.
}%
\newt{%
As most existing quantum HLLs can output circuit descriptions, and as circuits can easily be represented in the \zxcalculus,
}%
we first focus on a simple front end for the circuit language QASM~\cite{Cross2017Open-Quantum-As} in \ref{task:HHL} before moving towards more expressive HHLs.
\newt{%
This will allow virtually any extant quantum HLL to interface with the \dzxc system, albeit rather naively at first.
}%
Later, we will perform concrete front-end
experiments using more sophisticated existing HLLs in, for example
\emph{Quipper}, \Qsharp~\cite{qsharp}, or ProjectQ
\cite{Steiger2016ProjectQ:-An-Op}, with the help of
Task~\ref{task:betterboxes}.
The open database of tests developed in \ref{task:testBench} will
serve as a measuring tool for the quality of the output. The database
will also be made available to the community for rating and testing
future compilers or optimisation techniques. To encourage interaction
from other research groups, and to support other languages,
\newt{%
the interfaces and functionality for the \dzxc system will be made public.
}%
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 a
fixed 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}
%
Due to the novelty of our proposal, we adopt an exploratory approach with respect to back-end models.
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.
\newt{%
These models will allow us to prototype the development of hardware annotations for the \dzxc system.
In both cases, this involves three tightly related tasks:
\begin{enumerate}[label=(\roman*)]
\item
decomposing the tensor network into atomic operations;
\item
characterising runnability in the model, by predicates in monadic second order logic; and
\item
transforming the tensor network into an equivalent runnable version.
\end{enumerate}
}
This experience will inform the later work in \ref{wp:theory} and
\ref{wp:usefulstuff}.
Although we will provide specific modules for the tasks described above,
\newt{%
the \dzxc 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}).
\texttt{\bfseries \color{red!70!black}[is this redundant to a paragraph above about \ref{task:testBench}?]}
%% OUTDATED
%In a hybrid architecture like NQIT, these
%properties will vary across the subsystems, with concomitant
%implications for the execution of the desired program.
\subsubsection{Representation, reasoning, and resources}
\label{sec:machines-models}
\REM{stuff about WP 2 here}
\oldt{\benREM{This
paragraph needs refactoring, but I need Belen's input to make a
vaguely\\coherent new text}
Since the overall goal of the project is to produce a
\emph{retargetable} compiler, able to generate executables for
multiple architectures, these differing characteristics must be taken
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}.}
A key research challenge of this work package consists in the
management of the {\em classical computation} and {\em classical
information} within quantum algorithms: What computation should
occur at the \azx-generation phase, and which classical parameters are
passed on to the \azx terms? Task \ref{task:betterboxes} focuses on
the question of tests based on measurement results: how should they be
integrated within \azx?
%
While in the early stages of the project, it will already be quite
useful to study concrete diagrams of fixed size (e.g. a quantum
circuit on $N$ qubits for a previously-fixed $N$), in task
\ref{task:axioms}, we will extend \azx to support parametrised
families of diagrams (e.g. quantum circuits with $N$ qubits where $N$
can vary) mirroring the control structures present in a quantum
HLL. This will enable more sophisticated, generic optimisations to be
run in advance of needing any particular computational procedure.
The test suite designed in~\ref{task:testBench}
will be used to compare and choose amongst the possible solutions.
\subsubsection{Machine-independent optimisation}
\label{sec:repr-reas-azx}
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. We forsee three stage in the compilation process of an \azx
term into a physical machine. The first two stages are
machine-independent (\ref{wp:theory}) while the last stage is machine
dependent (\ref{wp:usefulstuff}).
The tasks to be performed within WP3 and WP4 may be broadly described in terms of how the \azx compiler will transform \zx terms produced by the front-end to obtain instructions to be realised by a quantum computer (or software quantum simulator) at the back-end.
These stages are: (i)~an initial round of generic,
hardware-independent optimisations; (ii)~application of some choice of
strategy for error correction; (iii)~translation to a specialised
annotation system which represents the parameters and constraints of a
specific hardware implementation; and finally (iv)~another round of
optimisation within the constraints imposed by the error correction
and hardware models.
WP3 is devoted to Items (i) and (ii) while WP4 focuses on (iii) and (iv).
In addition to the development of the tools for these stages, WP4 will develop an interface for the specification of the annotation systems used in stages (iii) and~(iv) above, allowing for easy extension of the \azx compiler to arbitrary hardware systems and allowing \azx to act as a general-purpose quantum compiler.
The first stage of the compilation process represents a ``generic optimisation'' subroutine (\ref{task:basic-opt}), which may be applied to arbitrary \zx terms.
This subroutine will re-write \zx terms into ones with fewer resources in a broadly applicable sense, such as fewer total nodes or fewer nodes which realise non-Clifford transformations (for instance, corresponding to $T$ gates).
This may be developed independently of the results of WP1 or WP2 using existing techniques (as well as incorporating any further useful techniques developed in \ref{task:axioms} and~\ref{task:algorithms}).
The second stage of the compilation process is to take a generic \zx term expressing a computation on idealised quantum systems, and re-write it as a \zx term representing an equivalent transformation of error-corrected qubits (\ref{task:ECC}).
As well as the \zx terms to translate, this will take as input a specification the particular error correction code or other fault-tolerance construction to apply.
Recent breakthroughs in the theory of the \zx-calculus
\cite{Jeandel2017A-Complete-Axio,NW-2017}, have shown that whenever two
\zxcalculus diagrams describe the same linear operator, then one can be
transformed into the other using just a finite set of local,
diagrammatic transformations.
However, completeness of the \zxcalculus is just the beginning of the
story for \azx.
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 and theory synthesis.
In task~\ref{task:axioms}, we will extend the
\zx-calculus in two respects. The first is to expand into complete
and universal qudit variations to work effectively beyond 2-level
systems, and the second is to gain a deeper understanding of the role
played by W-type tensors as they interact with the generators of the
\zx-calculus, which are themselves of GHZ-type.
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.
%%
%% OUTDATED
% 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}.
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} we
will 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.
\subsubsection{Machine-dependent optimisation}
\label{sec:comp-quant-softw}
\oldt{
\benREM{To update}
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.}
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 front-end \ref{wp:frontend},
the theoretical work of \ref{wp:backends} and instantiation of the
generic optimizations considered in \ref{wp:theory}, and will result
in software forming the basis of a general-purpose quantum compiler.
This machine-dependent, last part of the compilation process consists
in two stages: formatting to the target system (\ref{task:runnable})
and a last round of machine-dependent optimizations
(\ref{task:opt-machine}). We identify three main tasks: to add
suitable machine-dependent 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.
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}.
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.
\benREM{Missing discussion on the hardware: T4.1 and T4.2.}
\subsection{Interdisciplinary nature}
\label{sec:interd-nature}
\oldt{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.
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.
}
\newpage
\section{IMPACT \REM{(3 pages)}}
\label{sec:impact-2-pages}
\subsection{Expected impacts}
\label{sec:expected-impacts}
\oldt{
\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.
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.
\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.
\oldt{
\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.}
\subsection{Dissemination, exploitation of results, communication}
\label{sec:diss-expl-results}
\paragraph{Dissemination.\!\!}
\label{sec:dissemination}
\oldt{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.\!\!}
\oldt{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 and
the 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,
\oldt{
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.
}
\paragraph{Advisory Board:\!\!}
\label{sec:advsiory-board}
\oldt{
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 \bR Will Zeng (Rigetti Quantum Computing) --- may be fired soon\e.
\item \bR More suggestions: Winfried Hensinger, Mike Mosca, Martin Roetteler, Michael Beverland\e.
\end{itemize}
Letters of support from the board members are attached at the end of
this document.}
\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).
}
\oldt{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}
\oldt{
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}{A quantum compiler stack}{1M}{36M}{wp:frontend}
\WPleaderLOR
\WPeffort{0}{0}{0}{0}{0}{0}
\begin{WPaim}
This WP develops elements of \zx as in intermediate compiler language.
This includes interfaces between \zx and up to known high-level quantum languages (HLL), and down to the device level of the target technologies.
In the first instance we make contact between \zx and standard circuit and measurement-based models, in which all current quantum protocols are framed.
% 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:circuit-model}]{Idealised quantum circuits
(M1--M9; Responsible 2; Involved: 1,3,4)}{%
Translate an \zx term to an equivalent quantum circuit with ideal
gates. This will require algorithms for discovering a suitable
causal ordering on the \zx 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 a \zx 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: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:HHL}]{Front-end (M3--M36; responsible 3;
involved 2,4,5) }{%
Propose compiler front-end from known HLLs such as QASM, Quipper
or \Qsharp to \azx. This task serves as a test-bed
for~\ref{task:testBench} and~\ref{task:trans1}.
%
}
\WPtask[\label{task:testBench}]{Open test-suite (M3--M36;
responsible 3; involved 2,4,5) }{%
Devise test-suite of concrete instances of circuits and
algorithms to rate success of other WPs. This includes the task of protocol extraction from current known HLLs.
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.
%
}
\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[\label{del:earlyapi}]{M6}{Preliminary front-end for QASM, and initial \azx API}
%
\WPdeliverable{M12}{Preliminary benchtests of circuits and algorithms}
%
\WPdeliverable{M15}{Module for generation of 1WQC code from \azx terms}
%
\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}
\WPdeliverable[\label{del:backendapi}]{M36}{API for back-end
modules, including specification language for architectures.}
\end{WPdeliverables}
\end{WP}
\newpage
%%%
%%%%%%%WP 2
%%%
\begin{WP}{Representation, reasoning, and resources in \zx}{1M}{36M}{wp:backends}
\WPleaderPOL
\WPeffort{0}{0}{0}{0}{0}{0}
\begin{WPaim}
We build the theoretical foundations for \zx as an intermediate representation. This includes extending the capabilities of \zx to represent mixed states, qudit states, and control flows. We use \zx axiomatisations and automated theorem provers to extract out post-classical computing resources, which will be used both for further optimisation work, and for characterisation of quantum algorithmic speed-up.
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:axioms}]{Beyond qubits and stabilisers
(M1--M12; Responsible: 2; Involved: 1,3,5)}{%
We will exploit further the recent completeness results to give representations for mixed state qubit quantum theory. We will
extend the \textsc{zx} tensor formalism from the qubit domain to
higher dimensions.
% and exploit the translation from \textsc{zx}- to \textsc{zw}-calculus.
}
\WPtask[\label{task:betterboxes}]{Control in \zx
(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:resources}]{Resources and axioms
(M1--M18; Responsible: 1; Involved: 2,3,5)}{%
We will exploit the three axiom sets for Clifford, Clifford+T, and universal qubit QM,
to identify and distill specific resources that are necessary to quantum speed-up. In particular, to focus on finding multiple resource elements (rather than simply magic states), and to characterise post-classical composition as a resource.
This includes developing \zx representations of contextuality, as a possible post-classical resource.
}
\WPtask[\label{task:resourcesagain}]{Computational resources
(M1--M18; Responsible: 1; Involved: 2,3,5)}{%
We will use the existing graph re-writing and automated theorem proving tools of Quantomatic and PyZX to determine parts of the re-writing process that are difficult to compute classically. This will then be used to extract candidate subroutines for sources of quantum speed-up. Along with the previous task, these will be used to develop procedures for characterising if a \zx-represented algorithm demonstrates speed-up or not.
}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable{M12}{Deliverable.}
\WPdeliverable{M15}{Deliverable.}
\WPdeliverable{M24}{Deliverable.}
\WPdeliverable{M36}{Deliverable.}
\end{WPdeliverables}
\end{WP}
\newpage
%%%
%%%%%%%WP 3
%%%
\begin{WP}{Machine-independent optimisation}{M1}{M36}{wp:theory}
\WPleaderOXF
\WPeffort{0}{0}{0}{0}{0}{0}
\begin{WPaim}
We develop practical logical and algorithmic techniques for transforming ``abstract'' \zx terms produced from a high-level program in ways
which will be required by any practical compiler, and reasoning about their properties. Examples include:
resource optimisation, adding error-correction, and execution
layout. This lays the groundwork for machine-dependent optimisation in the next work package.
\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: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.
}
\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).
}
%%
\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.
}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable{M18}{\zx language constructs for basic control
flow, repetition and recursion}
\WPdeliverable{M24}{A library of general-purpose techniques and
algorithms for simplifying \zx terms}
\WPdeliverable{M24}{Algorithms and heuristics for optimising \zx
terms, including minimisation of T gate count}
\WPdeliverable{M24}{Routines for adding error-correction to \zx
programs}
\WPdeliverable{M24}{An extended \zx 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
%%%
%%%%%%%WP 4
%%%
\begin{WP}{Machine-dependent optimisation}{1M}{36M}{wp:usefulstuff}
\WPleaderGREN
\WPeffort{0}{0}{0}{0}{0}{0}
\begin{WPaim}
We import machine-dependent specifications to \zx terms, and use this to optimise algorithms further for specific hardware constraints. We focus on the silicon quantum dot devices developing in Grenoble, the ion traps developed in Oxford, and the superconducting devices accessible through CQC and partnership with IBM. This is the culmination of all previous work packages, and feeds back into them. The final result will be \ldots.
Also machine-dependent error correction here?
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:Si-model}]{Grenoble quantum dots (M13--M36 Responsible: 2;
Involved: 1,5)}{
We will model the quantum dot device being developed in Grenoble, and extract specific annotations for
\zx that describe key elements of the architecture. This will
include qubit layout on wafers, network connectivity, and timing
and fidelity of potential entanglement links. A suitably annotated \zx term
will then be translated to an executable sequence of hardware
instructions -- output language to be defined in collaboration with
the team at LETI.
}
\WPtask[\label{task:delft-model}]{Oxford ion traps (M13--M30 Responsible: 5;
Involved: 1,2)}{
In collaboration with the Oxford ion trap group and the NQIT team, we will design an output module which generates code for a realistic model of
ion trap quantum computers, including qubit losses and leakage, gate
timings, and circuit layout. Output language to be defined in collaboration with hardware experts at Oxford.}
\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}.
}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable{M24}{Deliverable}
\WPdeliverable{M24}{Deliverable}
\WPdeliverable{M30}{General purpose layout engine}
\WPdeliverable{M36}{Optimising compiler for \azx, suitable for compiling to Grenoble and/or Oxford 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}
\WPleaderGREN
\WPeffort{3}{3}{2}{1}{2}{0}
\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. Grenoble & 0 & 11 & 19 & 15 & 3 & 48 \\\hline
2. LORIA & 7 & 27 & 28 & 22 & 3 & 87 \\\hline
3. Oxford & 32 & 12 & 20 & 18 & 2 & 84 \\\hline
4. CQC & 5 & 18 & 0 & 5 & 1 & 29 \\\hline
5. Gdansk & 3 & 12 & 13 & 21 & 2 & 51 \\\hline
6. 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 were 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. For a year now the group has an ongoing collaboration with Cambridge Quantum Computing Ltd. The Computer Science Department at Oxford is currently ranked 1st in the world.
% \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{Dr.\ Miriam Backens} is Career Development Fellow at Balliol College, Oxford. They proved completeness of stabiliser \zxcalculus and of the single-qubit Clifford+T fragment, and co-developed the related ZH-calculus as well as proving its completeness. \textit{\color{gray} \textbf{Publications:}
(1) ---. The ZX-calculus is complete for stabilizer quantum mechanics. NJP 16, 2014. arXiv:1307.7025.
(2) ---. The ZX-calculus is complete for the single-qubit Clifford+T group. EPTCS 172. arXiv:1412.8553.
(3) --- and A.~Kissinger. ZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non- linearity. QPL 2018. arXiv: 1805.02175.}
\textbf{Prof.\ Bob Coecke} is Professor of Quantum Foundations, Logics and Structures, and pioneered categorical and diagrammatic methods for quantum computing (1), and \zxcalculus\ in particular (with Duncan) (2). He is/has supervised approx.~50 PhD students, which include Hadzisasanivic, Ng and Wang who proved universal completeness of the \zx-calculus \cite{NW-2017}, and included Backens who proved stabiliser completeness \cite{1367-2630-16-9-093021}. He co-authored \em Picturing Quantum Processes \em (3), which presents diagrammatic methods for quantum computing to a broader audience.
\textit{\color{gray} \textbf{Publications:} (1) S.~Abramsky and ---. A categorical semantics of quantum protocols. In LICS 2004. (2) --- and R.~Duncan. Interacting quantum observables: Categorical algebra and
diagrammatics. NJP 13 (043016), 2011. (3) --- and A.~Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. CUP, 2017. }
\textbf{Dr.\ Niel de Beaudrap} \bR 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. +++\e
\textit{\color{gray}
\textbf{Publications:}
(1) ---. Finding flows in the one-way measurement model. PRA~77 (022328), 2008.
(2) --- and D.~Horsman. The ZX calculus is a language for surface code lattice surgery. arXiv:1704.08670.
}
\textbf{Dr.\ Quanlong Wang} is on an IAA Secondment at Cambridge Quantum Computing Ltd., working on ZX-calculus. Before doing a 2nd PhD at Oxford he was a Lecturer in Mathematics at Beijing University of Aeronautics and Astronautics. He was the 1st to prove universal completeness of universal \zxcalculus. He also established a simple complete set of rules for 2-qubit circuits, which later were proved to be universally complete.
\textit{\color{gray} \textbf{Publications:}
(1) A. Hadzihasanovic, K. F Ng and ---.
Two complete axiomatisations of pure-state qubit quantum computing. LiCS 2018.
(2) B. Coecke and ---. ZX-rules for 2-qubit clifford+T quantum circuits. In RC 2018.
}
% \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}).
%
% \bR \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.}
% (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. \bR 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. \e
\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}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: