From 7f8cfa4ed1c7ec535e4e5f5193c0cbba4c98032d Mon Sep 17 00:00:00 2001
From: qwang <Quanlong.Wang@cs.ox.ac.uk>
Date: Fri, 15 Feb 2019 10:59:07 +0000
Subject: [PATCH] add description for circuit optimisation
---
NEWPROPOSAL/FULLPROP.tex | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index dad3354..c833d70 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -229,7 +229,7 @@ easily run existing programs, and future programming languages automatically gai
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.
+computations.
% and is complete for important subtheories such as the stablizer
% fragment \cite{1367-2630-16-9-093021} and single qubit Clifford+T
@@ -255,7 +255,7 @@ An example of such a transformation is the following:}
%\cnotv[0.6] \rTo^*
\cnotvi[0.7]
\]~\\[-4mm]%
-Members of our consortium have demonstrated how to use these formal reasoning techniques in 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 \newt{outperform other methods of circuit optimisation}.
+Members of our consortium have demonstrated how to use these formal reasoning techniques in 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 \newt{outperform other methods of circuit optimisation, in the sense that certain circuit metric (such as total size, tree-width, or number of non-Clifford subterms such as T-gates) can be minimised.}
\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
--
GitLab