first update of WP2

NEWPROPOSAL/FULLPROP.aux

@@ -91,8 +91,8 @@
 \citation{Raussendorf-2001}
 \@writefile{toc}{\contentsline {subsubsection}{\numberline {1.3.1}A quantum compiler stack}{6}{subsubsection.1.3.1}}
 \newlabel{sec:progr-lang-supp}{{1.3.1}{6}{A quantum compiler stack}{subsubsection.1.3.1}{}}
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.3.2}Representation and reasoning}{6}{subsubsection.1.3.2}}
-\newlabel{sec:machines-models}{{1.3.2}{6}{Representation and reasoning}{subsubsection.1.3.2}{}}
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.3.2}Representation, reasoning, and resources}{6}{subsubsection.1.3.2}}
+\newlabel{sec:machines-models}{{1.3.2}{6}{Representation, reasoning, and resources}{subsubsection.1.3.2}{}}
 \citation{Jeandel2017A-Complete-Axio}
 \citation{NgWang}
 \citation{PhysRevX.4.041041}

NEWPROPOSAL/FULLPROP.log

-This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (preloaded format=pdflatex 2019.2.1)  11 FEB 2019 17:35
+This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (preloaded format=pdflatex 2019.2.1)  11 FEB 2019 19:06
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -2170,7 +2170,7 @@ Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 2325.
 Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 2325.
 
 Package rerunfilecheck Info: File `FULLPROP.out' has not changed.
-(rerunfilecheck)             Checksum: 5325BCA331EF553F5681244BEE887C6C;1832.
+(rerunfilecheck)             Checksum: 0FAC8025A541D49D6B1F8D754EEA3226;1844.
 
 
 LaTeX Font Warning: Some font shapes were not available, defaults substituted.
@@ -2186,7 +2186,7 @@ Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 2325.
 Here is how much of TeX's memory you used:
  37879 strings out of 492649
  864709 string characters out of 6129623
- 1156244 words of memory out of 5000000
+ 1156256 words of memory out of 5000000
  40582 multiletter control sequences out of 15000+600000
  107870 words of font info for 225 fonts, out of 8000000 for 9000
  1141 hyphenation exceptions out of 8191
@@ -2213,7 +2213,7 @@ exmf-dist/fonts/type1/public/lm/lmsy8.pfb></usr/local/texlive/2018/texmf-dist/f
 onts/type1/public/lm/lmtt10.pfb></usr/local/texlive/2018/texmf-dist/fonts/type1
 /public/lm/lmtt9.pfb></usr/local/texlive/2018/texmf-dist/fonts/type1/public/ams
 fonts/symbols/msam7.pfb>
-Output written on FULLPROP.pdf (32 pages, 555028 bytes).
+Output written on FULLPROP.pdf (32 pages, 555551 bytes).
 PDF statistics:
  830 PDF objects out of 1000 (max. 8388607)
  740 compressed objects within 8 object streams

NEWPROPOSAL/FULLPROP.out

@@ -3,7 +3,7 @@
 \BOOKMARK [2][-]{subsection.1.2}{Novelty, level of ambition and foundational character}{section.1}% 3
 \BOOKMARK [2][-]{subsection.1.3}{Concept and methodology}{section.1}% 4
 \BOOKMARK [3][-]{subsubsection.1.3.1}{A quantum compiler stack}{subsection.1.3}% 5
-\BOOKMARK [3][-]{subsubsection.1.3.2}{Representation and reasoning}{subsection.1.3}% 6
+\BOOKMARK [3][-]{subsubsection.1.3.2}{Representation, reasoning, and resources}{subsection.1.3}% 6
 \BOOKMARK [3][-]{subsubsection.1.3.3}{Machine-independent optimisation}{subsection.1.3}% 7
 \BOOKMARK [3][-]{subsubsection.1.3.4}{Machine-dependent optimisation}{subsection.1.3}% 8
 \BOOKMARK [2][-]{subsection.1.4}{Interdisciplinary nature}{section.1}% 9

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
@@ -711,7 +711,7 @@ public.}
 
 
 
-\subsubsection{Representation and reasoning}
+\subsubsection{Representation, reasoning, and resources}
 \label{sec:machines-models}
 
 \REM{stuff about WP 2 here}
@@ -1340,18 +1340,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 IR. 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 +1362,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 distill specific resources that are necessary to quantum speed-up. 
+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}