article.tex

\RequirePackage[l2tabu,orthodox]{nag}
\documentclass[a4paper]{article}
\bibliographystyle{plain}

\pdfoutput=1

\usepackage{rwd-drafting}

\input{preamble.tex}
\input{tikzpreamble.tex}
\input{quantumcircuits.tex}

\input{front-matter.tex}

\begin{document}
% For article.cls abstract goes here 
% other classes may have it in front-matter
\maketitle
\input{abstract.tex}


\section{Introduction}
\label{sec:intro}

\section{Circuits and 2-PROPS}
\label{sec:prelim}

We assume that the reader is familiar with the notion of symmetric
monoidal category; a standard reference is
\cite{MacLane:CatsWM:1971}.  

\begin{definition} \label{def:PROP}
  A \emph{PROP} is strict symmetric monoidal category whose objects
  are the natural numbers, and where the action of the tensor product on
  objects is given by addition.
\end{definition}

PROPs have been used to formalise many algebraic structures
\cite{Lack:2004sf}, however our interest here is to formalise a
general notion of \emph{circuit} made by wiring together certain
atomic operations.  With this in mind, a PROP of circuits is
henceforth a PROP freely generated from some monoidal signature; the
members of the signature are called \emph{gates}, and a circuit is
a morphism in such a PROP.

\begin{example} \label{ex:boolean-circs}
  TODO -- boolean circuits
\end{example}

\begin{example} \label{ex:quantum-circs}
  The main example of interest is \Circ, the PROP of quantum circuits.
  Different authors, and different hardware manufacturers, prefer
  different primitive gate sets but the following is typical:
  \[
  \begin{array}{cccccccccc}
    \circZ{{}} & \qquad  & \circX{{}} & \qquad & \circH \\ 
    \vstrut{1.2em}
    Z : 1 \to 1 && X : 1 \to 1 && H : 1 \to 1\\
    \\
    \circbox{R_Z(\theta)} & \qquad & \circCPhase{\theta} & \qquad & \circCX  \\ 
    \vstrut{1.2em}
    R_Z(\theta) : 1 \to 1 &&  \CPhase\theta :2 \to 2 && \CX : 2 \to 2\\
  \end{array}
  \]
  We omit the usual matrix interpretations but these can be found in
  the standard textbook \cite{NieChu:QuantComp:2000}.  Note that in
  this example we actually have an uncountable family of generating
  gates, one for each value $\theta \in [0,2\pi)$.  Unlike the case of
  Boolean circuits all quantum gates have the same number of inputs and
  outputs.  In fact, \Circ is a \dag-PROP and all its but this will not concern
  us here.
\end{example}

\begin{example}  \label{ex:zx-calculus}
  TODO -- zx-calculus
\end{example}

\noindent
Note that all of these examples usually include an equational theory.
We will don't include these equations in the  definition since we will
model them as higher dimensional arrows.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        2-CATEGORY DEFINITION        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{definition}  \label{def:strict-two-cat}
  A \emph{strict} 2-category $\mathcal{C}$ is a category \emph{enriched over
    \textbf{Cat}}, the category of categories, \emph{viz:}
  \begin{itemize}
    \item A category $\mathcal{C}$, whose objects and arrows are known as
      \emph{0-cells} and \emph{1-cells} respectively.
    \item For every pair of objects $A$ and $B$, we have a
      category $\mathcal{C}(A, B)$, whose arrows are known as \emph{2-cells}.
    \item For \emph{2-cells} $\alpha : f \Rightarrow g$ and $\beta : g
      \Rightarrow h$ in $\mathcal{C}(A,B)$ their (vertical) composite is denoted
      $\beta \bullet \alpha : f \Rightarrow h$.
    \item For every 1-cell $f:A\to B$ we denote its identity 2-cell by
      $Id_f:f \Rightarrow f$.
    \item For all \emph{0-cells} $A$, $B$, $C$ a bifunctor $\circ:
      \mathcal{C}(B, C) \times \mathcal{C}(A, B) \to \mathcal{C}(A, C)$ called
      \emph{horizontal composition} of \emph{2-cells}.
  \end{itemize}
\REM{Need here the name for a 2-cat with all \emph{2-cells} invertible;  the
  term 2-groupoid refers to the case where both \emph{1-} and \emph{2-cells} are
  invertible.}
\end{definition}

