diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 1ae87bf2a4aab9920b133841e441717ea2eecb52..45bef449d91e35d9eea8512b1fbc0fe8b822c5ad 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -57,7 +57,7 @@ These NISQ computers are not so much single devices, but instead patchworks of c
This project develops the \zx calculus of observables as a flexible intermediate language for quantum computation, and a core element in compilation for immediate use with NISQ devices. This intermediate language will be versatile enough to target a wide variety of hardware implementations, and simple enough to support any programming language. This project builds on recent significant formal and practical advances in completeness and optimisation of the \zx calculus. The former enables provably-correct program transformations for automatically adding error correction and performing hardware-guided optimisations, e.g. by preferring certain quantum gates over others or enforcing topological constraints. This project will develop, enrich (with annotations), and standardise the \zx language for quantum computation, integrate it into an effective stack of tools for compiling quantum programs, and develop new techniques for automated transformations that make quantum computations run better and faster.
-%The goal of this project is to develop the flexible intermediate representation for compilation and optimisation, which is necessary for the immediate-term practical implementation of post-classical protocols on noisy intermediate-scale quantum computers. %how many buzzwords can we get in this sentence
+%The goal of this project is to develop the flexible intermediate for compilation and optimisation, which is necessary for the immediate-term practical implementation of post-classical protocols on noisy intermediate-scale quantum computers. %how many buzzwords can we get in this sentence
\REM{ OLDTEXT This project introduces \azx, a flexible intermediate language for
quantum computation, which removes this obstacle by providing a
@@ -135,6 +135,8 @@ Technology Flagship.
\section{EXCELLENCE \REM{(6 pages)}}
\label{sec:overview}
+\newt{Very recent revisions for the new proposal are in violet}
+
\subsection{Targeted breakthrough, baseline of knowledge and skills}
\label{sec:targ-breakthr-basel}
@@ -147,108 +149,85 @@ Describe the specific objectives of the project, which should be clear, measurab
\paragraph{Summary: }
\label{sec:summary:-}
-\oldt{Our goal is to develop a flexible intermediate representation
-for quantum software which enables formally verified program
-transformations, and based on this, to construct the back-end for a
-re-targetable optimising compiler for a variety of
-realistic quantum computer architectures.}\\
-\textit{FIGURE NEEDS RE-DRAWING}
+\newt{%
+ We propose to develop a flexible intermediate representation for quantum software, to enable formally verifiable transformations of circuits.
+ This will form the basis of a re-targetable optimising compiler for any practical quantum computer architecture based on quantum circuits.
+}
+\\
+\textit{\bfseries\ttfamily\color{red!70!black} FIGURE NEEDS RE-DRAWING}
\vspace{-2mm}
\vspace{-1mm}
\cgraph[0.65]{arch-diagram.pdf}\vspace{-5mm}
-
-
\paragraph{Context:}
\label{sec:context}
-\oldt{High-level programming languages (HLLs) increase programmer
-productivity and software reliability, provided that the HLL compiler
-can generate machine code which runs well on
-the intended hardware platform. Quantum algorithm designers have the
-choice of
-several powerful quantum programming languages %, in various paradigms
-\cite{Alexander-S.-Green:2013fk, Paykin2017a, Steiger2016ProjectQ:-An-Op, export:209634}.
-However, proposed implementations of quantum computers vary greatly due
-to differing underlying technologies (ion traps, superconducting
-circuits, optics) and architectural concepts (networked vs. hybrid, measurement
-based, ancilla driven)~\cite{PhysRevX.4.041041,Raussendorf-2001,KendonAncilla},
-and no language takes account of the specific characteristics of any
-given platform. Worse, the technology
-is evolving quickly, none of these characteristics are stable, and no
-consensus has yet emerged on the best choice. For classical programs,
-modern compiler toolchains such as LLVM\footnote{The LLVM Compiler
- Infrastructure, \url{http://llvm.org}}
-decouple the HLL from the machine by using an \emph{intermediate
- representation} (IR), which is independent of both. By translating
-to and from the IR, any HLL may be used on any platform. A quantum IR
-accommodating dissimilar architectures is needed
-to support software on rapidly shifting hardware.}
-
+High-level programming languages (HLLs) increase programmer productivity and software reliability --- provided that the HLL compiler can generate machine code which runs well on the intended hardware platform.
+Quantum algorithm designers have the choice of several powerful quantum programming languages~\cite{Alexander-S.-Green:2013fk, Paykin2017a, Steiger2016ProjectQ:-An-Op, qsharp}.
+\newt{%
+ However, these languages do not describe how to realise programs on specific hardware platforms, of which there are several, using different technologies (ion traps, superconducting circuits, optics) and architectural concepts (networked vs.\ hybrid, ancilla driven, measurement based)~\cite{PhysRevX.4.041041,Raussendorf-2001,KendonAncilla}.
+ Even at such a time as quantum hardware technology matures, we cannot be assured that exactly one platform will predominate for all quantum information processing applications.
+}
+For classical programs, modern compiler toolchains such as LLVM\footnote{%
+ The LLVM Compiler Infrastructure, \url{http://llvm.org}}
+decouple the HLL from the machine by using an \emph{intermediate representation} (IR), which is independent of both.
+By translating to and from the IR, any HLL may be used on any platform.
+A quantum IR accommodating dissimilar architectures is needed to support software on rapidly shifting hardware.
\paragraph{Targeted breakthrough:}
\label{sec:targ-breakthr}
-\oldt{We will define a universal intermediate representation language,
+\newt{%
+ We will define a versatile and universal intermediate representation language,
+}
called \azx, which is platform-agnostic but which facilitates program
-transformations appropriate
-to specific hardware. Specifically, \azx will provide the following (see \S\ref{sec:impl-2-pages} for more detail):
+transformations appropriate to specific hardware.
+Specifically, \azx will provide the following (see \S\ref{sec:impl-2-pages} for more detail):
\begin{itemize}
-\item An easy-to-generate universal language.
- \item Automated IR transformations for
- error correction, resource optimisation, and execution layout.
- \item A complete compilation pipeline from HLL to hardware for (i)
- superconducting transmon qubits (QuTech)
- \cite{Versluis2016Scalable-quantu} and (ii)
- optically-coupled ion traps (NQIT) \cite{PhysRevX.4.041041}.
+\item
+ \newt{An easily-specified and easily-generated universal language for quantum transformations.}
+\item
+ Automated IR transformations for error correction, resource optimisation, and execution layout.
+\item
+ A complete compilation pipeline from HLL to hardware for (i)~superconducting transmon qubits \oldt{(QuTech)~\cite{Versluis2016Scalable-quantu} and (ii)~optically-coupled ion traps (NQIT)~\cite{PhysRevX.4.041041}}.
\end{itemize}
-The theory, algorithms, and software architecture behind this will be
-flexible and extensible, thus permitting programming languages and
-architectures not explicitly included in the project scope to
-be supported. This will greatly improve the software
-ecosystem for quantum computers: by supporting \azx, future quantum
-devices may easily run existing programs, and future programming
-languages automatically gain support on a wide range of hardware.}
+\newt{%
+ The theory, algorithms, and software architecture behind this will be flexible and extensible.
+ This will permit programming languages and architectures not explicitly included in the project scope to be supported.}
+This will greatly improve the software ecosystem for quantum computers: by supporting \azx, future quantum devices may easily run existing programs, and future programming
+languages automatically gain support on a wide range of hardware.
\paragraph{Baseline of knowledge and skills:}
\label{sec:basel-knowl-skills}
-\oldt{The closest extant thing to a quantum IR is QASM
-\cite{Cross2017Open-Quantum-As}, a circuit description
-language. QASM is an output option for ProjectQ
-\cite{Hner2016A-Software-Meth}, and the input language for
-IBM's \emph{Quantum Experience}\footnote{This is a publicly accessible
- 5-qubit device; \url{http://research.ibm.com/quantum/}.}; the
-ProjectQ team describe a compilation process for
-quantum software involving possibly multiple IRs, but do not describe
-a specific one. State-of-the-art quantum programming languages such
-as Quipper \cite{Alexander-S.-Green:2013fk} and \liquid
-\cite{export:209634} support multiple targets; in practice the choice
+\newt{%
+ The closest extant thing to a quantum IR is QASM~\cite{Cross2017Open-Quantum-As}, a circuit description language.
+ QASM is the input language for IBM's quantum computing platforms, including the \emph{IBM Quantum Experience}\footnote{%
+ This is a publicly accessible 5-qubit device; \url{http://research.ibm.com/quantum/}.}.
+ QASM is an output option for ProjectQ \cite{Hner2016A-Software-Meth};
+ the ProjectQ team describe a compilation process for quantum software involving possibly multiple IRs, but do not describe a specific one.
+}
+State-of-the-art quantum programming languages such as Quipper~\cite{Alexander-S.-Green:2013fk}
+\newt{and Q\#~\cite{qsharp}}
+support multiple targets; in practice the choice
is between a circuit description or a classical simulation.
%(\liquid in particular is tightly integrated with its simulator).
Neither language exposes an IR.
-Our proposed language \azx is the successor to the \zxcalculus
-\cite{Coecke:2009aa}, a graphical tensor notation
-developed by members of this consortium during a decade
-of work on the mathematical foundations of quantum computing
-\cite{AbrCoe:CatSemQuant:2004,
+\newt{%
+ Our proposed IR is built on the \zxcalculus~\cite{Coecke:2009aa}, a graphical tensor notation developed by members of this consortium during a decade of work on the mathematical foundations of quantum computing \cite{AbrCoe:CatSemQuant:2004,
%Coecke:2009db, CDKW-lics:2012qy,
- Coecke2017Picturing-Quant}. The \zxcalculus can be viewed in two
-distinct ways: first, as a formal axiomatic theory which encodes the
-properties of complementary observables in categorical algebra;
-second, as a symbolic notation for tensor networks representing
-quantum states and linear operators. Terms in the \zxcalculus are labelled graphs;
-equations in the calculus are reified as a small number of graph
-rewrite rules.
-This equational theory is frequently more
-tractable than working explicitly with matrix representations. Very
-recently \cite{Jeandel2017A-Complete-Axio} members of our consortium
-have presented a version of the \zxcalculus which is \emph{complete}
-for the Clifford+T fragment of quantum mechanics, which means that for the first time
-there is a finite axiomatic theory which can prove every true
-statement about practical quantum computation, and just before submitting this proposal a version of the \zxcalculus which is complete for universal quantum computing i.e.~the Hilbert space based equational theory can be replaced with an entirely diagrammatic one \cite{NgWang}.\footnote{This result still needs some fine-tuning and cleaning-up, but the very fact that this can be done is an unexpected boost for the potential of the \zxcalculus.} This stunning achievement opens the door to many
+ Coecke2017Picturing-Quant}.}
+The \zxcalculus can be viewed in two distinct ways:
+\newt{%
+ either as a formal axiomatic theory which encodes the properties of complementary observables in categorical algebra; or as a symbolic notation for tensor networks representing quantum states and linear operators.}
+Terms in the \zxcalculus are labelled graphs; equations in the calculus are reified as a small number of graph rewrite rules.
+This equational theory is frequently more tractable than working explicitly with matrix representations.
+\newt{%
+ Recently, members of our consortium developed versions of the \zxcalculus which were complete for Clifford+T computations~\cite{Jeandel2017A-Complete-Axio,NW-2018} and for quantum computations including CNOTs and arbitrary single-qubit gates~\cite{NW-2017,JPV-2018}.
+ This means that one can formally prove every equality of quantum circuits in these gate models through the application of a small number of relatively simple rules for rewriting tensors.}
+This stunning achievement opens the door to many
new possibilities for optimisation and verification of quantum
computations.
@@ -259,23 +238,20 @@ computations.
%\REM{The closely related ZW-calculus \cite{Hadzihasanovic2015A-Diagrammatic-} provides a complete characterisation of qubit entanglement-classes.}
-The \zxcalculus has been extensively applied to
-quantum computation, and can easily describe computations
-in both the circuit and measurement-based models of quantum
+The \zxcalculus has been extensively applied to quantum computation, and can easily describe computations in both the circuit and measurement-based models of quantum
computation (MBQC)~\cite{Raussendorf-2001}.
% a proven track record in
%quantum computation, in particular treating error correction
%\cite{Horsman:2011lr,Chancellor2016Coherent-Parity}, and translating between
%architectures \cite{Duncan:2010aa}.
-Due to its great flexibility and expressive power, the \zxcalculus can be used to formulate and verify quantum error correcting codes
-\cite{Chancellor2016Coherent-Parity, Duncan:2013lr} and quantum algorithms
-\cite{Stefano-Gogioso2017Fully-graphical, Zeng2015The-Abstract-St}. Its graphical
-language is especially well-suited to systems which
-naturally have graph structure such as surface codes for topological
-cluster-states \cite{Horsman:2011lr} and MBQC \cite{Duncan:2012uq},
-where it has been used to translate
-\cite{Duncan:2010aa} between the 1-way model
-and the circuit model. Here is an expample of such a transformation:\vspace{-1mm} % (see Figure~\ref{fig:zx-mbqc-cnot}).
+Due to its great flexibility and expressive power, the \zxcalculus can be used to formulate and verify quantum error correcting codes \cite{Chancellor2016Coherent-Parity, Duncan:2013lr} and quantum algorithms \cite{Stefano-Gogioso2017Fully-graphical, Zeng2015The-Abstract-St}.
+\newt{Its graphical representation is especially well-suited to describe systems having a natural have graph structure.
+Examples include surface codes for topological cluster-states \cite{Horsman:2011lr}, and MBQC \cite{Duncan:2012uq}, where it has been used to translate \cite{Duncan:2010aa} between the 1-way model and the circuit model.}
+Here is an example of such a transformation:\vspace{-1mm}
+\\
+\textit{\bfseries\ttfamily\color{red!70!black} CONSIDER USING DIFFERENT FIGURE}
+\vspace{-2mm}%
+ % (see Figure~\ref{fig:zx-mbqc-cnot}).
\[
\cnoti[0.7] \rTo^*
\cnotii[0.6] \rTo^*
@@ -283,15 +259,11 @@ and the circuit model. Here is an expample of such a transformation:\vspace{-1mm
\cnotiv[0.6] \rTo^*
%\cnotv[0.6] \rTo^*
\cnotvi[0.7]
- \]\vspace{-3mm}
-
-Furthermore, techniques for automated
-reasoning in the \zxcalculus were developed for the interactive
-theorem prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-}
-which was used to formally verify quantum communication protocols and error
-correcting codes
-\cite{Chancellor2016Coherent-Parity,Duncan:2013lr}.
-\TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}}
+ \]~\\[-4mm]%
+\newt{
+ Furthermore, members of our consortium have also incorporated these formal reasoning techniques into software, including the interactive theorem prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which was used to formally verify quantum communication protocols and error correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr}) and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early demonstration of the capacity of the \zxcalculus to perform circuit optimisation.
+\TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}
+}
%%% cutting because repeated later
% It is strictly more powerful than the stabiliser
% formalism~\cite{Backens:2012fk},
@@ -318,11 +290,11 @@ correcting codes
\paragraph{Contribution to the theme addressed}
\label{sec:contr-theme-addr}
-\oldt{We specifically address the theme of \emph{Quantum Computation}. The
+We specifically address the theme of \emph{Quantum Computation}. The
goal of \azx is to make it easy to run quantum programs on any
available quantum device. This will speed new quantum devices and
architectures into use, and broaden the range of potential users of
-quantum computers.}
+quantum computers.
\subsection{Novelty, level of ambition and foundational character}
\label{sec:novelty-level-ambit}
@@ -349,29 +321,23 @@ quantum computers.}
\paragraph{Novelty:}
\label{sec:novelty}
-\oldt{\azx is a totally new way of representing computation.
-Tensor networks
-specify \emph{what} the program should do, augmented with separate
-instructions for \emph{how} the hardware should do it. Unlike
-sequences of gates, these tensor networks have no preordained causal
-structure beyond the global input and output. This gives the \azx
-system great flexibility with respect to time-space trade-offs, and
-will help to achieve optimal implementations on diverse architectures.
-Further, the language allows transformations of tensor networks which
-cannot be expressed as equations between circuits. Key examples
-include powerful normal-form theorems for Frobenius
-and Hopf algebras.
+\azx is a totally new way of representing computation.
+Tensor networks specify \emph{what} the program should do, augmented with separate instructions for \emph{how} the hardware should do it.
+Unlike sequences of gates, these tensor networks have no preordained causal structure beyond the global input and output.
+This gives the \azx system great flexibility with respect to time-space trade-offs, and will help to achieve optimal implementations on diverse architectures.
+\newt{Furthermore, our system allows} transformations of tensor networks which cannot be expressed as equations between circuits.
+\oldt{Key examples include powerful normal-form theorems for Frobenius and Hopf algebras.}
+\textsf{\bfseries\color{red!70!black} [I think that we need a better selling point here --- N]}
+
% to reduce its terms to minimal forms. This flexibility has been
% exploited in the \zxcalculus to convert between the circuit model and
% the MBQC model via intermediate steps not expressible in either model
% \cite{Duncan:2010aa,Duncan:2012uq}.
-A second indispensable novelty of our project, compared to existing
-program calculi, is that the equational theory is based on quantum
-mechanics rather than classical concepts. This formal underpinning
-implies that our program transformations are provably correct, and
-indeed will come with proofs of their correctness. This symbolic
-approach also avoids the dimensional explosion of explicit matrices.}
+\newt{%
+ Another novel and essential element of our project is that the basis of the \azx, the \zxcalculus, is a formal equational theory: this implies that our program transformations are provably correct, and indeed will come with proofs of their correctness.
+}
+This symbolic approach also avoids \newt{the immediate dimensional explosion} of explicit matrices.
\REM{This project rests on more than a decade of investigations into the
categorical structure of quantum mechanics. This project therefore has a uniquely
@@ -417,18 +383,10 @@ computation tasks.}
\paragraph{Ambition:}
\label{sec:ambition}
-\oldt{Developing a vertically integrated system from high-level programming
-languages to two different quantum computing architectures
-(\ref{task:delft-model}, \ref{task:NQIT-model}) is ambitious in its
-scale and reach, and has not been done before. We take a technically
-ambitious approach to quantum software, reconstructing a program's
-implementation from its specification and the characteristics of the
-target machine.
+\newt{%
+ Our goal is to develop a vertically integrated system to construct a program's implementation, from its specification in a high-level language, and the characteristics of the target machine, for two different quantum computing architectures (\ref{task:delft-model}, \ref{task:NQIT-model}).
+ This is very technically ambitious: but while it has never been done before, we believe it to be achievable on the basis of our earlier work.
}
-% However we believe, on the basis of our earlier work, that
-% this is achievable within the time frame of the project.
-
-
\REM{
Our central aim is to define, in \azx, (i)~a~formal tool to express formally verified code transformation and
@@ -457,19 +415,15 @@ of logical qubits.
\REM{More here. semantics of quantum programming languages is still very young, and already many dead ends. This project gives a unique opportunity for applications to drive theory.}
-\oldt{All other systems take the gate model of quantum computing as a given:
-this is entirely natural as it is the \emph{lingua franca} of quantum
-computation researchers. The project proposes a new foundation for
-quantum software, based on a flexible, powerful, tensor-based
-representation combined with mathematically rigorous semantics and
-formal verification. The \azx system will allow quantum hardware
-implementors to forget the gate model, present a simpler interface to
-the outside world, and let the compiler bridge the gap. This in turn
-will facilitate the development of new architectures and technologies
-for quantum computing. A key example, exploited in our collaboration
-with NQIT, is that lattice surgery operations on surface codes do not
-fit into the gate model, but have natural and simple representations
-in the \zxcalculus \cite{BH-2017}.}
+\newt{%
+ All other systems take the gate model of quantum computing as a given.
+ This is natural, as it is the \emph{lingua franca} of quantum computation researchers.
+ The project proposes a new foundation for quantum software, based on a flexible tensor-based representation, combined with mathematically rigorous semantics and formal verification.
+ The \azx system will allow the computer to do the heavy lifting of managing resources and mapping operations onto the quantum hardware, allowing both the developers of hardware and software to focus their attentions elsewhere.
+}
+This will facilitate the development of new architectures and technologies for quantum computing.
+A key example, exploited in our collaboration with NQIT, is that lattice surgery operations on surface codes do not fit into the gate model, but have natural and simple representations in the \zxcalculus \cite{BH-2017}.
+
\REM{
While the \zxcalculus is
@@ -495,7 +449,9 @@ multiple options and to address high scientific and technological
risks.
}
-\oldt{Our proposed \azx language is an advanced \textsc{zx}-style system
+\benREM{I think this part is more or less OK to keep ``as it''.}
+
+Our proposed \azx language is an advanced \textsc{zx}-style system
augmented with features needed for applications. The \zxcalculus
occupies a place in quantum computation similar to the
$\lambda$-calculus in classical computing: it provides a solid but
@@ -512,7 +468,7 @@ to achieving our goal of supporting multiple targets.
% don't stand for anything either!
\azx will retain the mature and effective formal tensor language of
the \zxcalculus at its heart, ensuring semantic soundness, logical
-completeness \cite{Jeandel2017A-Complete-Axio,NgWang}, and allowing
+completeness \cite{Jeandel2017A-Complete-Axio,NW-2017}, and allowing
techniques from earlier work (cf.~\texttt{quantomatic}
\cite{Kissinger2015Quantomatic:-A-}) %, as well as new techniques developed as part of this project,
to be applied to \azx terms. This denotational kernel specifies the
@@ -525,7 +481,7 @@ Development of such techniques is a low-risk extension of earlier
work, and will be done early in the project
(\ref{task:algorithms},\ref{task:basic-opt}). Further, at this stage
a program can be translated to a fault-tolerant equivalent with
-respect to a chosen error-correcting code.}
+respect to a chosen error-correcting code.
% \REM{Can do useful stuff at this level! Some optimisation; ECC
% simple generic optimisations. e.g.
@@ -543,8 +499,7 @@ respect to a chosen error-correcting code.}
-
-\oldt{The annotations of the second layer provide the basis of \emph{augmented
+The annotations of the second layer provide the basis of \emph{augmented
rewrites}: program transformations which are guided by the
annotations to achieve particular goals, not expressible in the basic
tensor language. For instance, there is an efficient algorithm
@@ -557,14 +512,15 @@ We propose to generalise this concept to encompass other sorts of information wh
For example, we would develop a system which specifies both how to represent logical operations in a particular error correcting code, and how the operations are constrained in order to satisfy basic precautions to keep the realisation fault-tolerant (\ref{task:ECC}).
We may then attempt to re-write procedures, to minimise the number of operations subject to the constraints described by those annotations.
We may further elaborate such a system of annotations by a description of the constraints and the costs involved for operations within a particular hardware platform (\ref{task:runnable}).
-For example, in
+%%For example, in
% Other
%examples of annotations might include paths in the graph corresponding
%to the trajectories of physical qubits, or subgraphs corresponding to
%the primitive hardware operations and the time required to execute
%them. For
-hybrid architectures like NQIT, the annotations will also
-indicate the differing behaviour of the subsystems. Augmented
+%%hybrid architectures like NQIT, the annotations will also
+%%indicate the differing behaviour of the subsystems.
+Augmented
rewrites will be used to find a runnable implementation of the
abstract tensor for the target platform, and to optimise resource use.
The development
@@ -597,7 +553,7 @@ project~\cite{KZ:2015:aa, Kissinger2015Quantomatic:-A-}.
Early in the project, we will implement translations from existing
quantum programming languages~(\ref{task:trans1}). These will provide
examples and test cases, and allow comparative
-evaluation.} % of the \azx system. %We will adapt an existing compiler to generate parameterised \azx terms (\ref{task:trans2}).
+evaluation. % of the \azx system. %We will adapt an existing compiler to generate parameterised \azx terms (\ref{task:trans2}).
% Due to the fact that there exist ZX-based software, additional features were added to the language e.g.~`bang-boxes' which are formal incarnations of the ``..." occurring in the above equations.
@@ -608,7 +564,6 @@ evaluation.} % of the \azx system. %We will adapt an existing compiler to gener
% \REM{Risk assessment: which are easy, which are hard? Dependencies.}
-\REM{WHY this is a good idea.}
@@ -659,9 +614,9 @@ various themes: the relation between \zx and other quantum computing representat
\subsubsection{A quantum compiler stack}
\label{sec:progr-lang-supp}
-\oldt{In the quantum setting, several powerful high-level languages
-(HLLs) such as Quipper~\cite{Alexander-S.-Green:2013fk} and \liquid
-\cite{export:209634} have been proposed. As in the case of their
+In the quantum setting, several powerful high-level languages
+(HLLs) such as Quipper~\cite{Alexander-S.-Green:2013fk} and Q\#
+\cite{qsharp} have been proposed. As in the case of their
classical counterparts, these HLLs are not designed to be run directly
on quantum hardware, rather their compilers typically output quantum
circuit descriptions.
@@ -675,48 +630,34 @@ general framework for compilation of HLLs to \azx.
Since most existing quantum HLLs can output circuit descriptions, and
since circuits can easily be represented in the \zxcalculus, we first
-design a simple front end for the circuit language
-QASM~\cite{Cross2017Open-Quantum-As} in
-\ref{task:transQASM}. This will allow \azx terms to be produced from
-virtually any extant quantum HLL, albeit rather naively.
-Later, we will perform concrete front-end experiments using more
-sophisticated existing HLLs, for example \emph{Quipper},
-\liquid, or ProjectQ \cite{Steiger2016ProjectQ:-An-Op} during the
-long running task~\ref{task:transHLL}.
-
-This work package consists of a back-and-forth interaction between
-HLLs and \azx, which is why many of its tasks span the entire lifetime
-of the project. HLL development influences \azx by providing the
-control structures and other constructs that must be represented at
-\azx level. Conversely, \azx developments will influence HLL, as we
-analyse how information and requirements from the back-end flow upward
-in a meaningful way, and how this can be translated into compilation
-flags and assertions/hints to the compiler within HLL programs.
-
-A key research challenge of this work package consists in the
-management of the {\em classical computation} and {\em classical
- information} within quantum algorithms: What computation should
-occur at the \azx-generation phase, and which classical parameters are
-passed on to the \azx terms? To help answer this question we will
-design a test suite (\ref{task:testBench}) to compare possible
-solutions.
-
+focus on a simple front end for the circuit language
+QASM~\cite{Cross2017Open-Quantum-As} in \ref{task:testBench}. This
+will allow \azx terms to be produced from virtually any extant quantum
+HLL, albeit rather naively. Later, we will perform concrete front-end
+experiments using more sophisticated existing HLLs, for example
+\emph{Quipper}, Q\#~\cite{qsharp}, or ProjectQ
+\cite{Steiger2016ProjectQ:-An-Op} during the
+task~\ref{task:betterboxes}.
+%
The open database of tests developed in \ref{task:testBench} will
serve as a measuring tool for the quality of the output. The database
will also be made available to the community for rating and testing
future compilers or optimisation techniques. To encourage interaction
from other research groups, and to support other languages, both our
interface and the \azx language will be made
-public.}
-
-
-
-\subsubsection{Representation and reasoning}
-\label{sec:machines-models}
-
-\REM{stuff about WP 2 here}
-
-\oldt{Proposed and existing quantum devices differ along a variety of axes.
+public.
+
+%% OUTDATED
+% This work package consists of a back-and-forth interaction between
+% HLLs and \azx, which is why many of its tasks span the entire lifetime
+% of the project. HLL development influences \azx by providing the
+% control structures and other constructs that must be represented at
+% \azx level. Conversely, \azx developments will influence HLL, as we
+% analyse how information and requirements from the back-end flow upward
+% in a meaningful way, and how this can be translated into compilation
+% flags and assertions/hints to the compiler within HLL programs.
+
+Proposed and existing quantum devices differ along a variety of axes.
At the most abstract level, the quantum circuit model and the
1-way model \cite{Raussendorf-2001} have different execution
concepts and primitive operations, despite their computational
@@ -726,10 +667,44 @@ restrictions on which qubits may interact directly.
%Looking more closely,
Primitive operations will require different amounts of time,
different qubit implementations have different failure
-modes.\REM{noise,fidelitY} In a hybrid architecture like NQIT, these
-properties will vary across the subsystems, with concomitant
-implications for the execution of the desired program.
+modes.\REM{noise,fidelitY}
+Due to its novelty, we adopt an exploratory approach. Initially, and
+in parallel, we study the circuit model (\ref{task:circuit-model}) and
+the 1-way model (\ref{task:mbqc-model}) because these models are well
+understood, stable, and have been extensively treated in the
+\zxcalculus literature. We will use these examples to develop
+prototypical \azx constructs expressing the relevant properties. This
+consists in three tightly related tasks: decomposing the tensor
+network into atomic operations; characterising runnability with
+respect to the model by predicates in monadic second order logic; and
+transforming the tensor network into an equivalent runnable version.
+This experience will inform the later work in \ref{wp:theory} and
+\ref{wp:usefulstuff}.
+
+Although we will provide specific modules for the tasks described above, the
+\azx system is intended to extensible, so we will also publish an open
+API and specification language to simplify the task of adding new
+architectures and error correcting schemes to the system
+(\ref{task:backendapi}).
+
+
+%% OUTDATED
+%In a hybrid architecture like NQIT, these
+%properties will vary across the subsystems, with concomitant
+%implications for the execution of the desired program.
+
+
+
+
+\subsubsection{Representation, reasoning, and resources}
+\label{sec:machines-models}
+
+\REM{stuff about WP 2 here}
+
+\oldt{\benREM{This
+ paragraph needs refactoring, but I need Belen's input to make a
+ vaguely\\coherent new text}
Since the overall goal of the project is to produce a
\emph{retargetable} compiler, able to generate executables for
multiple architectures, these differing characteristics must be taken
@@ -742,47 +717,63 @@ characteristics and architectural constraints of various idealised and
realistic machines, and develop language features of \azx to express
these properties. The goal is two-fold: to facilitate
\emph{code-generation} for a given machine from an \azx term; and to
-expose information needed by the \emph{optimiser}.
+expose information needed by the \emph{optimiser}.}
-Due to its novelty, we adopt an exploratory approach. Initially, and
-in parallel, we study the circuit model (\ref{task:circuit-model}) and
-the 1-way model (\ref{task:mbqc-model}) because these models are well
-understood, stable, and have been extensively treated in the
-\zxcalculus literature. We will use these examples to develop
-prototypical \azx constructs expressing the relevant properties. This
-consists in three tightly related tasks: decomposing the tensor
-network into atomic operations; characterising runnability with
-respect to the model by predicates in monadic second order logic; and
-transforming the tensor network into an equivalent runnable version.
-This experience will inform the later work in \ref{wp:theory} and
-\ref{wp:usefulstuff}.
+A key research challenge of this work package consists in the
+management of the {\em classical computation} and {\em classical
+ information} within quantum algorithms: What computation should
+occur at the \azx-generation phase, and which classical parameters are
+passed on to the \azx terms? Task \ref{task:betterboxes} focuses on
+the question of tests based on measurement results: how should they be
+integrated within \azx?
+%
+While in the early stages of the project, it will already be quite
+useful to study concrete diagrams of fixed size (e.g. a quantum
+circuit on $N$ qubits for a previously-fixed $N$), in task
+\ref{task:axioms}, we will extend \azx to support parametrised
+families of diagrams (e.g. quantum circuits with $N$ qubits where $N$
+can vary) mirroring the control structures present in a quantum
+HLL. This will enable more sophisticated, generic optimisations to be
+run in advance of needing any particular computational procedure.
+The test suite designed in~\ref{task:testBench}
+will be used to compare and choose amongst the possible solutions.
-In the second phase we switch attention to real computers. The first
-target is a classical simulator running on HPC hardware provided by
-our industrial partner Bull. This will leverage existing expertise in
-simulation, combined with new techniques for symbolic evaluation of
-\azx terms. \ROUGH{Finally we study two concrete quantum computers
- based on different technologies: superconducting circuits (Delft)
- and optically linked ion traps (NQIT).} In both cases we will
-interact strongly with the experimental groups working on these
-models, who are either members of our consortium (S. Benjamin and
-N. de Beaudrap for NQIT) or our advisory board (L. DiCarlo in Delft).
-Since these architectures are dissimilar, tackling both is an ideal
-demonstration of our approach. The completion of this phase will
-allow quantum programs represented as \azx terms to be run on real
-hardware.}
\subsubsection{Machine-independent optimisation}
\label{sec:repr-reas-azx}
-\oldt{The formal mechanisms for transforming the \azx diagrams produced by
+The formal mechanisms for transforming the \azx diagrams produced by
HLL compilers into optimised, physically implementable computations
are the theoretical core of this proposal, and developing effective
-techniques for working with \azx diagrams are a prerequisite for our success.
+techniques for working with \azx diagrams are a prerequisite for our
+success. We forsee three stage in the compilation process of an \azx
+term into a physical machine. The first two stages are
+machine-independent (\ref{wp:theory}) while the last stage is machine
+dependent (\ref{wp:usefulstuff}).
+
+
+The tasks to be performed within WP3 and WP4 may be broadly described in terms of how the \azx compiler will transform \zx terms produced by the front-end to obtain instructions to be realised by a quantum computer (or software quantum simulator) at the back-end.
+These stages are: (i)~an initial round of generic,
+hardware-independent optimisations; (ii)~application of some choice of
+strategy for error correction; (iii)~translation to a specialised
+annotation system which represents the parameters and constraints of a
+specific hardware implementation; and finally (iv)~another round of
+optimisation within the constraints imposed by the error correction
+and hardware models.
+WP3 is devoted to Items (i) and (ii) while WP4 focuses on (iii) and (iv).
+In addition to the development of the tools for these stages, WP4 will develop an interface for the specification of the annotation systems used in stages (iii) and~(iv) above, allowing for easy extension of the \azx compiler to arbitrary hardware systems and allowing \azx to act as a general-purpose quantum compiler.
+
+The first stage of the compilation process represents a ``generic optimisation'' subroutine (\ref{task:basic-opt}), which may be applied to arbitrary \zx terms.
+This subroutine will re-write \zx terms into ones with fewer resources in a broadly applicable sense, such as fewer total nodes or fewer nodes which realise non-Clifford transformations (for instance, corresponding to $T$ gates).
+This may be developed independently of the results of WP1 or WP2 using existing techniques (as well as incorporating any further useful techniques developed in \ref{task:axioms} and~\ref{task:algorithms}).
+
+The second stage of the compilation process is to take a generic \zx term expressing a computation on idealised quantum systems, and re-write it as a \zx term representing an equivalent transformation of error-corrected qubits (\ref{task:ECC}).
+As well as the \zx terms to translate, this will take as input a specification the particular error correction code or other fault-tolerance construction to apply.
+
Recent breakthroughs in the theory of the \zx-calculus
-\cite{Jeandel2017A-Complete-Axio,NgWang}, have shown that whenever two
+\cite{Jeandel2017A-Complete-Axio,NW-2017}, have shown that whenever two
\zxcalculus diagrams describe the same linear operator, then one can be
transformed into the other using just a finite set of local,
diagrammatic transformations.
@@ -799,13 +790,33 @@ presentations of the Clifford+T \zx-calculus and develop strategies
for effectively simplifying \zx-diagrams. These include Knuth-Bendix
completion and theory synthesis.
In task~\ref{task:axioms}, we will extend the
-\zx-calculus in two dimensions. The first is to expand into complete
+\zx-calculus in two respects. The first is to expand into complete
and universal qudit variations to work effectively beyond 2-level
systems, and the second is to gain a deeper understanding of the role
played by W-type tensors as they interact with the generators of the
\zx-calculus, which are themselves of GHZ-type.
-While in the early stages of the project, it will already be quite useful to study concrete diagrams of fixed size (e.g. a quantum circuit on $N$ qubits for a previously-fixed $N$), in task \ref{task:betterboxes}, we will extend \azx to support parametrised families of diagrams (e.g. quantum circuits with $N$ qubits where $N$ can vary) mirroring the control structures present in a quantum HLL. This will enable more sophisticated, generic optimisations to be run in advance of needing any particular computational procedure.
+Error correction should be performed automatically. We have extensive
+experience in treating error correcting codes in the \zxcalculus
+\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
@@ -821,14 +832,32 @@ 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.}
+modes.
+
\subsubsection{Machine-dependent optimisation}
\label{sec:comp-quant-softw}
-\oldt{An \azx term produced by the compiler front-end is, by design, an
+\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
@@ -836,55 +865,22 @@ abstractly-described procedures to code that can run on realistic
machines is a key objective for the project. WP4 is responsible for
developing the tools to do so. This work package represents the most
technically involved and multi-disciplinary component of the \azx
-project, requires the integration of the theoretical work of
-\ref{wp:theory} and generalisation from the specific machines
-considered in \ref{wp:backends}, and will result in software forming
-the basis of a general-purpose quantum compiler.
-
-We identify three main tasks: to add suitable error protection to the
-program; to optimise the program according to whichever resources are
-most appropriate for the given machine; and to layout the program for
+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.
-Error correction should be performed automatically. We have extensive
-experience in treating error correcting codes in the \zxcalculus
-\cite{Duncan:2013lr,Chancellor2016Coherent-Parity,BH-2017,Garvie2017Verifying-the-S}.
-Similar techniques will enable translating from ``raw'' \azx terms to
-error corrected / fault-tolerant versions of the same program;
-additional annotations will be added to ensure that other program
-transformations do not break the fault-tolerance.
-We identify two kinds of optimisation. First, generic,
-model-independent optimisations work on the raw tensor network,
-typically by reducing its graph complexity, or by minimising the
-number of non-Clifford operations in the graph. This draws on
-\ref{task:algorithms} and could be applied before the target hardwaere
-is known. Second, optimisations which take into
-account the resource models of a specific machine, expressed through
-annotations, cf.~\ref{task:annotate2}. This might be applied before
-or after layout, depending on the circumstances. Layout will be handled
-in a similar way to this second kind of optimisation, generalising
-from \ref{task:delft-model} and \ref{task:NQIT-model}.
-
-Although we will provide specific modules for the tasks described above, the
-\azx system is intended to extensible, so we will also publish an open
-API and specification language to simplify the task of adding new
-architectures and error correcting schemes to the system
-(\ref{task:backendapi}).
-
-The tasks to be performed within WP4 may be broadly described in terms of how the \azx compiler will transform \zx terms produced by the front-end to obtain instructions to be realised by a quantum computer (or software quantum simulator) at the back-end.
-These stages are: (i)~an initial round of generic, hardware-independent optimisations; (ii)~application of some choice of strategy for error correction; (iii)~translation to a specialised annotation system which represents the parameters and constraints of a specific hardware implementation; and finally (iv)~another round of optimisation within the constraints imposed by the error correction and hardware models.
-In addition to the development of the tools for these stages, WP4 will develop an interface for the specification of the annotation systems used in stages (iii) and~(iv) above, allowing for easy extension of the \azx compiler to arbitrary hardware systems and allowing \azx to act as a general-purpose quantum compiler.
-
-The first stage of the compilation process represents a ``generic optimisation'' subroutine (\ref{task:basic-opt}), which may be applied to arbitrary \zx terms.
-This subroutine will re-write \zx terms into ones with fewer resources in a broadly applicable sense, such as fewer total nodes or fewer nodes which realise non-Clifford transformations (for instance, corresponding to $T$ gates).
-This may be developed independently of the results of WP1 or WP2 using existing techniques (as well as incorporating any further useful techniques developed in \ref{task:axioms} and~\ref{task:algorithms}).
-
-The second stage of the compilation process is to take a generic \zx term expressing a computation on idealised quantum systems, and re-write it as a \zx term representing an equivalent transformation of error-corrected qubits (\ref{task:ECC}).
-As well as the \zx terms to translate, this will take as input a specification the particular error correction code or other fault-tolerance construction to apply.
-
-
-
The third stage of the compilation process attempts to map a \zx term into an equivalent \zx term which closely models the constraints of a target architecture (\ref{task:runnable}).
This represents the core of the compilation process, taking \zx terms representing a procedure in an abstract model of quantum computation such as circuits or MBQC patterns (with or without error correction), and mapping them into a form which conforms to the physical constraints of a specific hardware implementation.
Particular implementations are specified by a system of annotations provided by the development environment, consisting of an ``architecture-targeted annotation'' (or ArcTAn) system.
@@ -895,8 +891,9 @@ This will involve the development of a theory of re-writing techniques developed
By performing a final round of optimisations using a theory of rewrites which apply to all ArcTAn annotation systems, we aim to make possible a reduction in the resources used in any particular hardware platform without requiring the use of bespoke techniques for each target architecture.
Annotation systems representing the hardware implementation are to be provided by the development environment, using a standardised interface.
-By providing public documentation for this interface~(\ref{task:backendapi}), we enable third-party developers to extend the functionality of the \azx compiler to arbitrary platforms, thus ensuring the suitability of the \azx compiler as part of a general-purpose quantum software development platform.}
+By providing public documentation for this interface~(\ref{task:backendapi}), we enable third-party developers to extend the functionality of the \azx compiler to arbitrary platforms, thus ensuring the suitability of the \azx compiler as part of a general-purpose quantum software development platform.
+\benREM{Missing discussion on the hardware: T4.1 and T4.2.}
\subsection{Interdisciplinary nature}
\label{sec:interd-nature}
@@ -1340,18 +1337,16 @@ In the first instance we make contact between \zx and standard circuit and measu
%%%
%%%%%%%WP 2
%%%
-\begin{WP}{Representation and Reasoning in \zx}{1M}{36M}{wp:backends}
+\begin{WP}{Representation, reasoning, and resources in \zx}{1M}{36M}{wp:backends}
\WPleaderPOL
\WPeffort{0}{0}{0}{0}{0}{0}
\begin{WPaim}
-We build the theoretical foundations for \zx as an IR. This includes extending the capabilities of \zx to represent universal algorithms, control flows, and \ldots . We identify and develop annotations in \zx for relevant computational resources, which will then be used for subsequent machine (in)dependent optimisation protocols.
+We build the theoretical foundations for \zx as an intermediate representation. This includes extending the capabilities of \zx to represent mixed states, qudit states, and control flows. We use \zx axiomatisations and automated theorem provers to extract out post-classical computing resources, which will be used both for further optimisation work, and for characterisation of quantum algorithmic speed-up.
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:axioms}]{Beyond qubits and stabilisers
(M1--M12; Responsible: 2; Involved: 1,3,5)}{%
- We will exploit recently achieved completeness results for
- \zxcalculus to get both convenient and powerful presentations for
- Clifford+T and fully universal families of diagrams. We will
+ We will exploit further the recent completeness results to give representations for mixed state qubit quantum theory. We will
extend the \textsc{zx} tensor formalism from the qubit domain to
higher dimensions.
% and exploit the translation from \textsc{zx}- to \textsc{zw}-calculus.
@@ -1364,13 +1359,15 @@ We build the theoretical foundations for \zx as an IR. This includes extending t
of diagrams, e.g. for expressing and transforming regular families
of circuits.
}
- \WPtask[\label{task:resources}]{Resources
+ \WPtask[\label{task:resources}]{Resources and axioms
(M1--M18; Responsible: 1; Involved: 2,3,5)}{%
-Placeholder for stuff that's primarily Belen's.
+We will exploit the three axiom sets for Clifford, Clifford+T, and universal qubit QM,
+to identify and distill specific resources that are necessary to quantum speed-up. In particular, to focus on finding multiple resource elements (rather than simply magic states), and to characterise post-classical composition as a resource.
+This includes developing \zx representations of contextuality, as a possible post-classical resource.
}
- \WPtask[\label{task:resourcesagain}]{Other stuff
+ \WPtask[\label{task:resourcesagain}]{Computational resources
(M1--M18; Responsible: 1; Involved: 2,3,5)}{%
-Further placeholder for stuff that's primarily Belen's.
+We will use the existing graph re-writing and automated theorem proving tools of Quantomatic and PyZX to determine parts of the re-writing process that are difficult to compute classically. This will then be used to extract candidate subroutines for sources of quantum speed-up. Along with the previous task, these will be used to develop procedures for characterising if a \zx-represented algorithm demonstrates speed-up or not.
}
\end{WPtasks}
@@ -1947,7 +1944,7 @@ and non-locality in categorical quantum mechanics. LiCS 2012. IEEE Computer Soci
% to 5 relevant publications, and/or products, services
% (incl. widely-used datasets or software), or other achievements
% relevant to the call content. }
- \textbf{Prof.\ Bob Coecke} pioneered categorical and diagrammatic methods for quantum computing (1), and \zxcalculus\ in particular (with Duncan) (2). He is/has supervised approx.~40 PhD students, which include Ng and Wang who recently proved universal completeness of the \zx-calculus \cite{NgWang}, and included Backens who proved stabiliser completeness \cite{1367-2630-16-9-093021}. He co-authored \em Picturing Quantum Processes \em (3), which presents diagrammatic methods for quantum computing to a broader audience.
+ \textbf{Prof.\ Bob Coecke} pioneered categorical and diagrammatic methods for quantum computing (1), and \zxcalculus\ in particular (with Duncan) (2). He is/has supervised approx.~40 PhD students, which include Ng and Wang who recently proved universal completeness of the \zx-calculus \cite{NW-2017}, and included Backens who proved stabiliser completeness \cite{1367-2630-16-9-093021}. He co-authored \em Picturing Quantum Processes \em (3), which presents diagrammatic methods for quantum computing to a broader audience.
\textit{\color{gray} \textbf{Publications:} (1) Samson Abramsky and ---. A categorical semantics of quantum protocols. In LICS 2004. IEEE Computer Society, 2004. (2) Bob Coecke and Ross Duncan. Interacting quantum observables: Categorical algebra and
diagrammatics. New J. Phys, 13(043016), 2011. (3) --- and A. Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017.}
@@ -2447,3 +2444,8 @@ with very large graphs.
}
\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/NEWPROPOSAL/preamble.tex b/NEWPROPOSAL/preamble.tex
index 7b485e11959dfda09b672a2a7de44a178300949e..3136e491787b37e6440a6804b72c0e1edafe5344 100644
--- a/NEWPROPOSAL/preamble.tex
+++ b/NEWPROPOSAL/preamble.tex
@@ -24,6 +24,8 @@
\def\e{\end{color}\xspace}
\newcommand{\TODOb}[1]{\marginpar{\scriptsize\bB \textbf{TODO:} #1\e}}
\newcommand{\oldt}[1]{{\color{blue} #1}}
+\newcommand{\newt}[1]{{\color{blue!50!red} #1}}
+
% typographical improvements
\usepackage[T1]{fontenc}
@@ -272,8 +274,10 @@
\newcommand{\zx}{\textsc{zx}\xspace}
\newcommand{\zxcalculus}{\textsc{zx}-calculus\xspace}
-\newcommand{\azx}{\textsc{azx}\xspace}
-\newcommand{\liquid}{LIQUi$\ket{}$\xspace}
+\newcommand{\azx}{\texttt{\bfseries\color{red!70!black}AZX}\xspace}
+\newcommand{\liquid}{\texttt{\bfseries\color{red!70!black}Q\#}\xspace}
+
+\newcommand{\benREM}[1]{\texttt{\bfseries\color{red!70!black} [{#1}]}\xspace}
\usepackage{pgfgantt}
diff --git a/NEWPROPOSAL/quantera.bib b/NEWPROPOSAL/quantera.bib
index 27c0222b895843dad725c368247bbf7675cfc48c..a5fdc7e21b7da3fad2c18be75bda44d92c899ee1 100644
--- a/NEWPROPOSAL/quantera.bib
+++ b/NEWPROPOSAL/quantera.bib
@@ -168,7 +168,7 @@
Author = {Andrew W. Cross and Lev S. Bishop and John A. Smolin and Jay M. Gambetta},
Date-Added = {2017-03-05 21:01:08 +0000},
Date-Modified = {2017-03-05 21:03:10 +0000},
- Howpublished = {\url{https://github.com/IBM/qiskit-openqasm/blob/master/spec/qasm2.pdf}},
+ Howpublished = {\url{https://arXiv.org/abs/arXiv:1707.03429}},
Keywords = {QASM, quantum computing, programming language},
Month = {January},
Title = {Open Quantum Assembly Language},
@@ -3766,32 +3766,41 @@ well.},
Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8Qai4uLy4uLy4uLy4uLy4uL0RvY3VtZW50cy9SZWFkaW5nL1NjaWVuY2UvcGFwZXJzL0tlbGx5L1N0YXRlIHByZXNlcnZhdGlvbiBieSByZXBldGl0aXZlIGVycm9yIGRldGVjdGlvbi5wZGbSFwsYGVdOUy5kYXRhTxECUAAAAAACUAACAAAMTWFjaW50b3NoIEhEAAAAAAAAAAAAAAAAAAAAzpiHAkgrAAAAIJRBH1N0YXRlIHByZXNlcnZhdGlvbiBiI0EzNEZDRi5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAACjT8/RHQd8AAAAAAAAAAAABQAGAAAJIAAAAAAAAAAAAAAAAAAAAAVLZWxseQAAEAAIAADOmHjyAAAAEQAIAADRHPlsAAAAAQAcACCUQQAnAxkAJwMYACcDFwAKjkUACo5EAAJkfAACAGlNYWNpbnRvc2ggSEQ6VXNlcnM6AGt3YjEzMjE1OgBEb2N1bWVudHM6AFJlYWRpbmc6AFNjaWVuY2U6AHBhcGVyczoAS2VsbHk6AFN0YXRlIHByZXNlcnZhdGlvbiBiI0EzNEZDRi5wZGYAAA4AagA0AFMAdABhAHQAZQAgAHAAcgBlAHMAZQByAHYAYQB0AGkAbwBuACAAYgB5ACAAcgBlAHAAZQB0AGkAdABpAHYAZQAgAGUAcgByAG8AcgAgAGQAZQB0AGUAYwB0AGkAbwBuAC4AcABkAGYADwAaAAwATQBhAGMAaQBuAHQAbwBzAGgAIABIAEQAEgBqVXNlcnMva3diMTMyMTUvRG9jdW1lbnRzL1JlYWRpbmcvU2NpZW5jZS9wYXBlcnMvS2VsbHkvU3RhdGUgcHJlc2VydmF0aW9uIGJ5IHJlcGV0aXRpdmUgZXJyb3IgZGV0ZWN0aW9uLnBkZgATAAEvAAAVAAIAD///AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAPsBAAEIA1wDXgNjA24DdwOFA4kDkAOZA54DqwOuA8ADwwPIAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAA8o=},
Bdsk-Url-1 = {http://dx.doi.org/10.1038/nature14270}}
-@article{export:209634,
- Abstract = {Languages, compilers, and computer-aided design tools will be essential for
- scalable quantum computing, which promises an exponential leap in our ability to
- execute complex tasks. LIQUi|> is a modular software architecture designed to
- control quantum hardware. It enables easy programming, compilation, and
- simulation of quantum algorithms and circuits, and is independent of a specific
- quantum architecture. LIQUi|> contains an embedded, domain-specific language
- designed for programming quantum algorithms, with F{\#} as the host language. It
- also allows the extraction of a circuit data structure that can be used for
- optimization, rendering, or translation. The circuit can also be exported to
- external hardware and software environments. Two different simulation
- environments are available to the user which allow a trade-off between number of
- qubits and class of operations. LIQUi|> has been implemented on a wide range
- of runtimes as back-ends with a single user front-end. We describe the
- significant components of the design architecture and how to express any given
- quantum algorithm.},
- Author = {Dave Wecker and Krysta M. Svore},
- Date-Added = {2015-02-06 16:40:20 +0000},
- Date-Modified = {2015-02-06 16:41:57 +0000},
- Eprint = {arXiv:1402.4467},
- Month = {February},
- Title = {LIQUi|>: A Software Design Architecture and Domain-Specific Language for Quantum Computing},
- Url = {http://research.microsoft.com/apps/pubs/default.aspx?id=209634},
- Year = {2014},
- Bdsk-File-1 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QdS4uLy4uLy4uLy4uLy4uL0RvY3VtZW50cy9SZWFkaW5nL1NjaWVuY2UvcGFwZXJzL1dlY2tlci9MSVFVaXw+IEEgU29mdHdhcmUgRGVzaWduIEFyY2hpdGVjdHVyZSBhbmQgRG9tYWluLVNwZWNpZmljLnBkZtIXCxgZV05TLmRhdGFPEQJwAAAAAAJwAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAADOmIcCSCsAAACcKFAfTElRVWl8PiBBIFNvZnR3YXJlIEQjOUMyMjQ0LnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAJwiRNBRHfEAAAAAAAAAAAAFAAYAAAkgAAAAAAAAAAAAAAAAAAAABldlY2tlcgAQAAgAAM6YePIAAAARAAgAANBRAdEAAAABABwAnChQACcDGQAnAxgAJwMXAAqORQAKjkQAAmR8AAIAak1hY2ludG9zaCBIRDpVc2VyczoAa3diMTMyMTU6AERvY3VtZW50czoAUmVhZGluZzoAU2NpZW5jZToAcGFwZXJzOgBXZWNrZXI6AExJUVVpfD4gQSBTb2Z0d2FyZSBEIzlDMjI0NC5wZGYADgB+AD4ATABJAFEAVQBpAHwAPgAgAEEAIABTAG8AZgB0AHcAYQByAGUAIABEAGUAcwBpAGcAbgAgAEEAcgBjAGgAaQB0AGUAYwB0AHUAcgBlACAAYQBuAGQAIABEAG8AbQBhAGkAbgAtAFMAcABlAGMAaQBmAGkAYwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAdVVzZXJzL2t3YjEzMjE1L0RvY3VtZW50cy9SZWFkaW5nL1NjaWVuY2UvcGFwZXJzL1dlY2tlci9MSVFVaXw+IEEgU29mdHdhcmUgRGVzaWduIEFyY2hpdGVjdHVyZSBhbmQgRG9tYWluLVNwZWNpZmljLnBkZgAAEwABLwAAFQACAA///wAAgAbSGxwdHlokY2xhc3NuYW1lWCRjbGFzc2VzXU5TTXV0YWJsZURhdGGjHR8gVk5TRGF0YVhOU09iamVjdNIbHCIjXE5TRGljdGlvbmFyeaIiIF8QD05TS2V5ZWRBcmNoaXZlctEmJ1Ryb290gAEACAARABoAIwAtADIANwBAAEYATQBVAGAAZwBqAGwAbgBxAHMAdQB3AIQAjgEGAQsBEwOHA4kDjgOZA6IDsAO0A7sDxAPJA9YD2QPrA+4D8wAAAAAAAAIBAAAAAAAAACgAAAAAAAAAAAAAAAAAAAP1},
- Bdsk-Url-1 = {http://research.microsoft.com/apps/pubs/default.aspx?id=209634}}
+@inproceedings{qsharp,
+ title={Q\#: Enabling scalable quantum computing and development with a high-level domain-specific language},
+ author={Krysta M. Svore and Alan Geller and Matthias Troyer and John Azariah and Christopher Granade and Bettina Heim and Vadym Kliuchnikov and Mariia Mykhailova and Andres Paz and Martin Roetteler},
+ booktitle={Proceedings of the Real World Domain Specific Languages Workshop (RWDSL 2018)},
+ preprint={arXiv:1803.00652},
+ year=2018
+}
+
+@article{JPV-2018,
+ author={Emmanuel Jeandel and Simon Perdrix and Renaud Vilmart},
+ title={Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics},
+ year=2018,
+ preprint={arXiv:1801.10142}
+}
+
+@article{NW-2018,
+ author={Kang Feng Ng and Quanlong Wang},
+ title={Completeness of the ZX-calculus for Pure Qubit Clifford+T Quantum Mechanics},
+ year=2018,
+ preprint={arXiv:1801.07993}
+}
+
+@article{NW-2017,
+ author={Kang Feng Ng and Quanlong Wang},
+ title = {A universal completion of the ZX-calculus},
+ year=2017,
+ preprint={arXiv:1706.09877}
+}
+
+@article{DKPdW-2019,
+ author={Ross Duncan, Aleks Kissinger, Simon Pedrix, John van de Wetering},
+ title={Graph-theoretic Simplification of Quantum Circuits with the {ZX}-calculus},
+ year=2019,
+ preprint={arXiv:1902.03178}
+}
@article{Raphael-Dias-da-Silva:2013aa,
Abstract = {One of the main goals in quantum circuit optimisation is to reduce the number of ancillary qubits and the depth of computation, to obtain robust computation. However, most of known techniques, based on local rewriting rules, for parallelising quantum circuits will require the addition of ancilla qubits, leading to an undesired space-time tradeoff. Recently several novel approaches based on measurement-based quantum computation (MBQC) techniques attempted to resolve this problem. The key element is to explore the global structure of a given circuit, defined via translation into a corresponding MBQC pattern. It is known that the parallel power of MBQC is superior to the quantum circuit model, and hence in these approaches one could apply the MBQC depth optimisation techniques to achieve a lower depth. However, currently, once the obtained parallel pattern is translated back to a quantum circuit, one should either increase the depth or add ancilla qubits. In this paper we characterise those computations where both optimisation could be achieved together. In doing so we present a new connection between two MBQC depth optimisation procedures, known as the maximally delayed generalised flow and signal shifting. This structural link will allow us to apply an MBQC qubit optimisation procedure known as compactification to a large class of pattern including all those obtained from any arbitrary quantum circuit. We also present a more efficient algorithm (compared to the existing one) for finding the maximally delayed generalised flow for graph states with flow.},