diff --git a/NEWPROPOSAL/FULLPROP.aux b/NEWPROPOSAL/FULLPROP.aux
index 493fd0964debaf3b6035590f075d679583dcbe4d..a88e8da3869cd9972bcf7bd648bf04fb36ac4dcb 100644
--- a/NEWPROPOSAL/FULLPROP.aux
+++ b/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}
diff --git a/NEWPROPOSAL/FULLPROP.log b/NEWPROPOSAL/FULLPROP.log
index fa2405dd27efb38eaf2bce9aca6e1d80ff3dede7..339a6eb9b302d265e0479e8af13af734fba4dd0b 100644
--- a/NEWPROPOSAL/FULLPROP.log
+++ b/NEWPROPOSAL/FULLPROP.log
@@ -1,4 +1,4 @@
-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
diff --git a/NEWPROPOSAL/FULLPROP.out b/NEWPROPOSAL/FULLPROP.out
index 6871c9f11584c88e89b6480a4c4baedcbfd9729f..bd173562c41e501241eed74eeea0a755db1a8b33 100644
--- a/NEWPROPOSAL/FULLPROP.out
+++ b/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
diff --git a/NEWPROPOSAL/FULLPROP.pdf b/NEWPROPOSAL/FULLPROP.pdf
index d059af80fba79c218340bdebc6b1cd535dd96f93..84ee809b834a7df7b7062cc539c9617f60719697 100644
Binary files a/NEWPROPOSAL/FULLPROP.pdf and b/NEWPROPOSAL/FULLPROP.pdf differ
diff --git a/NEWPROPOSAL/FULLPROP.synctex.gz b/NEWPROPOSAL/FULLPROP.synctex.gz
index 2f91be598eb50f47188e8ab6519b6ecfcc5028da..4e6ec7436808c0a7aea5828319efd8258a76d26e 100644
Binary files a/NEWPROPOSAL/FULLPROP.synctex.gz and b/NEWPROPOSAL/FULLPROP.synctex.gz differ
diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 3dc11d86e71a2639710344a6450bbf8e5c800cc9..69d29db295b2c074828a18344f5ad5039dac567f 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
@@ -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}