\noindent
In the following we'll always write $A, B, C$ for \emph{0-cells}, $f,
g, h$ for \emph{1-cells} and $\alpha$, $\beta$, $\gamma$ for
\emph{2-cells}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        2-FUNCTOR DEFINITION        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{definition} \label{def:two-functor}
  A \emph{strict} 2-functor $F$ between two \emph{strict} 2-categories
    $\mathcal{C}$ and $\mathcal{D}$ is
  \begin{itemize}
    \item for all \emph{0-cells} $A \in \mathcal{C}$ a 0-cell $F(A) \in
      \mathcal{D}$
    \item for all \emph{0-cells} $(A, B) \in \mathcal{C}$ a functor $F_{A, B}:
      \mathcal{C}(A, B) \to \mathcal{D}(F(A), F(B))$
  \end{itemize}

  \noindent
  Such that $F$ respect the horizontal and vertical compositions.
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        MONOIDAL 2-CATEGORY DEFINITION        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{definition}\label{def:monoidal-two-cat}
  A \emph{strict} monoidal 2-category $(\mathcal{C}, \otimes, I)$ is a
  strict 2-category with a 2-bifunctor $\otimes: \mathcal{C} \times
  \mathcal{C} \to \mathcal{C}$ such that
  \begin{itemize}
    \item for all \emph{0-cells} $A$
      \[
        A \otimes I = A
      \]
    \item for all \emph{0-cells} $(A, B)$, $I$ is the monoidal unit of
    $\mathcal{C}(A, B)$
  \end{itemize}
  \TODO{Denis: fix this definition}
  \REM{What about the unit object?}
\end{definition}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        INTERCHANGE LAW REMARK        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{remark}[Interchange law]
\TODO{DENIS : please fix this statement.  THe second and third clauses
  are the same.!}
  Since $\circ$ and $\otimes$ are bifunctorial, we have the following
    interchange equations for all \emph{0-cells} $A, B \in \mathcal{C}$ and all
    \emph{2-cells} $\alpha, \beta, \gamma, \delta \in \mathcal{C}(A, B)$
  \begin{align}
    (\alpha \circ \beta) \bullet (\gamma \circ \delta) &= (\alpha \bullet
      \gamma) \circ (\beta \bullet \delta) \\
    (\alpha \otimes \beta) \bullet (\gamma \otimes \delta) &= (\alpha \bullet
      \gamma) \otimes (\beta \bullet \delta)
  \end{align}
  Since $\otimes$ is a 2-functor, we have for all \emph{0-cells} $A, B \in
    \mathcal{C}$ and all \emph{2-cells} $\alpha, \beta, \gamma, \delta \in
    \mathcal{C}(A, B)$
  \[
    (\alpha \otimes \beta) \circ (\gamma \otimes \delta) = (\alpha \circ \gamma)
      \otimes (\beta \circ \delta)
  \]
\end{remark}

Putting the preceding definitions together, a 2-PROP is then a strict
monoidal 2-category whose underlying monoidal 1-category is a PROP, or
equivalently, a strict monoidal 2-category whose 0-cells are generated
by a single object under $\otimes$.


\section{Rewriting systems as 2-PROPS}
\label{sec:rewriting}

