Merge branch 'master' of https://gitlab.cis.strath.ac.uk/kwb13215/quantera-2

NEWPROPOSAL/FULLPROP.tex

@@ -295,9 +295,11 @@ compilers for quantum software.
 \label{sec:contr-theme-addr}
 
 We specifically address the theme of \emph{Quantum Computation}.
-We 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.
+We develop tools for running quantum programs
+on any available quantum device and benchmarking algorithms and machines, significantly 
+enhancing the capabilities of near-term quantum computers.
+
+% 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}
@@ -310,100 +312,27 @@ This will speed new quantum devices and architectures into use, and broaden the
     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}
 
-  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 \newt{as illustrated in the figure on the previous page}.
-  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.}
+The concept of a `deep' quantum compiler is entirely novel. Integrating optimisation and error correction intelligently into the stack gives a completely new set of tools for developing and using quantum computers.
+  Using the \zxcalculus to manage resources in quantum hardware is a totally new application of the \zxcalculus, and an ambitious new way to realise computations on heterogenous 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, helping us to achieve optimal implementations on diverse architectures.
+Furthermore, our system allows transformations of tensor networks which cannot be expressed as equations between circuits as illustrated in the figure on the previous page.
+  In addition, the \zxcalculus is a sound and complete formal system for transforming quantum procedures, so that each program transformation which our compiler system comes with a proof of its correctness.
+  The way that the \zxcalculus represents quantum procedures also 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.
+The categorisation of multiple post-classical resources is also novel, as is the incorporation into the compiler chain. The development of a compiler stack that also doubles as a benchmarking tool is entirely new.
 
 
 \paragraph{Ambition:}
 \label{sec:ambition}
 
-  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; but 
-  \item
-    such that the result is a tightly integrated piece of software upon compilation, and well-tailored to the specific resources, architecture, control systems, and hardware of a specific platform.
-  \end{itemize}
+  A ``deep compiler'' for quantum computing systems allows for modular design of the software stack. This lets programmers write at a high level for any hardware and any quantum error correcting codes. It is nevertheless tightly integrated upon compilation. In addition, it is fully tailored to the specific resources, architecture, control systems, and hardware of a specific platform. Furthermore the project includes isolating, integrating, and then certifying quantum speed-up.
   %\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.
+  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, and the ideal combination of skills within the project consortium.
 
-\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}
@@ -413,17 +342,15 @@ of logical qubits.
 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 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}.
+The ability to demonstrate quantum speed-up at compile-time will enhance our understanding of quantum information.
+The deep quantum compiler we will develop
+will do the heavy lifting of managing resources and mapping operations to quantum hardware, %allowing the developers of both hardware and software to focus elsewhere.
+%This will 
+facilitating the development of new architectures and technologies for quantum computing.
+A key example, exploited by NQIT and others, is that lattice surgery operations on surface codes do not fit into the gate model, but have 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}