\RequirePackage[l2tabu,orthodox]{nag}
\documentclass[11pt,a4paper]{article}
\usepackage{etex}



%%%% do rwd stuff %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pdfoutput=1
\usepackage{rwd-drafting}
%\input{margins.tex}
\input{preamble.tex}

\begin{document}

\title{\projtitle}  % defined in preamble
\author{\small{Ross Duncan}}
\def\subtitle{QUANTERA PRE-PROPOSAL}
\date{}
\maketitle


\begin{abstract}
  This document is for discussion and to define objectives and
  work packages.  
\end{abstract}

\section{Overview}
\label{sec:overview}

At present there are many projects which aim to develop a scalable
quantum computer, using many different architectures and underlying
physical implementations, each having their own particular
characteristics.  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.

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, which has already been
used for similar things.

\section{Consortium}
\label{sec:consortium}

At present we have six partners in three countries.

\subsection{UK}
\label{sec:uk}

Total UK budget is set by EPSRC as ``\pounds2M split between 3--8
projects''

\subsubsection{Strathclyde}
\label{sec:strathclyde}

People:
\begin{itemize}
\item Ross Duncan (PI);
\item Postdoc (to be hired)
\end{itemize}
Possible coinvestigators:
\begin{itemize}
\item Daniel Oi  (hybrid quantum systems)
\item Jonathan Pritchard (quantum interfaces)
\item Conor McBride (programming languages, type theory)
\end{itemize}

\subsubsection{Oxford}
\label{sec:oxford}

People:
\begin{itemize}
\item Samson Abramsky 
\item Bob Coecke 
\item Jamie Vicary 
\item Sam Statton 
\item ?Niel de Beaudrap? 
\item Post doc (to be hired)
\end{itemize}

Possible Coinvestigators:
\begin{itemize}
\item Simon Benjamin (scalable quantum architecture, NQIT)
\end{itemize}

\subsubsection{External people}
\label{sec:external-people}

?Winfried Hensinger? (Sussex) (Scalable ion trap architecture)

\subsection{France}
\label{sec:france}

Total budget for French sites is capped at \euro 400k.  I don't know
how this maps out to hiring people, but there should be at least one
postdoc.  Given the low budget it may make more sense for one of the
French sites to become a subsite.

\subsubsection{Nancy}

\begin{itemize}
\item Simon Perdrix
\end{itemize}

\subsubsection{Orsay}

\begin{itemize}
\item Benoit Valiron
\end{itemize}

\subsubsection{ATOS-Bull}

\begin{itemize}
\item Cyril Allouche
\end{itemize}

\subsection{Netherlands}
\label{sec:netherlands}

Dutch budget capped at \euro 250k.

\subsubsection{Nijmegen}
\label{sec:nijmegen}

\begin{itemize}
\item Aleks Kissinger
\item Post-doc to be hired.
\end{itemize}

\subsubsection{External}
\label{sec:external}

QuTech Delft -- superconducting qubits people?

\subsection{Not Europe}
\label{sec:not-europe}

QuantERA cannot pay people outside the EU, but if they fund themselves
then outside partners are allowed.  Some ideas:
\begin{itemize}
\item Peter Selinger (Dalhousie, Canada)
\item Will Zeng (Rigetti, USA)
\item Krista Svore / Martin  Roteller (Microsoft, USA)
\end{itemize}

\section{Objectives and WPs}

\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}