As remarked earlier we don't include any equations in our notion of
circuits 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        REWRITING SYSTEM DEFINITION        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{definition}
  Given a free PROP of quantum circuits, we can extend it to a 2-PROP
    $\mathcal{P}$ where
  \begin{itemize}
    \item gates form the set of \emph{1-cells} 
    \item the \emph{2-cells} are generated by a finite set of \emph{rewriting}
      rules such that
    \begin{itemize}
      \item 2 rewriting rules with the same types must be equal
      \item each rewriting rule must be invertible, that is $\mathcal{P}(A, B)$
        is a \emph{groupoid} for all \emph{0-cells} $A, B$
    \end{itemize}
  \end{itemize}
  
  \emph{2-cells} are in general called \emph{rewrite sequence}, but if a rewrite
    sequence has only 1 occurence of a rewrite rule, it is called an
    \emph{atomic rule}.
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        REWRITING SYSTEM EXAMPLE        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\circuitExample}[3]{\inline{%
\begin{tikzpicture}[circuit]
 \node (0) at (0, 0.5) {};
 \node [box] (2) at (1, 0.5) {#1};
 \node (4) at (3, 0.5) {};
 \draw (0) to (2);
 \draw (2) to (4);

 \node (1) at (0, -0.5) {};
 \node [box] (3) at (1, -0.5) {#2};
 \node [box] (5) at (2, -0.5) {#3};
 \node (6) at (3, -0.5) {};
 \draw (1) to (3);
 \draw (3) to (5);
 \draw (5) to (6);
\end{tikzpicture}
}}
\begin{example}
  Let's take the previous quantum circuit example \ref{ex:quantum-circs} and add
    some \emph{noisy gates}, that is, gates which can failed with an $\epsilon$
    probability.
  \[
    \begin{array}{cccccccccc}
      \circZ{{\epsilon}} & \qquad  & \circX{{\epsilon}} & \qquad &
        \circbox{H_\epsilon} \\ 
      \vstrut{1.2em}
      Z_\epsilon : 1 \to 1 && X_\epsilon : 1 \to 1 && H_\epsilon : 1 \to 1
    \end{array}
  \]
  We form a 2-PROP by adding some rewriting rules (we omit the identies)
  \[
    \begin{array}{cccccccc}
      \circZ{{\epsilon}} & \Rightarrow & \circZ{{}} & \alpha : Z_\epsilon
        \Rightarrow Z \\
      \vstrut{1.2em} \\
      \circX{{\epsilon}} & \Rightarrow & \circX{{}} & \beta : X_\epsilon
        \Rightarrow X \\
      \vstrut{1.2em} \\
      \circbox{H_\epsilon} & \Rightarrow & \circH & \gamma : H_\epsilon
        \Rightarrow H
    \end{array}
  \]
  Then, on the circuit
  \[
    \circuitExample{$H_\epsilon$}{$Z_\epsilon$}{$X$}
  \]
  a rewriting sequence can be $(id_{H_\epsilon} \otimes \alpha) \bullet (\beta
    \otimes id_Z) \circ (id \otimes id_X)$ \REM{I'm not sure of the sequence}
  \[
    \circuitExample{$H_\epsilon$}{$Z_\epsilon$}{$X$}
    \xRightarrow{id_{H_\epsilon} \otimes \alpha}
    \circuitExample{$H$}{$Z_\epsilon$}{$X$}
    \xRightarrow{\beta \otimes id_Z}
    \circuitExample{$H$}{$Z$}{$X$}
  \]
  Moreover this sequence is atomic.
\end{example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        REWRITING SYSTEM PROPOSITION 1        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proposition}
  For all rewriting sequences $\alpha: f \Rightarrow g$, $\alpha$ can be writen
  \[
    \alpha = \alpha_1 \bullet \alpha_2 \bullet \alpha_3 \bullet \cdots \bullet
      \alpha_i
  \]
  
  \begin{proof}
    We'll prove it by induction of the size of the rewriting sequence using the
      properties of the bifunctors.
    With a atomic rule, we already have
    \[
      \alpha = \alpha_1
    \]
    For the inductive step let's assume $\beta$ is
    \[
      \alpha = \alpha_1 \bullet \alpha_2 \bullet \alpha_3 \bullet \cdots \bullet
        \beta
    \]
    If $s$ is such that
    \[
      \beta = (\beta_1 \bullet \beta_2) \circ (\beta_3 \bullet \beta_4)
    \]
    Then using the interchange law we can write
    \[
      \beta = (\beta_1 \circ \beta_3) \bullet (\beta_2 \circ \beta_4)
    \]
    So we have 
    \begin{align}
      \alpha &= \alpha_1 \bullet \alpha_2 \bullet \alpha_3 \bullet \cdots
        \bullet (\beta_1 \circ \beta_3) \bullet (\beta_2 \circ \beta_4) \\
      \alpha &= \alpha_1 \bullet \alpha_2 \bullet \alpha_3 \bullet \cdots
        \bullet \alpha_{i - 1} \bullet \alpha_i
    \end{align}
    Otherwise we can always add an identity rewriting rule to get the
      interchange law.
    \begin{align}
      \beta_1 \circ (\beta_3 \bullet \beta_4) &\Rightarrow (\beta_1 \bullet id)
        \circ (\beta_2 \bullet \beta_3) \\
      (\beta_1 \bullet \beta_2) \circ \beta_3 &\Rightarrow (\beta_1 \bullet
        \beta_2) \circ (id \bullet \beta_3)
    \end{align}
    The same is true with
    \[
      \beta = (\beta_1 \bullet \beta_2) \otimes (\beta_3 \bullet \beta_4)
    \]
  \end{proof}
\end{proposition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        REWRITING SYSTEM PROPOSITION 2        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proposition}
  For all rewriting sequences $\alpha: f \Rightarrow g$, $\alpha$ can be writen
  \begin{align}
    \alpha &= \alpha_1 \circ \alpha_2 \circ \alpha_3 \circ \cdots \circ \alpha_j
      \\
    \alpha &= \alpha_1 \otimes \alpha_2 \otimes \alpha_3 \otimes \cdots \otimes
      \alpha_k
  \end{align}
  
  \begin{proof}
    The proof is the same but this time we have to use
    \[
      (\alpha \otimes \beta) \circ (\gamma \otimes \delta) = (\alpha \circ
        \gamma) \otimes (\beta \circ \delta)
    \]
  \end{proof}
\end{proposition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        REWRITING SYSTEM PROPOSITION 2 COROLLARY        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{corollary}
  For all rewriting sequences $r: f \Rightarrow g$, $r$ can be writen
  \[
    \alpha = \alpha_1 \bullet \alpha_2 \bullet \alpha_3 \bullet \cdots \bullet
      \alpha_i
  \]
  Such that for all $i$
  \[
    \alpha_i = \alpha_{i, 1} \circ \alpha_{i, 2} \circ \alpha_{i, 3} \circ
      \cdots \circ \alpha_{i, j}
  \]
  and for all $j$
  \[
    \alpha_{i, j} = \bigotimes_k^l \alpha_{i, j, k}
  \]
  a tensor products of rewriting sequences.
\end{corollary}

\section{Quantale Enriched Categories}
\label{sec:quant-enrich-categ}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        QUANTALE DEFINITION        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{definition}[Quantale $\mathbb{Q}$]
  A quantale is a \emph{lattice} with a binary operator such that for all
    elements of the lattice $x, y$ and $\{x_i\}_i, \{y_i\}_i$
  \begin{align}
    x \oplus \bigvee y_i &= \bigvee x \oplus y_i \\
    \left(\bigvee x_i\right) \oplus y &= \bigvee x_i \oplus y
  \end{align}
  
  We require that for all $x$, it exist $x^{-1}$ such that
  \begin{align}
    x \oplus x^{-1} &= e \\
    x^{-1} \oplus x &= e
  \end{align}
  
  Such a quantale can be seen as a monoidal category over a \emph{group}.
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        Q-ENRICHED CATEGORY DEFINITION        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{definition}[$\mathbb{Q}$-enriched category]
  A $\mathbb{Q}$-enriched category $\mathcal{E}$ is
  
  \begin{itemize}
    \item A set of objects
    \item For all objects $(a, b)$, $\mathcal{E}(a, b) \in \mathbb{Q}$
  \end{itemize}
  
  such that for all objects $a$
  \[
    e \succeq \mathcal{E}(a, a)
  \]
  for all objects (a, b, c)
  \[
    \mathcal{E}(b, c) \oplus \mathcal{E}(a, b) \succeq \mathcal{E}(a, c)
  \]
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        MONOIDAL Q-ENRICHED CATEGORY DEFINITION        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{definition}[Monoidal $\mathbb{Q}$-enriched category]
  $(E, \otimes)$ is strictly monoidal if
  \[
    \mathcal{E}(a, b) \oplus \mathcal{E}(a', b') \succeq \mathcal{E}(a \otimes
      a', b \otimes b')
  \]
  and symmetric if
  \[
    e \succeq \mathcal{E}(a \otimes b, b \otimes a)
  \]
\end{definition}



\section{$\mathbb{Q}$-valued rewriting systems}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        HOMOMORPHISM DEFINITION        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{definition}
  For all $(A, B) \in \mathcal{P}$ we define a homomorphism $V:
    \mathcal{P}(A, B) \to \mathbb{Q}$, such that for all gates $f$
  \[
    V(f) \in \mathbb{Q}
  \]

  On gates
  \begin{align}
    V(f \circ g) &\preceq V(f) \oplus V(g) \\
    V(f \otimes g) &\preceq V(f) \oplus V(g)
  \end{align}
  
  On rewriting sequences
  \begin{align}
    V(\alpha \circ \beta) &= V(\alpha) \oplus V(\beta) \\
    V(\alpha \otimes \beta) &= V(\alpha) \oplus V(\beta) \\
    V(\alpha \bullet \beta) &= V(\alpha) \oplus V(\beta)
  \end{align}

  We all required that for all rewriting rules $\alpha: f \Rightarrow g$
  \[
    V(\alpha) = V(f) \oplus V(g)^{-1}
  \]
  
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        HOMOMORPHISM REMARK        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{remark}
  Note that because
  \[
    V(\alpha: f \Rightarrow g) = V(f) \oplus V(g)^{-1}
  \]
  then
  \begin{align}
    V(\alpha: f \Rightarrow f) &= V(f) \oplus V(f)^{-1} \\
    &= e
  \end{align}
  that is
  \[
    \forall f, V(id_f) = e
  \]
\end{remark}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        HOMOMORPHISM PROPOSITION 1        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proposition}
  Given two rewriting sequence $\alpha, \beta: f \Rightarrow g$, then $V(\alpha)
    = V(\beta)$.
  
  \begin{proof}
    The set of all possible rewriting sequences is freely generated by the set
      of rewriting rules, $\bullet$, $\circ$ and $\otimes$ so both $\alpha$ and
      $\beta$ can be written
    \begin{align}
      \alpha &= \alpha_1 \odot \alpha_2 \odot \alpha_3 \odot \cdots \odot
        \alpha_n \\
      \beta &= \beta_1 \odot \beta_2 \odot \beta_3 \odot \cdots \odot \beta_m
    \end{align}
    with $\odot \in \{\bullet, \circ, \otimes\}$ and for all i $\alpha_i$ and
      $\beta_i$ are rewriting rule.
    If $n = 1$ then $\alpha$ is a rewriting rule, so $V(r) = V(f) \oplus
      V(g)^{-1}$.
    Otherwise
    \begin{align}
      V(\alpha) &= V(\alpha_1 \odot \alpha_2 \odot \cdots \odot \alpha_n) \\
      &= V(\alpha_1) \oplus V(\alpha_2) \oplus \cdots \oplus V(\alpha_n) \\
      &= V(f \Rightarrow h_1) \oplus V(h_1 \Rightarrow h_2) \oplus \cdots \oplus
        V(h_n \Rightarrow g) \\
      &= V(f) \oplus V(h_1)^{-1} \oplus V(h_1) \oplus V(h_2)^{-1} \oplus \cdots
        \oplus V(h_n) \oplus V(g)^{-1}
    \end{align}
    A easy inductive proof can show us that
    \[
      V(f) \oplus V(h_1)^{-1} \oplus V(h_1) \oplus V(h_2)^{-1} \oplus V(h_2)
        \oplus \cdots \oplus V(h_n) \oplus V(g)^{-1} = V(f) \oplus V(g)^{-1}
    \]
    The same is true for $\beta$, so
    \[
      V(\alpha) = V(\beta) = V(f) \oplus V(g)^{-1}
    \]
  \end{proof}
\end{proposition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        HOMOMORPHISM PROPOSITION 1 COROLLARY        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{corollary}
  For all rewriting sequences $\alpha: f \Rightarrow g$, then $V(\alpha) = V(f)
    \oplus V(g)^{-1}$.
  Note that the homomorphism $V$ is now well defined
\end{corollary}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        HOMOMORPHISM PROPOSITION 2        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proposition}
  The following category $\mathcal{P}(\mathbb{Q})$ is a $\mathbb{Q}$-category
  \begin{itemize}
    \item A set of objects which are the gates of $\mathcal{P}$
    \item For all objects $(f, g)$
  \end{itemize}
  \[
    \mathcal{E}(f, g) =
    \begin{cases}
      \text{if } f \Rightarrow g \in \mathcal{P}, &V(f \Rightarrow g) \\
      \text{otherwise } &\top
    \end{cases}
  \]
  With $\top \in \mathbb{Q}$ such that for all $x \in \mathbb{Q}$
  \[
    x \preceq \top
  \]
  
  \begin{proof}
    For all gates $(f, g)$, if it exists a unique transformation $f \Rightarrow
      g$, then
    \begin{align}
      \mathcal{E}(f, g) &= V(f \Rightarrow g) \in \mathbb{Q} \\
      &= V(f) \oplus V(g)^{-1}
    \end{align}
    otherwise we already have $\mathcal{E}(f, g) = \top \in \mathbb{Q}$.
    For all gates $f$, we know that there is a identity transformation $f
      \Rightarrow f$ and
    \begin{align}
      \mathcal{E}(f, f) &= V(id_f) \\
      &= V(f \Rightarrow f)\\
      &= V(f) \oplus V(f)^{-1} \\
      &= e
    \end{align}
    Finally, for all gates $(f, g, h)$ such that there exists $\alpha: f
      \Rightarrow g$ and $\beta: g \Rightarrow h$ in $\mathcal{P}$, then the
      homomorphism $V$ give us
    \begin{align}
      \mathcal{E}(f, h) &= V(f \Rightarrow h) \\
      &= V(\alpha \circ \beta) \\
      &= V(\alpha) \oplus V(\beta) \\
      &= V(g \Rightarrow h) \oplus V(f \Rightarrow g) \\
      &= \mathcal{E}(g, h) \oplus \mathcal{E}(f, g)
    \end{align}
    If either $\alpha$ or $\beta$ doesn't exists in $\mathcal{P}$ then
    \[
      \mathcal{E}(b, c) \oplus \mathcal{E}(a, b) \succeq \mathcal{E}(a, c)
    \]
    become
    \[
      \begin{matrix}
        &\mathcal{E}(b, c) \oplus \top &\succeq \top \\
        \text{or} &\top \oplus \mathcal{E}(a, b) &\succeq \top \\
        \text{or} &\top \oplus \top &\succeq \top
      \end{matrix}
    \]
    which is still true.
  \end{proof}
\end{proposition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        HOMOMORPHISM PROPOSITION 3        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proposition}
  $\mathcal{P}(\mathbb{Q})$ is strictly symmetric monoidal with $\otimes$, the
    2-functor of $\mathcal{P}$.
  
  \begin{proof}
    The monoidal structure is immediate using the fact that
    \[
      V(\alpha) \oplus V(\beta) \succeq V(\alpha \otimes \beta)
    \]
    that is
    \[
      V(\alpha: f \Rightarrow g) \oplus V(\beta: f' \Rightarrow g') = V(\alpha
        \otimes \beta: f \otimes f' \Rightarrow g \otimes g')
    \]
    so
    \[
      \mathcal{E}(f, g) \oplus \mathcal{E}(f', g') = \mathcal{E}(f \otimes f', g
        \otimes g')
    \]
    For the symmetry, we use the fact that $V(f \Rightarrow g) \oplus V(g
      \Rightarrow f) = e$
    \begin{align}
      \mathcal{E}(f \otimes g, g \otimes f) &= V(f \otimes g \Rightarrow g
        \otimes g) \\
      &= V(f \Rightarrow g \otimes g \Rightarrow f) \\
      &\preceq V(f \Rightarrow g) \oplus V(g \Rightarrow f) \\
      &= V(f) \oplus V(g)^{-1} \oplus V(g) \oplus V(f)^{-1} \\
      &= e
    \end{align}
  \end{proof}
\end{proposition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        HOMOMORPHISM PROPOSITION 3 COROLLARY        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{corollary}
  Given $\alpha: f \Rightarrow g$ a rewriting sequence, and $\alpha^{-1}: g
    \Rightarrow f$ the inverse rewriting sequence
  \[
    V(s \otimes s^{-1}) = e
  \]
\end{corollary}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%        HOMOMORPHISM EXAMPLES        %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{example}[Gates count]
  Let's start with a simple example, a gates counter homomorphism $N$ over the
    quantale the additive group of natural numbers.
  \begin{align*}
    N(f) & = 1 \\
    N(f \circ g) &= N(f) + N(g) \\
    N(f \otimes g) &= N(f) + N(g)
  \end{align*}
  On rewriting sequences we have
  \[
    N(f \Rightarrow g) = N(f) - N(g)
  \]
  Then the induced $\mathbb{Q}$-enriched category become a tool which give us
    the number of gates added or removed given a rewriting sequence.
\end{example}

\begin{example}[Depth \& time count]
  Two similar counters can be made using the depth and the time of a circuit
  \begin{align*}
    D(f) &= 1 \\
    D(f \circ g) &= D(f) + D(g) \\
    D(f \otimes g) &= \max(D(f), D(g))
  \end{align*}
  and
  \begin{align*}
    T(f) &= t_f \\
    T(f \circ g) &= T(f) + T(g) \\
    T(f \otimes g) &= \max(T(f), T(g))
  \end{align*}
  With $t_f$ defined for the generators of the PROP.
  It is easily to check that
  \begin{align*}
    \max(D(f), D(g)) \preceq D(f) + D(g) \\
    \max(T(f), T(g)) \preceq T(f) + T(g)
  \end{align*}
  as required by the homomorphism.
\end{example}

\section{Conclusions and further work}
\label{sec:conclusion}



\small
\bibliography{all}


\end{document}