%Since $D\in\mathcal P$, each letter $u\in\{w_0,...,w_{n-1}\}$ appears as many times among the $w^D_{\Vpol,p}$ as among the $w^D_{\Hpol,p}$. Hence, for each letter $u\in\{w_0,...,w_{n-1}\}$, there are as many positions such that for some $p_1,p_2$ one has $p^L_{\Vpol,p_1}=p^L_{\Vpol,p_2}=p$ and $w_{p}=u$, as positions $p'$ such that for some $p'_1,p'_2$ one has $p^L_{\Hpol,p'_1}=p^L_{\Hpol,p'_2}=p$ and $w_{p'}=u$ (because $\forall c,p, w^D_{c,p}=w_{p^L_{c,p}}$). We denote the number of such positions $p$ by $d(D)$. We associate with each of them one of the $d(D)$ positions $p'$, so as to partition these $2d(D)$ positions into $d(D)$ couples $(p,p')$. Note that since for each such couple there is at least two basis states for which the semantics of $L$ changes the polarisation, one has $d(D)\leq n(D)$.\Acom{détailler ?} For each of these couples $(p,p')$, we do the following transformation in $D'''$ (up to deformation):
%\[\tikzfig{gateUsurgateU}\ \to\ \tikzfig{bsUhUbbs}.\]
%Each time, we put $L$ and $L^{-1}$ in stair form again, and since $D'''$ remains symmetric, we can remove any negations at the right of $L$ and at the left of $L^{-1}$. Note that if the PBS is connected to two different $C_i$s, then they are merged together, so that the number of PBS stays the same, and if both input wires of the PBS are connected to a single $C_i$ then it is split into two parts, so that the number of PBS in $L$ decreases by $2$. At the end, the number of PBS is at most $p(D)+d(D)$, and the equality can be reached only if at every step two $C_i$s have been merged.
%This gives us a diagram
%with $L'$ of the form
%in which there are no couples of positions $p_1,p_2$ such that $p^L_{\Vpol,p_1}=p^L_{\Vpol,p_2}$ anymore%, which means that the maps $p\mapsto p^L$
%. In particular, for each position $p$ such that for some $p_1$, $(L',\Vpol,p_1)\Rightarrow(\Hpol,p)$, there exists $p_2$ such that $(L',\Hpol,p_2)\Rightarrow(\Vpol,p)$. For each of these positions, we apply the following transformation:
%\[\tikzfig{gateU}\ \to\ \tikzfig{negUneg}\]
%This gives us a diagram
%%with $L''$ of the form
%with $L''$ such that for all $c,p$, $c^{L''}_{c,p}=c$. By putting $L''$ in normal form, then in stair form again, we get a diagram $L'''$ without negations and with at most as many $PBS$ as $L''$. In particular, it contains at most $p(D)+d(D)$ PBS. If it has strictly fewer PBS, or if $d(D)< n(D)$, then we have the desired result. If it has exactly $p(D)+d(D)$ PBS and $d(D)=n(D)$, then this means that at each of the steps of the transformation of $D'''$ into $D''''$, two $C_i$s have been merged. Since $d(D)\geq 1$, this implies that there is at least one couple of gates in $D^{(5)}$ with the same label and connected to the same \Acom{staircase}. Then by applying to them the same transformation:
%\[\tikzfig{gateUsurgateU}\ \to\ \tikzfig{bsUhUbbs}\]
%and putting $L'''$ (and ${L'''}^{-1}$) in stair form again, we get a diagram with $p(D)+n(D)-1$ PBS and no negations, which is equivalent to $D$. \Acom{à relire}
\end{proof}

%For any $\alpha\geq 0$, the problem of, given a \CPBS-diagram $D$, finding an equivalent gate-optimal diagram $D'$ such that $p(D')+\alpha n(D')$ is optimal, is NP-hard.\Acom{On pourrait remplacer partout ``NP-hard'' par ``NP-complete''.}
%We conjecture that the problem is still NP-hard if we allow the cost of negations to be lower than the cost of PBS:
%%For any $\alpha\geq 0$, the problem of, given an abstract diagram $D$ and a bound $M$, deciding whether there exists a gate-optimal diagram $D'$ equivalent to $D$ such that $p(D')+\alpha n(D')\leq M$, is NP-complete.
%For any $\alpha\geq 0$, the problem of, given an abstract diagram $D$, finding an equivalent gate-optimal diagram $D'$ such that $p(D')+\alpha n(D')$ is optimal\Acom{minimal ?}, is NP-hard.

%The problem of, given a \CPBS-diagram $D$, finding an equivalent gate-$\neg$-PBS-optimal\Acom{définir les notions de ce genre} diagram is NP-hard.
%The problem of, given an abstract diagram $D$ and two integers $k_n,k_p\geq0$, deciding whether there exists a gate-optimal diagram $D'$ equivalent to $D$ such that $(n(D),p(D))\le_{lex}(k_n,k_p)$, is NP-hard.
\begin{corollary}
The problem of, given an abstract diagram $D$, finding an equivalent query-$\neg$-PBS-optimal\footnote{A diagram is query-$\neg$-PBS-optimal if it is optimal according to the  lexicographic order: the number of queries then the number of negations and finally the number of polarising beam splitters.} diagram is NP-hard.
\end{corollary}
\begin{proof}
%It suffices to prove that the problem is already NP-hard when we restrict ourselves to inputs with $k_n=0$, which is exactly the statement of \cref{gatePBSnegfreeNPhard}.
The NP-hardness of this problem directly follows from \cref{gatePBSnegfreeNPhard}. Indeed, given a negation-free diagram $D$, the query optimisation procedure gives us a negation-free query-optimal diagram $D'$ equivalent to $D$. Any query-$\neg$-PBS-optimal diagram equivalent to $D$ has to contain at most as many negations as $D'$, namely $0$, that is, be negation-free. Thus, finding a query-$\neg$-PBS-optimal equivalent to $D$ amounts to finding a negation-free query-PBS-optimal diagram equivalent to $D$.
\end{proof}

\section{Conclusion}

The power and limits of quantum coherent control is an intriguing question. Maybe surprisingly, we have proved that coherently controlled quantum computations, when expressed in the CPBS-calculus, can be efficiently optimised: any CPBS-diagram can be transformed in polynomial time into a diagram that is optimal in terms of oracle queries. We have refined the procedure to also decrease the number of polarising beam splitters. It leads to an optimal diagram when each oracle is queried only once, but the corresponding optimisation problem is NP-hard in general.

To perform the resource optimisation, we have introduced a few add-ons to the framework of the PBS-calculus. First, we have extended the syntax in order to allow the representation of unsaturated (or 3-leg) polarising beam splitters. They are essential ingredients for resource optimisation, as they provide a way to decompose a diagram into elementary components and then remove the useless ones.  Notice that the vanilla PBS-calculus is a fragment of the CPBS-calculus, so one can use the CPBS-calculus only as an intermediate language for optimisation: Given a PBS-diagram, one can see it as a CPBS-diagram and apply  various optimisation procedures. The resulting optimised CPBS-diagram is not necessarily a PBS-diagram, but it can be easily turned into a PBS-diagram by `saturating' the 3-leg polarising beam splitters (by adding useless traces) and then making the diagram monochromatic.

We have also generalised the gates of the diagrams, by considering arbitrary monoids. This is a natural abstraction that allows one to consider various examples and in particular the one of the free monoid which is appropriate to model the oracle queries. The query complexity is a convenient model to prove lower bounds, but note that the optimisation procedures described in this paper can be applied with any arbitrary monoid (for instance using Proposition \ref{prop:inter}). However, there is no guarantee of minimality in an arbitrary monoid.

%%The problem of, given a \CPBS-diagram $D$, finding an equivalent query-PBS-$\neg$-optimal diagram is NP-hard.
%%The problem of, given an abstract diagram $D$ and two integers $k_p,k_n\geq0$, deciding whether there exists a query-optimal diagram $D'$ equivalent to $D$ such that $(p(D),n(D))\le_{lex}(k_p,k_n)$, is NP-hard.
%The problem of, given an abstract diagram $D$, finding an equivalent query-PBS-$\neg$-optimal diagram is NP-hard.
%This is a direct consequence of \cref{gatePBSNPhard}, since
%a query-PBS-$\neg$-optimal diagram is in particular query-PBS-optimal.
%%\alexandre{such a diagram $D'$ satisfies in particular that $p(D)\leq k_p$.}
%One can also show that the decision problems associated with the optimisation problems presented in this section (which consist of, instead of finding a diagram optimal with respect to a given measure, deciding whether there exists a diagram for which this measure is below a given bound) are NP-complete.
%\subsection{Optimising both gates and negations\Acom{?}}
%Given a \CPBS-diagram $D$, finding an equivalent query-$\neg$-optimal diagram is not NP-hard. Procedure ? \Acom{En fait ce n'est peut-être pas si trivial à cause des négations qui servent à passer deux fois dans la même porte. S'il y a beaucoup de paires de lettres identiques entremélées ça peut potentiellement être compliqué. \`A vérifier. Il y a peut-être un algorithme glouton au moins pour le cas où toutes les lettres apparaissent dans un seul mot de la sémantique (et où tous les autres mots sont le mot vide): considérer la première occurrence d'une lettre comme une parenthèse ouvrante et l'occurrence suivante comme une parenthèse fermante et placer les négations une par une à chaque fois à un endroit où le nombre de parenthèses ouvertes non refermées est maximal (vérifier ce que ça donne si une lettre apparaît plus de $2$ fois ?).}
%%\Acom{Il faut encore dire pourquoi on a choisi d'optimiser gates puis PBS. On peut éventuellement aussi parler du langage avec des matrices dans les portes et dire qu'on peut lui donner une axiomatisation complète et minimale, en donnant les équations qu'il faut ajouter (et enlever).}
%\Scom{Dans la derniere section il faut parler de complexité: avant de dire que le probleme est en général NP-complet, il faut donner la complexité de l'heuristique (dans un modèle réaliste)}

\begin{acks}
This work was supported in part by the French National Research Agency (ANR) under the research projects SoftQPro ANR-17-CE25-0009-02 and VanQuTe ANR-17-CE24-0035, by the DGE of the French Ministry of Industry under the research project
PIA-GDN/QuantEx P163746-484124, by the PEPR integrated project EPiQ, by the STIC-AmSud project Qapla’ 21-STIC-10, and by the European projects NEASQC and HPCQS.
\end{acks}

\bibliographystyle{ACM-Reference-Format}
%%% -*-BibTeX-*-
%%% Do NOT edit. File created by BibTeX with style
%%% ACM-Reference-Format-Journals [18-Jan-2012].

\begin{thebibliography}{32}

%%% ====================================================================
%%% NOTE TO THE USER: you can override these defaults by providing
%%% customized versions of any of these macros before the \bibliography
%%% command.  Each of them MUST provide its own final punctuation,
%%% except for \shownote{}, \showDOI{}, and \showURL{}.  The latter two
%%% do not use final punctuation, in order to avoid confusing it with
%%% the Web address.
%%% To suppress output of a particular field, define its macro to expand
%%% to an empty string, or better, \unskip, like this:
%%% \newcommand{\showDOI}[1]{\unskip}   % LaTeX syntax
%%% \def \showDOI #1{\unskip}           % plain TeX syntax
%%% ====================================================================

\ifx \showCODEN    \undefined \def \showCODEN     #1{\unskip}     \fi
\ifx \showDOI      \undefined \def \showDOI       #1{#1}\fi
\ifx \showISBNx    \undefined \def \showISBNx     #1{\unskip}     \fi
\ifx \showISBNxiii \undefined \def \showISBNxiii  #1{\unskip}     \fi
\ifx \showISSN     \undefined \def \showISSN      #1{\unskip}     \fi
\ifx \showLCCN     \undefined \def \showLCCN      #1{\unskip}     \fi
\ifx \shownote     \undefined \def \shownote      #1{#1}          \fi
\ifx \showarticletitle \undefined \def \showarticletitle #1{#1}   \fi
\ifx \showURL      \undefined \def \showURL       {\relax}        \fi
% The following commands are used for tagged output and should be
% invisible to TeX
\providecommand\bibfield[2]{#2}
\providecommand\bibinfo[2]{#2}
\providecommand\natexlab[1]{#1}
\providecommand\showeprint[2][]{arXiv:#2}

\bibitem[\protect\citeauthoryear{{Abbott}, {Wechs}, {Horsman}, {Mhalla}, and
{Branciard}}{{Abbott} et~al\mbox{.}}{2020}]%
\bibfield{author}{\bibinfo{person}{Alastair~A. {Abbott}},
\bibinfo{person}{Julian {Wechs}}, \bibinfo{person}{Dominic {Horsman}},
\bibinfo{person}{Mehdi {Mhalla}}, {and} \bibinfo{person}{Cyril {Branciard}}.}
\bibinfo{year}{2020}\natexlab{}.
\newblock \showarticletitle{Communication through coherent control of quantum
\newblock \bibinfo{journal}{\emph{{Quantum}}}  \bibinfo{volume}{4}
(\bibinfo{date}{Sept.} \bibinfo{year}{2020}), \bibinfo{pages}{333}.
\newblock
\showISSN{2521-327X}
\urldef\tempurl%
\url{https://doi.org/10.22331/q-2020-09-24-333}
\showDOI{\tempurl}
\showeprint{1810.09826}

\bibitem[\protect\citeauthoryear{Amir, Hartman, Kapah, Levy, and Porat}{Amir
\bibfield{author}{\bibinfo{person}{Amihood Amir}, \bibinfo{person}{Tzvika
Hartman}, \bibinfo{person}{Oren Kapah}, \bibinfo{person}{Avivit Levy}, {and}
\bibinfo{person}{Ely Porat}.} \bibinfo{year}{2010}\natexlab{}.
\newblock \showarticletitle{On the Cost of Interchange Rearrangement in
\newblock \bibinfo{journal}{\emph{SIAM J. Comput.}} \bibinfo{volume}{39},
\bibinfo{number}{4} (\bibinfo{year}{2010}), \bibinfo{pages}{1444--1461}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1137/080712969}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Amy, Maslov, and Mosca}{Amy
\bibfield{author}{\bibinfo{person}{Matthew Amy}, \bibinfo{person}{Dmitri
Maslov}, {and} \bibinfo{person}{Michele Mosca}.}
\bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{Polynomial-time T-depth optimization of Clifford+ T
circuits via matroid partitioning}.
\newblock \bibinfo{journal}{\emph{IEEE Transactions on Computer-Aided Design of
Integrated Circuits and Systems}} \bibinfo{volume}{33}, \bibinfo{number}{10}
(\bibinfo{year}{2014}), \bibinfo{pages}{1476--1489}.
\newblock

\bibitem[\protect\citeauthoryear{Ara{\'u}jo, Costa, and Brukner}{Ara{\'u}jo
\bibfield{author}{\bibinfo{person}{Mateus Ara{\'u}jo}, \bibinfo{person}{Fabio
Costa}, {and} \bibinfo{person}{{\v{C}}aslav Brukner}.}
\bibinfo{year}{2014}\natexlab{a}.
\newblock \showarticletitle{Computational advantage from quantum-controlled
ordering of gates}.
\newblock \bibinfo{journal}{\emph{Physical review letters}}
\bibinfo{volume}{113}, \bibinfo{number}{25} (\bibinfo{year}{2014}),
\bibinfo{pages}{250402}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1103/PhysRevLett.113.250402}
\showDOI{\tempurl}
\showeprint{1401.8127}

\bibitem[\protect\citeauthoryear{Ara{\'u}jo, Feix, Costa, and
Brukner}{Ara{\'u}jo et~al\mbox{.}}{2014b}]%
\bibfield{author}{\bibinfo{person}{Mateus Ara{\'u}jo}, \bibinfo{person}{Adrien
Feix}, \bibinfo{person}{Fabio Costa}, {and} \bibinfo{person}{{\v{C}}aslav
Brukner}.} \bibinfo{year}{2014}\natexlab{b}.
\newblock \showarticletitle{Quantum circuits cannot control unknown
\newblock \bibinfo{journal}{\emph{New Journal of Physics}}
\bibinfo{volume}{16}, \bibinfo{number}{9} (\bibinfo{year}{2014}),
\bibinfo{pages}{093026}.
\newblock

\bibitem[\protect\citeauthoryear{Arrighi, Cedzich, Costes, R{\'e}mond, and
Valiron}{Arrighi et~al\mbox{.}}{2021}]%
\bibfield{author}{\bibinfo{person}{Pablo Arrighi}, \bibinfo{person}{Christopher
Cedzich}, \bibinfo{person}{Marin Costes}, \bibinfo{person}{Ulysse
R{\'e}mond}, {and} \bibinfo{person}{Beno{\^\i}t Valiron}.}
\bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Addressable quantum gates}.
\newblock \bibinfo{journal}{\emph{arXiv preprint arXiv:2109.08050}}
\newblock

\bibitem[\protect\citeauthoryear{Branciard, Cl{\'e}ment, Mhalla, and
Perdrix}{Branciard et~al\mbox{.}}{2021}]%
\bibfield{author}{\bibinfo{person}{Cyril Branciard}, \bibinfo{person}{Alexandre
Cl{\'e}ment}, \bibinfo{person}{Mehdi Mhalla}, {and} \bibinfo{person}{Simon
Perdrix}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Coherent Control and Distinguishability of Quantum
Channels via {PBS}-Diagrams}. In \bibinfo{booktitle}{\emph{46th International
Symposium on Mathematical Foundations of Computer Science (MFCS 2021)}}
\emph{(\bibinfo{series}{Leibniz International Proceedings in Informatics
(LIPIcs)}, Vol.~\bibinfo{volume}{202})},
\bibfield{editor}{\bibinfo{person}{Filippo Bonchi} {and}
\bibinfo{person}{Simon~J. Puglisi}} (Eds.). \bibinfo{publisher}{Schloss
Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, \bibinfo{address}{Dagstuhl,
Germany}, \bibinfo{pages}{22:1--22:20}.
\newblock
\showISBNx{978-3-95977-201-3}
\showISSN{1868-8969}
\urldef\tempurl%
\url{https://doi.org/10.4230/LIPIcs.MFCS.2021.22}
\showDOI{\tempurl}
\showeprint[arxiv]{2103.02073}~[quant-ph]

\bibitem[\protect\citeauthoryear{Caprara}{Caprara}{1999}]%
\bibfield{author}{\bibinfo{person}{Alberto Caprara}.}
\bibinfo{year}{1999}\natexlab{}.
\newblock \showarticletitle{Sorting Permutations by Reversals and {E}ulerian
Cycle Decompositions}.
\newblock \bibinfo{journal}{\emph{SIAM Journal on Discrete Mathematics}}
\bibinfo{volume}{12}, \bibinfo{number}{1} (\bibinfo{year}{1999}),
\bibinfo{pages}{91--110}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1137/S089548019731994X}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Chiribella}{Chiribella}{2012}]%
\bibfield{author}{\bibinfo{person}{Giulio Chiribella}.}
\bibinfo{year}{2012}\natexlab{}.
\newblock \showarticletitle{Perfect discrimination of no-signalling channels
via quantum superposition of causal structures}.
\newblock \bibinfo{journal}{\emph{Physical Review A}} \bibinfo{volume}{86},
\bibinfo{number}{4} (\bibinfo{year}{2012}), \bibinfo{pages}{040301}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1103/PhysRevA.86.040301}
\showDOI{\tempurl}
\showeprint{1109.5154}

\bibitem[\protect\citeauthoryear{Chiribella, D'Ariano, Perinotti, and
Valiron}{Chiribella et~al\mbox{.}}{2013}]%
\bibfield{author}{\bibinfo{person}{Giulio Chiribella},
\bibinfo{person}{Giacomo~Mauro D'Ariano}, \bibinfo{person}{Paolo Perinotti},
{and} \bibinfo{person}{Beno{\^\i}t Valiron}.}
\bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Quantum computations without definite causal
\newblock \bibinfo{journal}{\emph{Physical Review A}}  \bibinfo{volume}{88}
(\bibinfo{date}{Aug.} \bibinfo{year}{2013}), \bibinfo{pages}{022318}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1103/PhysRevA.88.022318}
\showDOI{\tempurl}
\showeprint[arxiv]{0912.0195}~[quant-ph]

\bibitem[\protect\citeauthoryear{Cl{\'e}ment and Perdrix}{Cl{\'e}ment and
\bibfield{author}{\bibinfo{person}{Alexandre Cl{\'e}ment} {and}
\bibinfo{person}{Simon Perdrix}.} \bibinfo{year}{2020}\natexlab{}.
\newblock \showarticletitle{{PBS}-Calculus: A Graphical Language for Coherent
Control of Quantum Computations}. In \bibinfo{booktitle}{\emph{45th
International Symposium on Mathematical Foundations of Computer Science (MFCS
2020)}} \emph{(\bibinfo{series}{Leibniz International Proceedings in
Informatics (LIPIcs)}, Vol.~\bibinfo{volume}{170})},
\bibfield{editor}{\bibinfo{person}{Javier Esparza} {and}
\bibinfo{person}{Daniel Kr{\'a}{\v l}}} (Eds.). \bibinfo{publisher}{Schloss
Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik}, \bibinfo{address}{Dagstuhl,
Germany}, \bibinfo{pages}{24:1--24:14}.
\newblock
\showISBNx{978-3-95977-159-7}
\showISSN{1868-8969}
\urldef\tempurl%
\url{https://doi.org/10.4230/LIPIcs.MFCS.2020.24}
\showDOI{\tempurl}
\showeprint[arxiv]{2002.09387}~[quant-ph]

\bibitem[\protect\citeauthoryear{Colnaghi, D'Ariano, Facchini, and
Perinotti}{Colnaghi et~al\mbox{.}}{2012}]%
\bibfield{author}{\bibinfo{person}{Timoteo Colnaghi},
\bibinfo{person}{Giacomo~Mauro D'Ariano}, \bibinfo{person}{Stefano Facchini},
{and} \bibinfo{person}{Paolo Perinotti}.} \bibinfo{year}{2012}\natexlab{}.
\newblock \showarticletitle{Quantum computation with programmable connections
between gates}.
\newblock \bibinfo{journal}{\emph{Physics Letters A}} \bibinfo{volume}{376},
\bibinfo{number}{45} (\bibinfo{year}{2012}), \bibinfo{pages}{2940--2943}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1016/j.physleta.2012.08.028}
\showDOI{\tempurl}
\showeprint{1109.5987}

\bibitem[\protect\citeauthoryear{D{\'\i}az-Caro, Guillermo, Miquel, and
Valiron}{D{\'\i}az-Caro et~al\mbox{.}}{2019}]%
\bibfield{author}{\bibinfo{person}{Alejandro D{\'\i}az-Caro},
\bibinfo{person}{Mauricio Guillermo}, \bibinfo{person}{Alexandre Miquel},
{and} \bibinfo{person}{Beno{\^\i}t Valiron}.}
\bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Realizability in the unitary sphere}. In
\bibinfo{booktitle}{\emph{2019 34th Annual ACM/IEEE Symposium on Logic in
Computer Science (LICS)}}. IEEE, \bibinfo{pages}{1--13}.
\newblock

\bibitem[\protect\citeauthoryear{Dowek and Arrighi}{Dowek and Arrighi}{2017}]%
\bibfield{author}{\bibinfo{person}{Gilles Dowek} {and} \bibinfo{person}{Pablo
Arrighi}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Lineal: A linear-algebraic lambda-calculus}.
\newblock \bibinfo{journal}{\emph{Logical Methods in Computer Science}}
\bibinfo{volume}{13} (\bibinfo{year}{2017}).
\newblock

\bibitem[\protect\citeauthoryear{Ebler, Salek, and Chiribella}{Ebler
\bibfield{author}{\bibinfo{person}{Daniel Ebler}, \bibinfo{person}{Sina Salek},
{and} \bibinfo{person}{Giulio Chiribella}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Enhanced communication with the assistance of
indefinite causal order}.
\newblock \bibinfo{journal}{\emph{Physical review letters}}
\bibinfo{volume}{120}, \bibinfo{number}{12}, Article
\bibinfo{articleno}{120502} (\bibinfo{date}{March} \bibinfo{year}{2018}),
\bibinfo{numpages}{120502}~pages.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1103/PhysRevLett.120.120502}
\showDOI{\tempurl}
\showeprint[arxiv]{1711.10165}~[quant-ph]

\bibitem[\protect\citeauthoryear{Facchini and Perdrix}{Facchini and
\bibfield{author}{\bibinfo{person}{Stefano Facchini} {and}
\bibinfo{person}{Simon Perdrix}.} \bibinfo{year}{2015}\natexlab{}.
\newblock \showarticletitle{Quantum circuits for the unitary permutation
problem}. In \bibinfo{booktitle}{\emph{International Conference on Theory and
Applications of Models of Computation}}. Springer, \bibinfo{pages}{324--331}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-319-17142-5_28}
\showDOI{\tempurl}
\showeprint{1405.5205}

\bibitem[\protect\citeauthoryear{Feix, Ara{\'u}jo, and Brukner}{Feix
\bibfield{author}{\bibinfo{person}{Adrien Feix}, \bibinfo{person}{Mateus
Ara{\'u}jo}, {and} \bibinfo{person}{{\v{C}}aslav Brukner}.}
\bibinfo{year}{2015}\natexlab{}.
\newblock \showarticletitle{Quantum superposition of the order of parties as a
communication resource}.
\newblock \bibinfo{journal}{\emph{Physical Review A}} \bibinfo{volume}{92},
\bibinfo{number}{5} (\bibinfo{year}{2015}), \bibinfo{pages}{052326}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1103/PhysRevA.92.052326}
\showDOI{\tempurl}
\showeprint{1508.07840}

\bibitem[\protect\citeauthoryear{Giles and Selinger}{Giles and
\bibfield{author}{\bibinfo{person}{Brett Giles} {and} \bibinfo{person}{Peter
Selinger}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \bibinfo{title}{Remarks on {M}atsumoto and {A}mano's normal form for
single-qubit {Clifford+$T$} operators}.
\newblock
\newblock
\showeprint[arxiv]{1312.6584}~[quant-ph]

\bibitem[\protect\citeauthoryear{Gu{\'e}rin, Feix, Ara{\'u}jo, and
Brukner}{Gu{\'e}rin et~al\mbox{.}}{2016}]%
\bibfield{author}{\bibinfo{person}{Philippe~Allard Gu{\'e}rin},
\bibinfo{person}{Adrien Feix}, \bibinfo{person}{Mateus Ara{\'u}jo}, {and}
\bibinfo{person}{{\v{C}}aslav Brukner}.} \bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Exponential communication complexity advantage from
quantum superposition of the direction of communication}.
\newblock \bibinfo{journal}{\emph{Physical review letters}}
\bibinfo{volume}{117}, \bibinfo{number}{10} (\bibinfo{year}{2016}),
\bibinfo{pages}{100502}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1103/PhysRevLett.117.100502}
\showDOI{\tempurl}
\showeprint{1605.07372}

\bibitem[\protect\citeauthoryear{Hardy}{Hardy}{2005}]%
\bibfield{author}{\bibinfo{person}{Lucien Hardy}.}
\bibinfo{year}{2005}\natexlab{}.
\newblock \showarticletitle{Probability theories with dynamic causal structure:
a new framework for quantum gravity}.
\newblock \bibinfo{journal}{\emph{arXiv preprint gr-qc/0509120}}
\newblock

\bibitem[\protect\citeauthoryear{Hasegawa, Hofmann, and Plotkin}{Hasegawa
\bibfield{author}{\bibinfo{person}{Masahito Hasegawa}, \bibinfo{person}{Martin
Hofmann}, {and} \bibinfo{person}{Gordon Plotkin}.}
\bibinfo{year}{2008}\natexlab{}.
\newblock \showarticletitle{Finite dimensional vector spaces are complete for
traced symmetric monoidal categories}.
\newblock In \bibinfo{booktitle}{\emph{Pillars of computer science}}.
\bibinfo{publisher}{Springer}, \bibinfo{pages}{367--385}.
\newblock

\bibitem[\protect\citeauthoryear{Holyer}{Holyer}{1981}]%
\bibfield{author}{\bibinfo{person}{Ian Holyer}.}
\bibinfo{year}{1981}\natexlab{}.
\newblock \showarticletitle{The {NP}-Completeness of Some Edge-Partition
\newblock \bibinfo{journal}{\emph{SIAM J. Comput.}} \bibinfo{volume}{10},
\bibinfo{number}{4} (\bibinfo{year}{1981}), \bibinfo{pages}{713--717}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1137/0210054}
\showDOI{\tempurl}

\bibitem[\protect\citeauthoryear{Kliuchnikov and Maslov}{Kliuchnikov and
\bibfield{author}{\bibinfo{person}{Vadym Kliuchnikov} {and}
\bibinfo{person}{Dmitri Maslov}.} \bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Optimization of Clifford circuits}.
\newblock \bibinfo{journal}{\emph{Physical Review A}} \bibinfo{volume}{88},
\bibinfo{number}{5} (\bibinfo{year}{2013}), \bibinfo{pages}{052307}.
\newblock

\bibitem[\protect\citeauthoryear{MacLane}{MacLane}{1965}]%
\bibfield{author}{\bibinfo{person}{Saunders MacLane}.}
\bibinfo{year}{1965}\natexlab{}.
\newblock \showarticletitle{Categorical algebra}.
\newblock \bibinfo{journal}{\emph{Bull. Amer. Math. Soc.}}
\bibinfo{volume}{71}, \bibinfo{number}{1} (\bibinfo{year}{1965}),
\bibinfo{pages}{40--106}.
\newblock

\bibitem[\protect\citeauthoryear{Matsumoto and Amano}{Matsumoto and
\bibfield{author}{\bibinfo{person}{Ken Matsumoto} {and}
\bibinfo{person}{Kazuyuki Amano}.} \bibinfo{year}{2008}\natexlab{}.
\newblock \bibinfo{title}{Representation of Quantum Circuits with {C}lifford
and $\pi/8$ Gates}.
\newblock
\newblock
\showeprint[arxiv]{0806.3834}~[quant-ph]

\bibitem[\protect\citeauthoryear{Nam, Ross, Su, Childs, and Maslov}{Nam
\bibfield{author}{\bibinfo{person}{Yunseong Nam}, \bibinfo{person}{Neil~J
Ross}, \bibinfo{person}{Yuan Su}, \bibinfo{person}{Andrew~M Childs}, {and}
\bibinfo{person}{Dmitri Maslov}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Automated optimization of large quantum circuits
with continuous parameters}.
\newblock \bibinfo{journal}{\emph{npj Quantum Information}}
\bibinfo{volume}{4}, \bibinfo{number}{1} (\bibinfo{year}{2018}),
\bibinfo{pages}{1--12}.
\newblock

\bibitem[\protect\citeauthoryear{Oreshkov, Costa, and Brukner}{Oreshkov
\bibfield{author}{\bibinfo{person}{Ognyan Oreshkov}, \bibinfo{person}{Fabio
Costa}, {and} \bibinfo{person}{{\v{C}}aslav Brukner}.}
\bibinfo{year}{2012}\natexlab{}.
\newblock \showarticletitle{Quantum correlations with no causal order}.
\newblock \bibinfo{journal}{\emph{Nature communications}} \bibinfo{volume}{3},
\bibinfo{number}{1} (\bibinfo{year}{2012}), \bibinfo{pages}{1--8}.
\newblock

\bibitem[\protect\citeauthoryear{Selinger}{Selinger}{2011}]%
\bibfield{author}{\bibinfo{person}{Peter Selinger}.}
\bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{Finite Dimensional Hilbert Spaces are Complete for
Dagger Compact Closed Categories}.
\newblock \bibinfo{journal}{\emph{Electronic Notes in Theoretical Computer
Science}} \bibinfo{volume}{270}, \bibinfo{number}{1} (\bibinfo{year}{2011}),
\bibinfo{pages}{113--119}.
\newblock

\bibitem[\protect\citeauthoryear{Vanrietvelde, Kristj{\'a}nsson, and
Barrett}{Vanrietvelde et~al\mbox{.}}{2021}]%
\bibfield{author}{\bibinfo{person}{Augustin Vanrietvelde},
\bibinfo{person}{Hl{\'e}r Kristj{\'a}nsson}, {and} \bibinfo{person}{Jonathan
Barrett}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Routed quantum circuits}.
\newblock \bibinfo{journal}{\emph{Quantum}}  \bibinfo{volume}{5}
(\bibinfo{year}{2021}), \bibinfo{pages}{503}.
\newblock

\bibitem[\protect\citeauthoryear{Wechs, Dourdent, Abbott, and Branciard}{Wechs
\bibfield{author}{\bibinfo{person}{Julian Wechs}, \bibinfo{person}{Hippolyte
Dourdent}, \bibinfo{person}{Alastair~A Abbott}, {and} \bibinfo{person}{Cyril
Branciard}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Quantum circuits with classical versus quantum
control of causal order}.
\newblock \bibinfo{journal}{\emph{arXiv preprint arXiv:2101.08796}}
\newblock

\bibitem[\protect\citeauthoryear{Wilson and Chiribella}{Wilson and
\bibfield{author}{\bibinfo{person}{Matt Wilson} {and} \bibinfo{person}{Giulio
Chiribella}.} \bibinfo{year}{2020}\natexlab{}.
\newblock \showarticletitle{A diagrammatic approach to information transmission
in generalised switches}.
\newblock \bibinfo{journal}{\emph{arXiv preprint arXiv:2003.08224}}
\newblock

\bibitem[\protect\citeauthoryear{Zych, Costa, Pikovski, and Brukner}{Zych
\bibfield{author}{\bibinfo{person}{Magdalena Zych}, \bibinfo{person}{Fabio
Costa}, \bibinfo{person}{Igor Pikovski}, {and} \bibinfo{person}{{\v{C}}aslav
Brukner}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Bell's theorem for temporal order}.
\newblock \bibinfo{journal}{\emph{Nature communications}} \bibinfo{volume}{10},
\bibinfo{number}{1} (\bibinfo{year}{2019}), \bibinfo{pages}{1--10}.
\newblock

\end{thebibliography}

\appendix

\section{Proofs\Acom{à structurer}}

\subsection{Proof of Proposition \ref{quantumsemiso}}\label{preuvequantumsemiso}

%Note that for any $c,p$, $U^D_{c,p}$ is an isometry since it is an element of $\UU(\H)$.
Since there exists an orthonormal basis of $\CC^{[a]}\otimes\Ve$ composed of vectors of the form $\ket{c,p}\otimes\ket\phi$, it suffices to check that $V_D$ preserves all scalar products of vectors of this form. For any $c$, $p$, $c'$, $p'$, $\ket\phi$ and $\ket{\phi'}$, one has $(\bra{c,p}\otimes\bra\phi)V_D^\dag V_D^{}(\ket{c'\!,p'}\otimes\ket{\phi'})=\scalprod{c^D_{c,p},p^D_{c,p}}{c^D_{c'\!,p'},p^D_{c'\!,p'}}\otimes\bra\phi {U^D_{c,p}}^{\!\dag} U^D_{c'\!,p'}\ket{\phi'}$. On the one hand, it can be proved in the same way as in \cite{alex2020pbscalculus} that the function $(c,p)\mapsto(c^D_{c,p},p^D_{c,p})$ is a bijection, so that $(c^D_{c,p},p^D_{c,p})=(c^D_{c'\!,p'},p^D_{c'\!,p'})$ if and only if $(c,p)=(c'\!,p')$, and\\ $\scalprod{c^D_{c,p},p^D_{c,p}}{c^D_{c'\!,p'},p^D_{c'\!,p'}}=\scalprod{c,p}{c'\!,p'}=\begin{cases}1&\text{if $(c,p)=(c'\!,p')$}\\0&\text{if $(c,p)\neq(c'\!,p')$}\end{cases}$. On the other hand, since $U^D_{c,p}$ is an isometry, if $(c,p)=(c'\!,p')$ then $\bra\phi {U^D_{c,p}}^{\!\dag} U^D_{c,p}\ket{\phi'}=\scalprod{\phi}{\phi'}$. Thus,\\ $(\bra{c,p}\otimes\bra\phi)V_D^\dag V_D^{}(\ket{c'\!,p'}\otimes\ket{\phi'})=\begin{cases}\scalprod{\phi}{\phi'}&\text{if $(c,p)=(c'\!,p')$}\\0&\text{if $(c,p)\neq(c'\!,p')$}\end{cases}\allowbreak=(\bra{c,p}\otimes\bra\phi)(\ket{c'\!,p'}\otimes\ket{\phi'})$.

%(\bra{c,p}\otimes\bra\phi)V_D^\dag V_D(\ket{c'\!,p'}\otimes\ket{\phi'})&=&

%\subsection{Proof of Proposition \ref{prop:denpath}}\label{preuvepropdenpath}

%\subsection{Proof of Proposition \ref{prop:qinterpimplpathsem}}\label{preuvepropqinterpimplpathsem}
%%{[sketch]} If $q$ is large enough then we can choose $\gamma$ in such a way that for any $w,w'\in \V^*$, $\gamma(w)=\gamma(w)$ implies $w=w'$.\Scom{Give an explicit construction to provide a bound on $q$?}
%By \cref{prop:denpath}, $%\left(\forall \gamma:\V \to \mathbb C^{q\times q}, \interp D_\gamma = \interp{D'}_\gamma\right)
%\interp{D}^q=\interp{D'}^q$ is equivalent to
%\[\forall (c,p)\in X, c_{c,p}^D =c_{c,p}^{D'} \wedge p_{c,p}^D =p_{c,p}^{D'} \wedge \left(\forall \gamma:\V \to \mathbb C^{q\times q}, \gamma(w_{c,p}^D) =\gamma(w_{c,p}^{D'})\right)\]
%Therefore, it suffices to prove that for any two words $w,w'\in\V^*$,
%\[\left(\forall \gamma:\V \to \mathbb C^{q\times q}, \gamma(w) =\gamma(w')\right)\Rightarrow w=w'.\]
%If $w\neq w'$, then
%\item either $w$ and $w'$ are of the form $U^n$ and $U^m$ respectively, with $n,m\in\N$ and $n\neq m$, in which case by taking $\gamma(U)=e^{\mathrm{i}\pi\theta}I$ with $\theta\notin\mathbb Q$ we get $\gamma(w)\neq\gamma(w')$
%\item or there exist two letters $U,V\in\V$ such that the subwords $w\longrestr{U,V}$ and $w'\longrestr{U,V}$ obtained by keeping only the occurrences of $U$ and $V$ are different\footnote{For instance one can consider the first place where $w$ and $w'$ differ: if both have a letter at this place then one can take their respective letter at this place as $U$ and $V$, and if one of the two words does not have a letter at this place (which means that it is a prefix of the other word) then one can take the letter present at this place in the longer word as $U$ and any other letter as $V$.}. In this case, let us consider $\gamma$ defined by $\gamma(U)=(HT)^{(q)}$ and $\gamma(V)=(SHT)^{(q)}$ where $T=\begin{pmatrix}1&0\\0&e^{\mathrm{i}\pi/4}\end{pmatrix}$, $S=T^2=\begin{pmatrix}1&0\\0&\mathrm{i}\end{pmatrix}$, $H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$, and for any %$2\times 2$
%matrix $M%=\begin{pmatrix}a&b\\c&d\end{pmatrix}
%\in\C^{2\times 2}$\smallskip, $M^{(q)}=\left(%\begin{array}{@{}c@{}|c}\begin{array}{cc}a&b\\c&d\end{array}
%\begin{array}{c|c}M&0\\\hline 0&I_{q-2}\end{array}\right)\in\C^{q\times q}$. Theorem 4.1 of \cite{giles2019remarks} or Theorem 1(II) of \cite{matsumoto2008representation} implies that $\gamma(w)\neq\gamma(w')$.
%%\item or there exist two letters $U,V\in\V$ such that the subwords $w\longrestr{U,V}$ and $w'\longrestr{U,V}$ obtained by keeping only the occurrences of $U$ and $V$ are different\footnote{For instance one can consider the first place where $w$ and $w'$ differ: if both have a letter at this place then one can take their respective letter at this place as $U$ and $V$, and if one of the two words does not have a letter at this place (which means that it is a prefix of the other word) then one can take the letter present at this place in the longer word as $U$ and any other letter as $V$.}. In this case, let us consider $\gamma$ defined by $\gamma(U)=\begin{pmatrix}2&0\\0&1\end{pmatrix}$, $\gamma(V)=\begin{pmatrix}2&1\\0&1\end{pmatrix}$ and $\forall W\neq U,V, \gamma(W)=I$. Let us decompose $w\restr{U,V}=A_1...A_n$ with $\forall i,A_i\in\{U,V\}$. By a direct induction, one can show that $\gamma(w)=\begin{pmatrix}2^n&\sum\limits_{i=1}^n 2^{n-i} \delta_i\\0&1\end{pmatrix}$ where $\delta_i=\begin{cases}0&\text{if $A_i=U$}\\1&\text{if $A_i=V$}\end{cases}$. Similarly, if we decompose $w'\restr{U,V}=B_1...B_m$ with $\forall i,B_i\in\{U,V\}$, then we have $\gamma(w')=\begin{pmatrix}2^m&\sum\limits_{i=1}^m 2^{n-i} \delta'_i\\0&1\end{pmatrix}$ where $\delta'_i=\begin{cases}0&\text{if $B_i=U$}\\1&\text{if $B_i=V$}\end{cases}$
%%. Since the binary representation of a natural integer is unique, this implies that $\gamma(w)\neq\gamma(w')$.\Acom{On peut aussi garder toutes les lettres et définir $\gamma(U_i)=\begin{pmatrix}b&i\\0&1\end{pmatrix}$ où $b$ est le nombre de lettres différentes.}
%By contraposition, we get the result.
%%\Acom{Je ne sais pas si ca reste vrai avec des unitaires.}
%%\Scom{Pour les unitaires, peut être choisir $X(\theta)$ et $Z(\theta')$ avec $\theta$, $\theta'$ (et $\theta-\theta'$) des multiples irrationnels de $\pi$..}

%\subsection{Proof of Proposition \ref{equivdenpath}}\label{preuveequivdenpath}
%[$\Leftarrow$] Since the denotational semantics is defined in terms of the path semantics, if two diagrams have the same path semantics then they also have the same denotational semantics.
%\noindent[$\Rightarrow$] It follows directly from \cref{prop:denpath} that $\interp{D}=\interp{D'}$ is equivalent to
%\[\hspace*{-10em}\forall (c,p)\in X, c_{c,p}^D =c_{c,p}^{D'} \wedge p_{c,p}^D =p_{c,p}^{D'} \wedge \left(\forall q\geq0,\forall \gamma:\V \to \mathbb C^{q\times q}, \gamma(w_{c,p}^D) =\gamma(w_{c,p}^{D'})\right)\]
%Therefore, it suffices to prove that for any two words $w,w'\in\V^*$,
%\[\left(\forall q\geq0,\forall \gamma:\V \to \mathbb C^{q\times q}, \gamma(w) =\gamma(w')\right)\Rightarrow w=w'.\]
%A fortiori, it suffices to prove that
%\[\left(\forall \gamma:\V \to \mathbb C^{2\times 2}, \gamma(w) =\gamma(w')\right)\Rightarrow w=w'.\]
%If $w\neq w'$, then
%\item either $w$ and $w'$ are of the form $U^n$ and $U^m$ respectively, with $n,m\in\N$ and $n\neq m$, in which case by taking $\gamma(U)=e^{\mathrm{i}\pi\theta}I$ with $\theta\notin\mathbb Q$ we get $\gamma(w)\neq\gamma(w')$
%\item or there exist two letters $U,V\in\V$ such that the subwords $w\longrestr{U,V}$ and $w'\longrestr{U,V}$ obtained by keeping only the occurrences of $U$ and $V$ are different\footnote{For instance one can consider the first place where $w$ and $w'$ differ: if both have a letter at this place then one can take their respective letter at this place as $U$ and $V$, and if one of the two words does not have a letter at this place (which means that it is a prefix of the other word) then one can take the letter present at this place in the longer word as $U$ and any other letter as $V$.}. In this case, let us consider $\gamma$ defined by $\gamma(U)=HT$ and $\gamma(V)=SHT$ where $T=\begin{pmatrix}1&0\\0&e^{\mathrm{i}\pi/4}\end{pmatrix}$, $S=T^2=\begin{pmatrix}1&0\\0&\mathrm{i}\end{pmatrix}$ %,
%and $H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$%, and for any %$2\times 2$
%%matrix $M%=\begin{pmatrix}a&b\\c&d\end{pmatrix}
%%\in\C^{2\times 2}$\smallskip, $M^{(q)}=\left(%\begin{array}{@{}c@{}|c}\begin{array}{cc}a&b\\c&d\end{array}
%%\begin{array}{c|c}M&0\\\hline 0&I_{q-2}\end{array}\right)\in\C^{q\times q}$
%. Theorem 4.1 of \cite{giles2019remarks} or Theorem 1(II) of \cite{matsumoto2008representation} implies that $\gamma(w)\neq\gamma(w')$.
%%\item or there exist two letters $U,V\in\V$ such that the subwords $w\longrestr{U,V}$ and $w'\longrestr{U,V}$ obtained by keeping only the occurrences of $U$ and $V$ are different\footnote{For instance one can consider the first place where $w$ and $w'$ differ: if both have a letter at this place then one can take their respective letter at this place as $U$ and $V$, and if one of the two words does not have a letter at this place (which means that it is a prefix of the other word) then one can take the letter present at this place in the longer word as $U$ and any other letter as $V$.}. In this case, let us consider $\gamma$ defined by $\gamma(U)=\begin{pmatrix}2&0\\0&1\end{pmatrix}$, $\gamma(V)=\begin{pmatrix}2&1\\0&1\end{pmatrix}$ and $\forall W\neq U,V, \gamma(W)=I$. Let us decompose $w\restr{U,V}=A_1...A_n$ with $\forall i,A_i\in\{U,V\}$. By a direct induction, one can show that $\gamma(w)=\begin{pmatrix}2^n&\sum\limits_{i=1}^n 2^{n-i} \delta_i\\0&1\end{pmatrix}$ where $\delta_i=\begin{cases}0&\text{if $A_i=U$}\\1&\text{if $A_i=V$}\end{cases}$. Similarly, if we decompose $w'\restr{U,V}=B_1...B_m$ with $\forall i,B_i\in\{U,V\}$, then we have $\gamma(w')=\begin{pmatrix}2^m&\sum\limits_{i=1}^m 2^{n-i} \delta'_i\\0&1\end{pmatrix}$ where $\delta'_i=\begin{cases}0&\text{if $B_i=U$}\\1&\text{if $B_i=V$}\end{cases}$
%%. Since the binary representation of a natural integer is unique, this implies that $\gamma(w)\neq\gamma(w')$.\Acom{On peut aussi garder toutes les lettres et définir $\gamma(U_i)=\begin{pmatrix}b&i\\0&1\end{pmatrix}$ où $b$ est le nombre de lettres différentes.}
%By contraposition, we get the result.
%%\Acom{Je ne sais pas si ca reste vrai avec des unitaires.}
%%\Scom{Pour les unitaires, peut être choisir $X(\theta)$ et $Z(\theta')$ avec $\theta$, $\theta'$ (et $\theta-\theta'$) des multiples irrationnels de $\pi$..}

\subsection{Proof of Proposition \ref{equivquantumaction}}\label{preuveequivquantumaction}
Let us assume that $\M$ is a monoid of linear maps on a complex vector space $\Ve$.

Since the quantum semantics is defined from the action semantics, it is clear that $\forall D,D', \interp{D} = \interp {D'} \Rightarrow V_D=V_{D'}$.

Given a $\M$-diagram $D$, %for any $c,p$, let $((c',p'),U_{cp})=\interp{D}(c,p)$. I
if $0\notin \M$, then for all $c,p$, $U^D_{c'p}\neq 0$, so that there exists $\ket\phi\in\Ve$ such that $U^D_{c,p}\ket\phi\neq0$. Then $\ket{c^D_{c,p},p^D_{c,p}}\otimes U^D_{c,p}\ket\phi\neq0$, which implies that $c^D_{c,p}$ and $p^D_{c,p}$ are uniquely determined from the data of $c$, $p$ and $V_D$. Since in any case, $U^D_{c,p}$ is uniquely determined from the data of $c$, $p$ and $V_D$, this implies that if $0\notin \M$ then $\interp{D}$ is uniquely determined from $V_D$. Hence if $0\notin \M$ then for any two $\M$-diagrams $D$ and $D'$, $V_D=V_{D'} \Rightarrow \interp{D} = \interp {D'}$.

Conversely, if $0\in \M$, then for example, with $D=\sgtikzfig{gate0}$ and $D'=\sgtikzfig{gate0neg}$, both of type $\top\to\top$, one has $V_D=V_D'=0$ but $\interp{D}(\Vpol,0)=((\Vpol,0),0)\neq\interp{D'}(\Vpol,0)=((\Hpol,0),0)$.

\subsection{Proof of Propositions \ref{interpretationuniverselle} and \ref{matricescompletes}}\label{preuveinterpretationuniverselle}

Given a monoid homomorphism $\gamma\colon\GG^*\to\UU(\H)$, %and
a $\GG^*$-diagram $D$ %, if $V_{\gamma(D_1)}=V_{\gamma(D_2)}$ then since $0\notin\UU(\H)$, by \cref{equivquantumaction}, one has $\interp{\gamma(D_1)}=\interp{\gamma(D_2)}$. Given
and any $c,p$, %let $((c'_1,p'_1),w_1)=\interp{D_1}(c,p)$ and $((c'_2,p'_2),w_2)=\interp{D_2}(c,p)$; one has $\interp{\gamma(D_1)}=((c'_1,p'_1),\gamma(w_1))$ and $\interp{\gamma(D_2)}=((c'_2,p'_2),\gamma(w_2))$
one has %$\interp{\gamma(D_1)}=((c^{D_1}_{c,p},p^{D_1}_{c,p}),\gamma(w^{D_1}_{c,p}))$ and
$\interp{\gamma(D)}=((c^{D}_{c,p},p^{D}_{c,p}),\gamma(w^{D}_{c,p}))$. Therefore, to prove that $\forall D_1,D_2,\interp{\gamma(D_1)}=\interp{\gamma(D_2)}\Rightarrow\interp{D_1}=\interp{D_2}$, it suffices to prove that for any two words $w_1,w_2\in\GG^*$, if $\gamma(w_1)=\gamma(w_2)$ then $w_1=w_2$.

By Zorn's lemma, there exists a maximal family $(\alpha_i)_{i\in I}$ of $\QQ$-algebraically independent complex numbers of absolute value $1$. Such a family must have the cardinality of $\CC$ (that is, $2^{\aleph_0}$). Indeed, the cardinality of the set of polynomials in one variable with coefficients in the field extension of $\QQ$ generated by the $\alpha_i$, is $\max(\aleph_0,\mathrm{card}(I))$, and since each of these polynomials has finitely many roots, the set of their roots also has cardinality $\max(\aleph_0,\mathrm{card}(I))$. If $\mathrm{card}(I)$ is strictly less than $2^{\aleph_0}$, then so is $\max(\aleph_0,\mathrm{card}(I))$; therefore, since the set $\bigl\{\alpha\in\CC~\bigm|~|\alpha|=1\bigr\}$ has cardinality $2^{\aleph_0}$, it contains an element $\alpha_\bot$ which is not a root of any of these polynomials, so that by adding $\alpha_\bot$ to the family $(\alpha_i)_{i\in I}$, we still have a family of $\QQ$-algebraically independent complex numbers of absolute value $1$, which contradicts the maximality of $(\alpha_i)_{i\in I}$.

If the cardinality of $\GG$ is no greater than $2^{\aleph_0}$, then without loss of generality, we can assume that $\GG\subseteq I$. We start with the case where $\H=\CC^2$. We consider the function $\gamma\colon U\nolinebreak\in\nolinebreak\GG\mapsto H\begin{pmatrix}1&0\\0&\alpha_U\end{pmatrix}$, extended into a monoid homomorphism $\gamma\colon \GG^*\to\UU(\CC^2)$ (where $H=\frac{1}{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$). Given two words $w_1,w_2\in\GG^*$ such that $w_1\neq w_2$, the entries of $\gamma(w_1)$ and $\gamma(w_2)$ are polynomials in the $\alpha_U$ with coefficients in $\QQ$. The two associated matrices of polynomials differ by at least one entry: indeed, by replacing each of the $\alpha_U$ by either $e^{\mathrm{i}\pi/4}$ or $e^{3\mathrm{i}\pi/4}$ in such a way that the sequence of angles induced by $w_1$ and $w_2$ are different, we get two different sequences of the patterns $HT$ and $HTS$ with $T=\begin{pmatrix}1&0\\0&e^{\mathrm{i}\pi/4}\end{pmatrix}$ and $S=T^2$, and it %is easy to see that one can adapt{\Acom{TODO : énoncer le théorème adapté, où on remplace $SHT$ par $HTS$}}
follows from
Theorem 4.1 of \cite{giles2019remarks} (which is Theorem 1(II) of \cite{matsumoto2008representation}) %to show
that these two products of matrices have distinct values.\footnote{Indeed, the regular expression $(HT|HTS)^*$ describes the same set of words as $\epsilon|(HT(HT|SHT)^*(\epsilon|S))$, which, since both the identity operator and $S$ belong to the Clifford group, clearly describes a subset of the Matsumoto-Amano normal forms defined in \cite{giles2019remarks} (Equation (2)).} Since the $\alpha_U$ are algebraically independent, this implies that $\gamma(w_1)\neq \gamma(w_2)$.

In the case where the cardinality of $\GG$ is no greater than $2^{\aleph_0}$ and $\H\neq\CC^2$, it suffices to consider a subspace of $\H$ of dimension $2$ and to define $\gamma(U)$ in the same way on this subspace and as the identity on the orthogonal complement.

If the dimension of $\H$ is strictly greater than %If the cardinality of $\H$ is strictly greater than $2^{\aleph_0}$
$\aleph_0$ (and the cardinality of $\GG$ is no greater than the cardinality of $\H$) then %$\dim(\H)=\mathrm{card}(\H)$ so that there
Zorn's lemma implies that $\H$ can be decomposed into a direct sum of $\dim(\H)$ orthogonal subspaces of dimension $2$: $\H=\bigoplus_{j\in J}\H_j$ with $\mathrm{card}(J)=\dim(\H)$ and $\forall j,\dim(\H_j)=2$. For each of the $(2^{\aleph_0})^{\dim(\H)}=2^{\dim(\H)}$ possible families $(i_j)_{j\in J}$ of elements of $I$ indexed by $J$, one can define a map $\delta\!\left((i_j)_{j\in J}\right)\in\UU(\H)$ as having matrix $H\begin{pmatrix}1&0\\0&\alpha_i\end{pmatrix}$ in an arbitrary orthonormal basis of $\H_j$ (chosen with the help of the axiom of choice) for every $j$. If the cardinality of $\GG$ is no greater than $2^{\dim(\H)}$, then without loss of generality, we can assume that $\GG\subseteq I^J$. We define the function %$\gamma\colon U\nolinebreak\in\nolinebreak\GG\mapsto \delta(U)$
$\gamma\colon\GG\to\UU(\H)$ by $\forall U,\gamma(U)=\delta(U)$, and extend it into a monoid homomorphism $\gamma\colon \GG^*\to\UU(\CC^2)$. Given two words $w_1,w_2\in\GG^*$ such that $w_1\neq w_2$, there exists an index $j\in J$ such that the two sequence of elements of $i$ induced by $w_1$ and $w_2$ at index $j$ are distinct, which, by the argument given above, implies that the unitary maps on $\H_j$ induced respectively by $\gamma(w_1)$ and $\gamma(w_2)$ %, that are given by the corresponding products of $2\times 2$ matrices,
are distinct. Hence, $\gamma(w_1)\neq \gamma(w_2)$.

Finally, to prove Proposition \ref{matricescompletes} without using the axiom of choice, it suffices to exhibit an infinite family of $\QQ$-algebraically independent complex numbers of absolute value $1$. One can consider for example the $e^{\mathrm{i}\pi^k}, k\geq 2$, whose algebraic independence follows from the Lindemann-Weierstrass theorem and the fact that $\pi$ is transcendental. Given such a family, one can use a similar argument as above to prove a weaker version of Proposition \ref{interpretationuniverselle} in which the cardinality of $\GG$ is required to be at most $\aleph_0$, which immediately implies Proposition \ref{matricescompletes}.

\subsection{Proof of Lemma \ref{uniquenessNF}}\label{preuveuniquenessNF}
If $\interp{N}=\interp{N'}$, then in particular $N$ and $N'$ have same type: $N,N':a\to b$ for some $a,b$.

Let us decompose $N$ and $N'$ into $N=M\circ P\circ F\circ G\circ S$ and $N'=M'\circ P'\circ F'\circ G'\circ S'$.

%Let $X$, $X'$, $Y$ and $Y'$ be such that $N:X\to Y$ and $N':X'\to Y'$. Since $\interp{N}=\interp{N'}$, one has $X=X'$ and $Y=Y'$. Since $S$, $S'$, $M$ and $M'$ are uniquely determined by $X$, $X'$, $Y$ and $Y'$ respectively, one has $S=S'$ and $M=M'$.
%Since $\interp{N}=\interp{N'}$, there exist $X,Y$ such that $N,N':X\to Y$. Since $S$ and $S'$ are uniquely determined by their input type and $M$ and $M'$ are uniquely determined by their output type, one has $S=S'$ and $M=M'$.
It follows directly from the definition that $S$ and $S'$ are uniquely determined by their input type, so that since they both have input type $a$, $S=S'$. Similarly, $M$ and $M'$ are uniquely determined by their output type, so that since they both have output type $b$, $M=M'$.

%One can prove in a similar way as in \cite{alex2020pbscalculus} that for any diagram $D$, the function $(c,p)\mapsto (c^D_{c,p},p^D_{c,p})$ is a bijection. %Let $s_S\colon\mapsto (c^S_{c,p},p^S_{c,p})$ and $s_M\colon\mapsto (c^M_{c,p},p^M_{c,p})$. Let $a',b'$ be such that $S:a\to a'$, $M:b'\to b$ and
%This is in particular the case for $S$ and $M$, and since additionally their semantics
Let $S^{-1}$ and $M^{-1}$ be the horizontal reflections of respectively $S$ and $M$, that is, the diagrams obtained by replacing $\xstikzfig{beamsplitterNRwB}$ by $\xstikzfig{beamsplitterRNBw}$ in $S$ and $\xstikzfig{beamsplitterRNBw}$ by $\xstikzfig{beamsplitterNRwB}$ in $M$. One has $\eqref{bsbsmergesplit}\vdash M^{-1}\circ N\circ S^{-1} = P\circ F\circ G$ and $\eqref{bsbsmergesplit}\vdash M^{-1}\circ N'\circ S^{-1} = P'\circ F'\circ G'$, so that by \cref{soundnessCPBS}, $\interp{M^{-1}\circ N\circ S^{-1}} = \interp{P\circ F\circ G}=\interp{M^{-1}\circ N'\circ S^{-1}} = \interp{P'\circ F'\circ G'}$. % In particular, the semantics of $P\circ F\circ G$ (resp. $P'\circ F'\circ G'$) is uniquely determined by the semantics of $N$ (resp. $N'$).
For any $c,p$, one has $\interp{P\circ F\circ G}=((c^F_{c,p},p^P_{c,p}),U^G_{c,p})$ and\\
$\interp{P'\circ F'\circ G'}=((c^{F'}_{c,p},p^{P'}_{c,p}),U^{G'}_{c,p})$, %and it is easy to see that $G$, $F$ and $P$ are uniquely determined by
so that for any $c,p$, $U^{G}_{c,p}=U^{G'}_{c,p}$, $c^{F}_{c,p}=c^{F'}_{c,p}$ and $p^{P}_{c,p}=p^{P'}_{c,p}$. Because of their respective forms required by \cref{defNFcoloree}, %$G$ (resp. $G'$) is uniquely determined by the family of the $U^{G}_{c,p}$ (resp. $U^{G'}_{c,p}$), so that $G=G'$; $F$ (resp. $F'$) is uniquely determined by the family of the $c^{F}_{c,p}$ (resp. $c^{F'}_{c,p}$), so that $F=F'$; and $P$ (resp. $P'$) is uniquely determined by the family of the $p^{P}_{c,p}$ (resp. $p^{P'}_{c,p}$), so that $P=P'$.
$G$, $G'$, $F$, $F'$, $P$ and $P'$ are uniquely determined by the family of, respectively, the $U^{G}_{c,p}$, the $U^{G'}_{c,p}$, the $c^{F}_{c,p}$, the $c^{F'}_{c,p}$, the $p^{P}_{c,p}$, and the $p^{P'}_{c,p}$. Hence, $G=G'$, $F=F'$ and $P=P'$.
%\Acom{peut-être relire encore un peu}
%Let $X'', Y''$ be such that $S:X\to X''$ and $M:Y''\to Y$. Since $(c,p)\mapsto(c^S_{c,p},p^S_{c,p})$ is surjective on the set of couples $(c',p')\in X''$ and $(c,p)\mapsto(c^M_{c,p},p^M_{c,p})$ is injective, $\interp{N}=\interp{N'}$ implies %$\interp{P\circ F\circ G}=\interp{P'\circ F'\circ G'}$
%$\forall (c,p)\in X'',c^{P\circ F\circ G}_{c,p}=c^{P'\circ F'\circ G'}_{c,p}\wedge p^{P\circ F\circ G}_{c,p}=p^{P'\circ F'\circ G'}_{c,p}\wedge w^{P\circ F\circ G}_{c,p}=w^{P'\circ F'\circ G'}_{c,p}$. It is easy to see that $G$, $F$ and $P$ (resp. $G'$, $F'$ and $P'$) are uniquely determined by their semantics. Moreover, since $F$ and $P$ (resp. $F'$ and $P'$) do not contain any gates, $G$ and $P$ (resp. $G'$ and $P'$) do not contain any negations, and $G$ and $F$ (resp. $G'$ and $F'$) do not contain any swaps or beam splitters, one has $\forall(c,p)\in X'', (G,c,p)\xRightarrow{w^{P\circ F\circ G}_{c,p}}(c,p)$ (resp. $\forall(c,p)\in X'', (G',c,p)\xRightarrow{w^{P'\circ F'\circ G'}_{c,p}}(c,p)$), $\forall(c,p)\in X'', (F,c,p)\Rightarrow(c^{P\circ F\circ G}_{c,p},p)$ (resp. $\forall(c,p)\in X'', (F',c,p)\Rightarrow(c^{P'\circ F'\circ G'}_{c,p},p)$) and $\forall(c,p), (P,c,p)\Rightarrow(c,p^{P\circ F\circ G}_{c,p})$ (resp. $\forall(c,p), (P',c,p)\Rightarrow(c,p^{P'\circ F'\circ G'}_{c,p})$). Therefore, $G=G'$, $F=F'$ and $P=P'$, which gives us the result.
%%Passing through $S$ or $S'$ leads a ``classical'' particle to a different wire for each of its possible input states of polarisation and position, and each wire between $S$ and $M$ %or $S'$ and $M'$
%%in $N$ or $N'$ can be reached by such a particle. For each possible such input state $\ket{c,p}$, we have that $\interp{N}(\ket{c,p,0})$ is of the form $\ket{c',p'}\oplus W\ket{0}$. The sequence of variables $W$ gives us the sequence of gates that is on the wire associated with $\ket{c,p}$, and we have $c'=c$ if and only if there is a \xntikzfig{negww} on the wire associated with $\ket{c,p}$. Therefore, $G=G'$ and $F=F'$. Finally, since the wires on the left of each beam splitter in $M$ have different colours, $p'$ uniquely determines the position of the particle just before passing through $M$. Therefore, the data of the $p'$ for all possible $\ket{c,p}$ allows us to know precisely how $P$ and $P'$ permute the positions, and by the axioms of the PROP this data entirely characterises $P$ and $P'$. Hence, $P=P'$.

\subsection{Proof of Theorem \ref{minimalityCPBS}}\label{preuveminimalityCPBS}

%each instance of Equations \eqref{neguRB} and \eqref{ubscol}% and \eqref{bouclevideUR}
%, for each instance of Equation \eqref{fusionUVR} without $I$ gates in the left-hand side, for each class of instances of Equation \eqref{bouclevideUR} given by an equivalence class of elements of $\M$ for the equivalence relation $\sim_{\mathrm{conj}}^*$ defined as the transitive closure of $\sim_{\mathrm{conj}}$ defined by $U\sim_{\mathrm{conj}}V$ if there exists $W,T\in\M$ such that $U=WT$ and $V=TW$, and for each of %Equations \eqref{idboxR} and \eqref{nbscol} to %\eqref{bouclevideR}
\begin{itemize}
\item \cref{idboxR,nbscol,negnegRBR,negnegBRB,bsbssplitmerge,bsbsmergesplit,bsxcol,xbscol,bsbigebre,bsnrrn,bsrnnr,bsnnbb,bsbbnn}
\item each instance of Equations \eqref{neguRB} and \eqref{ubscol}
\item the class of all instances of Equation \eqref{fusionUVR} without $I$ gates in the left-hand side
\item each class of instances of Equation \eqref{bouclevideUR} given by an equivalence class of elements of $\M$ for the equivalence relation $\sim_{\mathrm{conj}}^*$, defined as the transitive closure of $\sim_{\mathrm{conj}}$, itself defined by $U\sim_{\mathrm{conj}}V$ if there exists $W,T\in\M$ such that $U=WT$ and $V=TW$
\end{itemize}
we give an invariant that is satisfied by exactly one side of the considered equation (or of each element of the considered class of instances of Equation \eqref{fusionUVR} or \eqref{bouclevideUR}), and such that for any diagram $D$, applying any other equation or instance %else
inside $D$ (that is, replacing a sub-diagram of $D$ that matches one side of the equation by the other side) preserves the fact that $D$ satisfies the invariant or not. In each case, this proves that the equations that break the invariant are not consequences of those that preserve it inside any diagram. %\Acom{peut-être \`a clarifier, peut-être dire pourquoi ça prouve l'indépendance}
\Acom{raccourcir la phrase}

Note that the instances of Equation \eqref{fusionUVR} with an $I$ gate in the left-hand side are consequences of Equation \eqref{idboxR}, and that the elements of a class of instances of Equation \eqref{bouclevideUR} are consequences of any single instance of Equation \eqref{bouclevideUR} of the same class together with Equation \eqref{fusionUVR}.

\begin{itemize}
\item For Equation \eqref{idboxR}, the invariant is that at least one gate can be reached by a particle from an input wire.
\item For the class of all instances of Equation \eqref{fusionUVR} without $I$ gates in the left-hand side, the invariant is the maximum number of non-$I$ gates that a particle coming from an input wire can traverse along its path in the diagram.
\item For each instance of Equation \eqref{neguRB} given by a particular %variable
$U$, the invariant is that all gates labelled with $U$ are red.
\item For Equation \eqref{nbscol}, the invariant is that the diagram contains a %\Acom{at least one ?}
(black) \xntikzfig{neg}.
%\item For Equation \eqref{bouclevideR}, the invariant is that %the diagram is nonempty and \Acom{all gates are accessible from the input. clarifier la notion d'accessibilité, mais de toute façon ça ne marche pas} gate-free. \Acom{ne marche pas non plus}
%there exists a wire in the diagram and a ``classical'' polarisation $\Vpol$ or $\Hpol$ such that a particle starting in this wire with this polarisation turns infinitely in the diagram without ever traversing any gate. Note that \cref{bouclevideR} can be seen as the instance of \cref{bouclevideRnonbornee} with $m=0$, and that this invariant can be obtained by taking $m=0$ in the proof of independence of \cref{bouclevideRnonbornee} below.
\item For each instance of Equation \eqref{ubscol} given by a particular %variable
$U$, the invariant is that the diagram contains a (black) \xgtikzfig{gateU}.
%\Acom{ou alors, all gates labelled with $U$ are black.}
%\item For any instance of Equation \eqref{bouclevideUR} given by a particular variable $U$, the invariant is that the diagram contains at least one gate labelled with $U$.  \Acom{ou bien invariant de l'équation \eqref{bouclevideRnonbornee} avec $m=1$}
\item For each class of instances of Equation \eqref{bouclevideUR}, the invariant is that there exists a wire in the diagram and a polarisation $\Vpol$ or $\Hpol$ such that the path of a particle starting from this wire with this polarisation is a closed loop, and that the product of the labels of the gates traversed by the particle before getting back to its starting point with its initial polarisation for the first time, is an element of the equivalence class (note that this does not depend on the choice of the starting point).
\item For Equation \eqref{negnegRBR}, the invariant is that all wires are red.
\item For Equation \eqref{negnegBRB}, the invariant is that %all wires connected to the input are blue. \Acom{Marche pour certains diagrammes donc OK pour la preuve, mais pas pour tous les diagrammes a cause de \eqref{bsbsmergesplit}. Il faut clarifier ``connected to the input''.}\Acom{en fait ne marche pas}
no particle entering the diagram by a blue input wire can reach the output without passing through a negation at some point in the diagram. Note that \cref{negnegRBR} cannot change this invariant because in order to reach a red wire, the particle coming from a blue wire has to get its polarisation changed, and therefore to pass through a negation.
\item For Equation \eqref{bsbssplitmerge}, the invariant is that all wires are black and the diagram is nonempty and does not contain any \xstikzfig{beamsplitter}.
\item For Equation \eqref{bsbsmergesplit}, the invariant is that the diagram contains at least one black wire.
\item For Equation \eqref{bsxcol}, the invariant is that the diagram contains at least one generator among $\xstikzfig{beamsplitterwBNR}$, $\xstikzfig{beamsplitter}$, $\xstikzfig{beamsplitterRNNR-s-label}$, $\xstikzfig{beamsplitterBBNN-s-label}$ and $\xntikzfig{neg}$.
\item For Equation \eqref{xbscol}, the invariant is that the diagram contains %a \xstikzfig{beamsplitterBwRN} or a \xstikzfig{beamsplitter}.
at least one generator among $\xstikzfig{beamsplitterBwRN}$, $\xstikzfig{beamsplitter}$, $\xstikzfig{beamsplitterNRRN-s-label}$ and $\xstikzfig{beamsplitterBBNN-s-label}$.
\item For Equation \eqref{bsbigebre}, the invariant is that the diagram contains a \xstikzfig{beamsplitter}.
\item For Equation \eqref{bsnrrn}, the invariant is that the diagram contains a \xstikzfig{beamsplitterNRRN-s-label}.
\item For Equation \eqref{bsrnnr}, the invariant is that the diagram contains a \xstikzfig{beamsplitterRNNR-s-label}.
\item For Equation \eqref{bsnnbb}, the invariant is that the diagram contains a \xstikzfig{beamsplitterNNBB-s-label}.
\item For Equation \eqref{bsbbnn}, the invariant is that the diagram contains a \xstikzfig{beamsplitterBBNN-s-label}.
\end{itemize}

%Finally, for any $m\geq 2$ and $U_1,...,U_m$, the corresponding instance of Equation \eqref{bouclevideRnonbornee} is not a consequence of the set of equations composed of
%\item all possible sound equations with strictly less than $m$ gates on each side
%\item all instances of Equation \eqref{bouclevideRnonbornee} with strictly more than $m$ gates
%\item all instances of Equation \eqref{bouclevideRnonbornee} with exactly $m$ gates except those whose left-hand side is of the form \tikzfig{bouclevideUjRUmRU1RUjmoinsunR-label} for some $j\in\{1,...,m\}$.
%Indeed, first, applying a sound equation with strictly less than $m$ gates on each side preserves the invariant that there exists a wire in the diagram and a ``classical'' polarisation $\Vpol$ or $\Hpol$ such that a particle starting in this wire with this polarisation passes through $U_1,...,U_m$ in order, repeatedly and without passing through any other gates, because such an equation necessarily acts on a strict subset of the set of gates $\{\xgtikzfig{gateU1rosefonce},...,\xgtikzfig{gateUmrosefonce}\}$ (note, however, that the equations can change the colours of the gates) and therefore cannot take the trace into account. Since the instances of Equation \eqref{bouclevideRnonbornee} listed above do not satisfy this invariant on any of their two sides, they can only be applied to a sub-diagram that does not contain any of the gates of the sequence $\xgtikzfig{gateU1rosefonce},...,\xgtikzfig{gateUmrosefonce}$% that satisfies the invariant
%. Thus, the set of equations considered cannot remove this sequence from the left-hand side of the instance of Equation \eqref{bouclevideRnonbornee} under consideration, and therefore cannot transform it into the right-hand side. \Acom{a relire}

\subsection{Proof of Theorem \ref{stairsoptimal}}\label{preuvestairsoptimal}

%\Acom{à mettre après : Let $P=\tikzfig{superpetpermsnegpotentiels}$ be a diagram in stair form and let $P'$ be any diagram equivalent to $P$. Let $\{X_i\}_{i=1,...,p}$ be the partition of $\{0,...,|X|-1\}$ such that an index $j$ is in $X_i$ if the input wire of $P$ of index $j$ is connected to $C_i$. Similarly, let $\{Y_i\}_{i=1,...,p}$ be the partition of $\{0,...,|Y|-1\}$ such that an index $j$ is in $Y_i$ if the output wire of $P$ of index $j$ is connected to $C_i$. \Acom{conflit de notation avec $p$, il faut changer} One has $\forall i,\forall c,p,(p\in X_i\Leftrightarrow p^P_{c,p}\in Y_i)$. It is easy to see that $\{X_i\}_{i=1,...,p}$ is the finest partition of $\{0,...,|X|-1\}$ such that there exists $\{Y_i\}_{i=1,...,p}$ satisfying this property. That is, for any other partition $\{X'_j\}_{j=1,...,q}$ such that there exists $\{Y'_j\}_{j=1,...,q}$ with $\forall j,\forall c,p,(p\in X'_j\Leftrightarrow p^P_{c,p}\in Y'_j)$, one has $q\leq p$ and there exists a partition $\{I_j\}_{j=1,...,q}$ of $\{1,...,p\}$ such that $\forall j,X'_j=\bigcup_{i\in I_j}X_i$. %Note that one additionally has $\forall j,Y'_j=\bigcup_{i\in I_j}Y_i$.
%Symmetrically,  $\{Y_i\}_{i=1,...,p}$ is the finest partition of $\{0,...,|Y|-1\}$ such that there exists $\{X_i\}_{i=1,...,p}$ satisfying this property.}
%\Acom{améliorer les notations}

Given any gate-free diagram $Q:d\to e$, we denote by $\{a^{Q}_i\}_{i=1,...,k_Q}$ the finest partition of $\{0,...,|d|-1\}$ such that there exists a partition $\{b^Q_i\}_{i=1,...,k_Q}$ of $\{0,...,|e|-1\}$ satisfying $\forall i,\forall c,p,(p\in a_i\Leftrightarrow p^P_{c,p}\in b_i)$. It is easy to see that the partition $\{b^Q_i\}_{i=1,...,k_Q}$ is unique and that symmetrically, it is the finest partition of $\{0,...,|e|-1\}$ such that there exists a partition $\{{d}^{Q}_i\}_{i=1,...,k_Q}$ of $\{0,...,|d|-1\}$ satisfying $\forall i,\forall c,p,(p\in {d}^Q_i\Leftrightarrow p^P_{c,p}\in b_i)$ (which of course implies that $\forall i,{d}^Q_i=a^Q_i$).

We now want to prove that $p_L(Q)\geq |d|-k_Q$, where $p_L(Q)$ is the number of PBS in $Q$ that belong to the set $\mathcal{L}\coloneqq\{\stikzfig{beamsplitter},\stikzfig{beamsplitterNRRN-s-label},\stikzfig{beamsplitterRNNR-s-label},\stikzfig{beamsplitterNNBB-s-label},\stikzfig{beamsplitterBBNN-s-label},\stikzfig{beamsplitterRNBw},\stikzfig{beamsplitterBwRN}\}$. For this purpose, we remark that $Q$ can be built by starting from the %identity diagram $\mathrm{Id}_{d}=\bigotimes_{i=1,...,|a|}\ntikzfig{cfilcourt-s-ai}$, where $d=a_1\oplus\cdots\oplus a_{|a|}$ with $\forall i, a_i\in\{\vtype,\htype,\top\}$,
empty diagram and applying a finite number of transformations taken among the following ones:
\begin{enumerate}
\item append %$\stikzfig{beamsplitter}$, $\stikzfig{beamsplitterNRRN-s-label}$, $\stikzfig{beamsplitterRNNR-s-label}$, $\stikzfig{beamsplitterNNBB-s-label}$, $\stikzfig{beamsplitterBBNN-s-label}$, $\stikzfig{beamsplitterRNBw}$ or $\stikzfig{beamsplitterBwRN}$
an element of $\mathcal{L}$
to the right of $Q$ (that is, parallelly compose this element with identities in a way that gives a diagram whose input type matches the output type of $Q$, and sequentially compose the two diagrams)
\item append $\stikzfig{beamsplitterNRwB}$, $\stikzfig{beamsplitterwBNR}$, $\sgtikzfig{cneg}$ or $\stikzfig{cswap}$ to the right of $Q$
\item change $Q$ into $Tr_a(Q)$, provided that $Q$ has a suitable type
\item change $Q$ into $Q\oplus\ntikzfig{cfilcourt-s}$.
\end{enumerate}
The empty diagram satisfies the inequality since $p_L(\ntikzfig{diagrammevide-s})=0=|I|-k_{\ntikzfig{diagrammevide-xs-regulier}}$. Hence it suffices to prove that each of these transformations preserves it.

\begin{enumerate}
\item Appending a PBS of $\mathcal{L}$ to the right of $Q$ increases $p_L(Q)$ by $1$, and does not affect the ${d}^Q_i$ except one or two of them which is/are replaced in the partition by at least one set, so that $k_Q$ cannot decrease by more than $1$. Additionally, this does not change $d$, so that $|d|-k_Q$ does not increase by more than $1$. Thus this preserves the inequality.
\item Appending $\stikzfig{beamsplitterNRwB}$, $\stikzfig{beamsplitterwBNR}$, $\sgtikzfig{cneg}$ or $\stikzfig{cswap}$ neither  changes $d$ nor the ${d}^Q_i$ (it only %increases the size of one of
the ${e}^Q_i$% in the case of $\stikzfig{beamsplitterNRwB}$ and $\stikzfig{beamsplitterwBNR}$, and may exchange two elements_Acom{...} in the case of $\stikzfig{cswap}$
), and also does not change $p_L(Q)$, so that the inequality is preserved.
\item Changing $Q$ into $Tr_a(Q)$ does not affect the ${d}^Q_i$ except one or two of them (namely, this containing the last position $|d|-1$ and this corresponding to the ${e}^Q_i$ that contains the last position %$|d|-1$
$|e|-1$). If there exists $i$ such that %${d}^Q_i={e}^Q_i=\{|d|-1\}$
${d}^Q_i=\{|d|-1\}$ and ${e}^Q_i=\{|e|-1\}$, then this only affects ${d}^Q_i$ and removes it from the partition, which decreases $k_Q$ by $1$, while $|d|$ decreases by $1$ and $p_L(Q)$ does not change, hence the inequality is preserved. If this is not the case, then the one or two affected ${d}^Q_i$ are replaced by at least one set in the partition, which does not decrease $k_Q$ by more than $1$, while $|d|$ still decreases by $1$ and $p_L(Q)$ still does not change, so that the inequality is preserved.
\item Changing $Q$ into $Q\oplus\ntikzfig{cfilcourt-s}$ increases $|d|$ by $1$, and adds a set to the partition, which increases $k_Q$ by $1$ too. Additionally, this does not change $p_L(Q)$, so that the inequality is preserved.
\end{enumerate}
This finishes proving that %one has
$p_L(Q)\geq |d|-k_Q$% for any $Q$
. Symmetrically, one can also prove that $p_R(Q)\geq |e|-k_Q$, where $p_R(Q)$ is the number of PBS in $Q$ that belong to the set $\mathcal{R}\coloneqq\{\stikzfig{beamsplitter},\stikzfig{beamsplitterNRRN-s-label},\stikzfig{beamsplitterRNNR-s-label},\stikzfig{beamsplitterNNBB-s-label},\stikzfig{beamsplitterBBNN-s-label},\stikzfig{beamsplitterNRwB},\stikzfig{beamsplitterwBNR}\}$.

Given $P=%\ptikzfig{superpetpermsnegpotentiels}{0.7}{0.7}1
\ptikzfig{superpetpermsnegpotentiels-xl}{1.085}{0.7}1:a\to b$ a diagram in stair form, %and let $P'$ be any diagram equivalent to $P$. L
let $\{a_i\}_{i=1,...,k}$ be the partition of $\{0,...,|a|-1\}$ such that an index $j$ is in $a_i$ if the input wire of $P$ of index $j$ is connected to $C_i$. Similarly, let $\{b_i\}_{i=1,...,k}$ be the partition of $\{0,...,|b|-1\}$ such that an index $j$ is in $b_i$ if the output wire of $P$ of index $j$ is connected to $C_i$. %\Acom{conflit de notation avec $p$, il faut changer (ça a été fait en partie, c'est peut-être suffisant)}
One has $\forall i,\forall c,p,(p\in a_i\Leftrightarrow p^P_{c,p}\in b_i)$. It is easy to see that $\{a_i\}_{i=1,...,k}$ is the finest partition of $\{0,...,|a|-1\}$ such that there exists $\{b_i\}_{i=1,...,k}$ satisfying this property, %. That is, for any other partition $\{d_j\}_{j=1,...,q}$ such that there exists $\{Y'_j\}_{j=1,...,q}$ with $\forall j,\forall c,p,(p\in d_j\Leftrightarrow p^P_{c,p}\in e_j)$, one has $q\leq p$ and there exists a partition $\{I_j\}_{j=1,...,q}$ of $\{1,...,p\}$ such that $\forall j,a'_j=\bigcup_{i\in I_j}a_i$. %Note that one additionally has $\forall j,e_j=\bigcup_{i\in I_j}b_i$.
%Symmetrically,  $\{b_i\}_{i=1,...,p}$ is the finest partition of $\{0,...,|b|-1\}$ such that there exists $\{a_i\}_{i=1,...,p}$ satisfying this property.
that is, up to reordering the partitions, one has $k=k_P$ and $\forall i,a_i= a_i^{P}\text{ and }b_i=b_i^P$.

Let us decompose $d=x_1\oplus\cdots\oplus x_n$ and $e=y_1\oplus\cdots\oplus y_m$ with $\forall j, x_j,y_j\in\{\vtype,\htype,\top\}$. Since any trace-free diagram $Q$ is equivalent to a diagram in stair form, the preceding paragraph implies that for every $i$ there are four cases:
\begin{enumerate}
\item $\left|{d}^Q_i\right|=\left|{e}^Q_i\right|$, $\forall j\in {d}^Q_i, x_j=\top$ and $\forall j\in {e}^Q_i, y_j=\top$
\item\label{equilibrecolore} $\left|{d}^Q_i\right|=\left|{e}^Q_i\right|$ and exactly one element of ${d}^Q_i$ and one element of ${e}^Q_i$ are not equal to $\top$
\item\label{splitL} $\left|{d}^Q_i\right|=\left|{e}^Q_i\right|+1$, $\forall j\in {e}^Q_i, y_j=\top$ and exactly two elements of ${d}^Q_i$ are not equal to $\top$
\item\label{splitR} $\left|{e}^Q_i\right|=\left|{d}^Q_i\right|+1$, $\forall j\in {d}^Q_i, x_j=\top$ and exactly two elements of ${e}^Q_i$ are not equal to $\top$
\end{enumerate}

Let $s_L(Q)$ be the number of indices $i$ for which we are in Case \ref{splitL}, and $s_R(Q)$ be the number of indices for which we are in Case \ref{splitR}. Let also $p'_L(Q)$ be the number of $\stikzfig{beamsplitterRNBw}$ and $\stikzfig{beamsplitterBwRN}$ in $Q$, and $p'_R(Q)$ be the number of $\stikzfig{beamsplitterNRwB}$ and $\stikzfig{beamsplitterwBNR}$ in $Q$. We now want to prove that $p'_L(Q)\geq s_L(Q)$. The empty diagram satisfies this inequality, so as before, it suffices to prove that this equality is preserved by the four elementary transformations described above.

%\Acom{relire ce qui suit}
\begin{enumerate}
\item Appending $\stikzfig{beamsplitter}$ to the right of $Q$ does not increase $s_L(Q)$. Indeed, by a simple case distinction%\Acom{préciser sur quoi ?}
, it is easy to see that this could only happen if the indices of the wires to which the PBS is plugged were in two different sets $b^Q_i$ and $b^Q_j$ that both correspond to Case \ref{equilibrecolore}. More precisely, this would happen if among the sets that replace $b^Q_i$ and $b^Q_j$ in the new partition, one contains the indices of both non-$\top$ wires. But in this case, %\Aout{if we change the type of the non-$\top$ wire of $a^Q_i$ and $b^Q_i$ into $\top$, then}
by changing $Q$ into a diagram of the form $\tikzfig{Qfilnoirci}$, we obtain a diagram with the same partition% except that  the type of the non-$\top$ wire of $a^Q_i$ and $b^Q_i$ now $\top$
, whose partition undergoes the same transformation when one appends the PBS at the same place, and whose wires have same type except that all wires of $a^Q_i$ and $b^Q_i$ are of type $\top$. This implies that appending the PBS cannot turn $a^Q_i$, $b^Q_i$, of $a^Q_i$ and $b^Q_i$ into sets among which one or more would be in Case \ref{splitL} or \ref{splitR}. A similar proof, with the difference that the PBS is appended to the type-changing wire, shows that appending $\stikzfig{beamsplitterNRRN-s-label}$, $\stikzfig{beamsplitterRNNR-s-label}$, $\stikzfig{beamsplitterNNBB-s-label}$ or $\stikzfig{beamsplitterBBNN-s-label}$ also does not increase $s_L(Q)$.

Additionally, appending $\stikzfig{beamsplitterRNBw}$ or $\stikzfig{beamsplitterBwRN}$ decreases by $2$ the number of non-$\top$ wires in the one or two sets $b^Q_i$ concerned, which implies that a necessary condition so that some of the new sets are in Case \ref{splitR} is that the PBS has been appended to wires in two different sets $b^Q_i$ and $b^Q_j$ both already in Case \ref{splitR}. Thus, appending $\stikzfig{beamsplitterRNBw}$ or $\stikzfig{beamsplitterBwRN}$ does not increase $s_R(Q)$. Finally, appending $\stikzfig{beamsplitterRNBw}$ or $\stikzfig{beamsplitterBwRN}$ can create at most one couple of sets $a^Q_i$ and $b^Q_i$ in Case \ref{splitL}, only if appended to two sets $b^Q_i$ and $b^Q_j$ both in Case \ref{equilibrecolore}. This increases $s_L(Q)$ by $1$, while, since $\stikzfig{beamsplitterRNBw}$ or $\stikzfig{beamsplitterBwRN}$ is added, $p'_L(Q)$ increases by $1$. Thus, the inequality is preserved.
\item It is easy to see that appending $\sgtikzfig{cneg}$ or $\stikzfig{cswap}$ does not change $s_L(Q)$ or $s_R(Q)$, and appending $\stikzfig{beamsplitterNRwB}$ or $\stikzfig{beamsplitterwBNR}$ only affects one set $b^Q_i$ and does not change the types of the wires of $a^Q_i$, therefore this cannot increase $s_L(Q)$.
\item By changing the type of an input and an output wire in a similar way as for the case of appending $\stikzfig{abbeamsplitter}$, one can show that changing $Q$ into $Tr_a(Q)$ cannot increase $s_L(Q)$. %Since this also does not change $P'_L(Q)$, the inequality is preserved.
\item Changing $Q$ into $Q\oplus\ntikzfig{cfilcourt-s}$ adds a singleton to the partition of $[d]$ and of $[e]$, since the two singletons are not in Case \ref{splitL}, this does not increase $s_L(Q)$.
\end{enumerate}
This finishes proving that $p'_L(Q)\geq s_L(Q)$. Symmetrically, one can also prove that $p'_R(Q)\geq s_R(Q)$.

Note that given any diagram in stair form $P:a\to b$, one has $p_L(P)= |a|-k_P$, $p_R(P)= |b|-k_P$, $p'_L(P)= s_L(P)$ and $p'_R(P)= s_R(P)$, that is, $P$ reaches the equality in all four inequalities that we have just proved. Note additionally that given any diagram $Q:d\to e$, one has $\nopbs(Q)=p_R(Q)+p'_L(Q)$ (where $\nopbs(Q)$ is the total number of PBS in $Q$). Hence, $\nopbs(Q)\geq |e|-k_Q+s'_L(Q)$. Since the diagrams in stair form reach the lower bound, they are PBS-optimal.

%The fact that any gate-free diagram is equivalent to a diagram
%\Acom{Il faut encore prouver qu'il y a au moins un $\stikzfig{beamsplitterNRwB}$ ou un $\stikzfig{beamsplitterwBNR}$ pour chaque $i$ t.q. ${Y'}^Q_i>{X'}^Q_i$, et la version en miroir de ça.}

%for any $i$ and for any nonempty, strict subset $\Upsilon$ of $Y_i$, there exists a position $p\in X_i$ and a polarisation $c$ such that $p^P_{c,p}\in\Upsilon$ and $p^P_{\neg c,p}\in Y_i\setminus\Upsilon$, which implies that there is at least one PBS that is connected, possibly through other PBS, to an output wire of index in $\Upsilon$ and an output wire with index in $Y_i\setminus\Upsilon$. Therefore, one can build an increasing sequence $Y_i^{(1)}\subsetneq\cdots\subsetneq Y_i^{(|Y_i|)}$ of subsets of $Y_i$, such that $Y_i^{(1)}=\{p_1\}$ for an arbitrary element $p_1$ of $Y_i$, and for every $j$, $Y_i^{(j+1)}=Y_i^{(j)}\cup\{p_{j+1}\}$ where there is a PBS connected to the output wire of $P'$ of index $p_{j+1}$ and to an output wire of $P'$ of index in $Y_i^{(j)}$. % $p_{j+1}$ connected to has one more element  In a PBS-free diagram, the finest partition is composed of singletons, adding and adding a PBS

\subsection{Proof of Theorem \ref{optimalitequanduneportedechaque}}\label{preuveoptimalitequanduneportedechaque}

Let $D:a\to b$ be an abstract diagram in PGT form in which all gates bear different labels. We write in in the form
\[\tikzfig{CPNFnoire}\]
with $P$ in stair form and $U_1, ..., U_\ell\in\GG$ (where all wires and gates can be of arbitrary colours).

For each $(c,p)\in [a]$, let $p^{(1)}_{c,p}, ..., p^{(\ell_{c,p})}_{c,p}$ be the sequence of positions such that $w^D_{c,p}=U_{p^{(1)}_{c,p}}...U_{p^{(\ell_{c,p})}_{c,p}}$ (with $\ell_{c,p}=|w^D_{c,p}|$). This sequence is determined without ambiguity since the names $U_i$ are pairwise distinct. There exists a sequence of polarisations $c^{(1)}_{c,p}, ..., c^{(\ell_{c,p})}_{c,p}$ such that $\interp{P}(c,p)=((c^{(1)}_{c,p},|b|+p^{(1)}_{c,p}),\epsilon)$, $\forall i\in\{1,...,\ell_{c,p}-1\},\interp{P}(c^{(i)}_{c,p},|a|+p^{(i)}_{c,p})=((c^{(i+1)}_{c,p},|b|+p^{(i+1)}_{c,p}),\epsilon)$, %, ..., $(P,c^{(\ell_{c,p}-1)}_{c,p},|a|+p^{(\ell_{c,p}-1)}_{c,p})\Rightarrow(c^{(\ell_{c,p})}_{c,p},|b|+p^{(\ell_{c,p})}_{c,p})$
and $\interp{P}(c^{(\ell_{c,p})}_{c,p},|a|+p^{(\ell_{c,p})}_{c,p})=((c^D_{c,p},p^D_{c,p}),\epsilon)$%, for some sequence of polarisations $c^{(1)}_{c,p}, ..., c^{(\ell_{c,p})}_{c,p}$
(where $\epsilon$ denotes the empty word).

Given a query-PBS-optimal diagram $D'$ equivalent to $D$, up to applying the query optimisation procedure and the PGT procedure, we can assume that $D'$ is in PGT form. Note that any query-optimal $\GG^*$-diagram $E$ that contains only elementary %\Acom{single-letter}
gates (i.e. single-letter gates) necessarily satisfies that, for every $U\in\GG$, it contains exactly $\left\lceil\sum_{(c,p)\in [a]}\frac{|w_{c,p}^E|_U}2\right\rceil$ black gates labelled with $U$, and one red or blue gate labelled with $U$ if and only if $\sum_{(c,p)\in [a]}|w_{c,p}^E|_U$ is odd. Since $D$ and $D'$ both satisfy this property and have the same semantics, this implies that they have the same gates up to turning some red gates into blue gates and vice-versa. That is, up to slightly deforming it in order to permute the gates, we can put $D'$ in the form
\[\tikzfig{CPNFnoirePprime}\]
with $P'$ in stair form. %For every $i\in\{1, ...,\ell\}$, the gate labelled with $U_i$ is black if $\noa_U(D')=2$, and red or blue if $\noa_U(D')=1$. Since
%Note that the gates are the same as in $D$ up to changing blue into red
%\Acom{justifier pourquoi on a les mêmes labels ?}
For each $(c,p)\in[a]$, there also exists a sequence of polarisations $c^{\prime(1)}_{c,p}, ..., c^{\prime(\ell_{c,p})}_{c,p}$ such that $\interp{P'}(c,p)=((c^{\prime(1)}_{c,p},|b|+p^{(1)}_{c,p}),\epsilon)$, $\forall i\in\{1,...,\ell_{c,p}-1\},\interp{P'}(c^{\prime(i)}_{c,p},|a|+p^{(i)}_{c,p})=((c^{\prime(i+1)}_{c,p},|b|+p^{(i+1)}_{c,p}),\epsilon)$, %, ..., $(P,c^{\prime(\ell_{c,p}-1)}_{c,p},|a|+p^{(\ell_{c,p}-1)}_{c,p})\Rightarrow(c^{\prime(\ell_{c,p})}_{c,p},|b|+p^{(\ell_{c,p})}_{c,p})$
and $\interp{P'}(c^{\prime(\ell_{c,p})}_{c,p},|a|+p^{(\ell_{c,p})}_{c,p})=((c^D_{c,p},p^D_{c,p}),\epsilon)$%, for some sequence of polarisations $c^{\prime(1)}_{c,p}, ..., c^{\prime(\ell_{c,p})}_{c,p}$

Let $P''$ be the diagram obtained from $P'$ by adding, for every position $q$ such that there exist $c,p$ and $i\in\{1,...,\ell_{c,p}\}$ satisfying $q=p^{(i)}_{c,p}$ and $c^{(i)}_{c,p}\neq c^{\prime(i)}_{c,p}$, a negation on input wire $|a|+q$ and on output wire $|b|+q$. Let $d$ be such that $P:a\oplus d\to b\oplus d$. It is easy to see that for every $(c,p)\in[a]$, and for every couple $(c,p)\in[a\oplus d]$ with $p\geq |a|$ that can be written as $(c^{\prime(i)}_{c',p'},|a|+p^{(i)}_{c',p'})$ for some $c',p'\in[a]$ and $i\in\{1,...,\ell_{c',p'}\}$, one has $\interp{P''}(c,p)=\interp{P}(c,p)$. Since $D$ is query-optimal, every black gate can be reached from two basis states $(c,p)\in[a]$ and every nonblack gate can be reached from one basis state, which implies that every couple $(c,p)\in[b\oplus d]$ with $p\geq |b|$ can be written as $(c^{\prime(i)}_{c',p'},|b|+p^{(i)}_{c',p'})$, and therefore, every couple $(c,p)\in[a\oplus d]$ with $p\geq |a|$ can be written as $(c^{\prime(i)}_{c',p'},|a|+p^{(i)}_{c',p'})$. Hence, $P''$ has the same semantics as $P$. Since $P''$ contains the same number of PBS as $P'$ and by \cref{stairsoptimal}, $P$ is PBS-optimal, this implies that $P$ contains at most as many PBS as $P'$, that is, $D$ contains at most as many PBS as $D'$. Hence, $D$ is query-PBS-optimal.

%The length of this sequence of arrows, as well as %the sequence of the $|X|+p^{(i)}_{c,p}$\Acom{et des $|Y|+p^{(i)}_{c,p}$}
%all positions appearing in it, and the final couple $(c^D_{c,p},p^D_{c,p})$, depend only on the word $w^D_{c,p}$. Hence, given another diagram $D'$ in PGT form equivalent to $D$, if we put $D'$ in the form
%(which can be done by mere deformation and keeps it in PGT form), then the sequences of arrows formed using $P'$ instead of $P$ have the same length, the same %sequences of $p^{(i)}_{c,p}$
%positions in the same places, and the same final $(c^D_{c,p},p^D_{c,p})=(c^{D'}_{c,p},p^{D'}_{c,p})$. %Moreover, since %each letter appears at most twice among all $w^D_{c,p}$,
%%%each gate can be traversed at most twice among
%%the maps $(c,p)\mapsto(c^P_{c,p},p^P_{c,p})$ and $(c,p)\mapsto(c^{P'}_{c,p},p^{P'}_{c,p})$ are bijections, each position $p\geq|X|$ appears at most twice as a starting point%, and each position $p\geq|Y|$, at most twice as an arrival point, among all of these sequences of arrows
%%, and is associated with a different polarisation the two times (and each position $p\geq |Y|$ appears as an arrival point in the arrows just before those where the position $p-|Y|+|X|$ appears as a starting point, and is associated with the same polarisation each time)$. Therefore, the two sequences differ by swapping the two polarisations associated t
%This implies that there is a one-to-one correspondence between the arrows of the word path semantics of $P$ and the arrows of the word path semantics of $P$, such that each arrow $(P,c,p)\Rightarrow(c',p')$ corresponds to an arrow $(P',c'',p)\Rightarrow(c''',p')$ with the same positions. Moreover, since the maps $(c,p)\mapsto(c^P_{c,p},p^P_{c,p})$ and $(c,p)\mapsto(c^{P'}_{c,p},p^{P'}_{c,p})$ are bijections, each position appears at most twice as a starting point (resp. an arrival point), and if it appears twice, the it is associated with a different polarisation the two times. Therefore, the family of arrows of $P'$ can be obtained from this of $P$ by applying a sequence of elementary operations consisting of swapping the two polarisations associated with the two occurrence of a position as a starting point, swapping the two polarisations associated with the two occurrence of a position as an arrival point, changing the polarisation associated with the single ocurrence of a position that appears only once as a starting point, and changing the polarisation associated with the single ocurrence of a position that appears only once as an arrival point. %This implies that the partitions $\{X^{P}_i\}_{i=1,...,k_P}$ and $\{Y^P_i\}_{i=1,...,k_P}$, as defined in the proof of \cref{stairsoptimal}, are the same as, respectively, $\{X^{P'}_i\}_{i=1,...,k_{P'}}$  $\{Y^{P'}_i\}_{i=1,...,k_{P'}}$, which implies that $P$ and $P'$ have the same number of PBS. %In particular, they have the same number of subsets $k_P=k_{P'}$, so that
%It is clear that these elementary operations do not change the partitions $\{X^{P}_i\}_{i=1,...,k_P}$ and $\{Y^P_i\}_{i=1,...,k_P}$ defined in the proof of \cref{stairsoptimal}, so that these partitions are the same for $P'$. Since $P$ and $P'$ are in stair form, this implies that they have the same number of PBS (namely, $\sum_{i=1}^{k_P}(\max(|X^{P}_i|,|Y^{P}_i|)-1)$). \Acom{expliquer un peu plus ?}
%Thus, all query-optimal diagrams in PGT form that are equivalent to a given query-optimal diagram in PGT form have the same number of PBS, which implies that they are all query-PBS-optimal.

\subsection{NP-hardness results}

\subsubsection{Proof of \cref{gatePBSNPhard}}\label{preuvegatePBSNPhard}

Let $\GG$ be a set a names. We will prove that the problem is already NP-hard when we restrict the input diagram to the family $\mathcal P$ defined as follows:
%We denote by $\mathcal W$ the set of \CPBS-diagrams $D:\top^{\oplus n}\to\top^{\oplus n}$ such that for every $c\in\hv$ and $p\in[n]$, there exists a single letter $a_{c,p}$ such that $(D,c,p)\xRightarrow{a_{c,p}\ }(c,p)$.
%\Acom{alternative :}

\begin{definition}
Given a word $w=w_0...w_{n-1}$ with $w_0,...,w_{n-1}\in\GG$ and a permutation $\sigma$ of $[n]$, we define $\sigma(w)$ as the rearranged word $w_{\sigma(0)}...w_{\sigma(n-1)}$.
\end{definition}

\begin{definition}
We denote by $\mathcal P$ the set of %abstract
$\GG^*$-diagrams $D:\top^{\oplus n}\to\top^{\oplus n}$ such that there exists a word $w=w_0...w_{n-1}\in\GG^n$ %\in\GG^*$ of length $n$
and a permutation $\sigma$ of $[n]$ such that for every $p\in[n]$, %$(D,\Vpol,p)\xRightarrow{w_p\ }(\Vpol,p)$ and $(D,\Hpol,p)\xRightarrow{w_{\sigma(p)}\ }(\Hpol,p)$.
$\interp{D}(\Vpol,p)=((\Vpol,p),w_p)$ and $\interp{D}(\Hpol,p)=((\Hpol,p),w_{\sigma(p)})$.
\end{definition}

We polynomially reduce this restricted problem from the \emph{maximum Eulerian cycle decomposition problem}, also called MAX-ECD \cite{caprara1999eulerian}, which consists of, given an Eulerian undirected graph $G$, finding a maximum-cardinality edge-partition of $G$ into cycles (that is, partitioning the set of edges of $G$ into the maximum number of cycles). %\alexandre{More precisely, we consider the associated decision problem of given an Eulerian undirected graph $G$ and an integer $k$, deciding whether $G$ can be edge-partitioned into at least $k$ cycles.} \Acom{C'est moi qui invente la définition du problème de décision, le papier \cite{caprara1999eulerian} n'en parle pas.}
The NP-hardness of MAX-ECD follows directly from the NP-completeness of the %\emph{triangle partition problem}
problem of %finding an edge-partition of $G$ into triangles
deciding whether $G$ can be edge-partitioned into triangles, which is proved in \cite{holyer1981edgepartition} (it corresponds to the case of the edge-partition into copies of the complete graph $K_3$).
%We polynomially reduce to this restricted problem\Aout{/We prove that this restricted problem is equivalent to}\Acom{Pour avoir equivalence il faut en plus les conditions correspondant au fait que le graphe n'est pas un multigraphe. Voire celles correspondant au fait qu'il est connexe.} the \emph{maximum Eulerian cycle decomposition problem}, also called MAX-ECD \cite{caprara1999eulerian}, which consists of, given an Eulerian undirected graph $G$, finding a maximum-cardinality edge-partition of $G$ into cycles (that is, partitioning the set of edges of $G$ into the maximum number of cycles). The NP-hardness of MAX-ECD follows directly from the NP-hardness of the %\emph{triangle partition problem}
%problem of finding an edge-partition of $G$ into triangles, which is proved in \cite{holyer1981edgepartition} (it corresponds to the case of the edge-partition into copies of the complete graph $K_3$).

The MAX-ECD problem is equivalent to the problem of, given an Eulerian graph $G$,
%Let $G$ be an Eulerian graph. Finding an edge-decomposition of $G$ into cycles is equivalent to
finding a suitable orientation of its edges %\Acom{(that is, a direction for each edge)}
together with an edge-partition of the resulting directed graph into directed cycles, so that the number of cycles is maximal among all possible choices of orientation and partition. Indeed, given these, it suffices to erase the directions of the edges to get an undirected edge-partition into cycles, and given such a partition, it suffices to choose, for each cycle, one of the two possible ways of orienting it.

Given an Eulerian graph $G$, we construct a %\Acom{PBS-}
diagram of $\mathcal P$ as follows: first, we choose an arbitrary orientation of the edges of $G$ %such that each vertex has in- and out-degree equal,
so as to get an Eulerian directed graph $\vec G$ %,
%\Scom{Is it clear that it"'s always possible?}
(which can be done by following an Eulerian circuit of $G$, which itself can be found in polynomial time\Acom{reference ?}) and we associate a label, which is an element of $\GG$, to each vertex of $G$, in such a way that any two distinct vertices bear distinct labels. Without loss of generality, we can assume that the vertices of $G$ are elements of $\GG$ and thereby identify them with their labels. We enumerate the edges of $\vec G$ as
$e_0,...,e_{n-1}$% be any order of the edges of $\vec G$
. %Since $\vec G$ is Eulerian\Acom{peut-être justifier un peu plus en détails},
In $\vec G$, each vertex has in- and out-degree equal, that is, each vertex appears as many times as the head of an arrow as as the tail of an arrow, so that there exists a permutation $\sigma$ of $[n]$ and a word $w=w_0...w_{n-1}\in\GG^n$ such that for any $p\in[n]$, $e_p$ is of the form $(w_p,w_{\sigma(p)})$. We consider the following diagram:
\[C_{w,\sigma}\coloneqq\tikzfig{sigmawsigmainv}\]
where $D_\sigma:\top^{\oplus n}\to\top^{\oplus n}$ is a $\xntikzfig{neg}$-free diagram %\Acom{, gate-free} PBS-diagram \Acom{that is, a \CPBS-diagram generated by $\ntikzfig{diagrammevide-s}$, $\ntikzfig{filcourt-s}$, $\xstikzfig{swap}$, $\xgtikzfig{gateU}$ and \xstikzfig{beamsplitter}}
in stair form\footnote{Note that the type of $D_\sigma$ forces all of its staircases to be %of the form \ptikzfig{escalierbsnoir-abrege}{0.375}{0.6}1.
%monochromatic, i.e.
made only of all-black PBS.}
such that for any $p\in[n]$, %$(D_\sigma,{\Vpol},p)\Rightarrow({\Vpol},p)$ and $(D_\sigma,{\Hpol},p)\Rightarrow({\Hpol},\sigma(p))$
$\interp{D_\sigma}(\Vpol,p)=((\Vpol,p),\epsilon)$ and $\interp{D_\sigma}(\Hpol,p)=((\Hpol,\sigma(p)),\epsilon)$, and $D_\sigma^{-1}$ is the horizontal reflection of $D_\sigma$, which therefore satisfies that for any $p\in[n]$, %$(D_\sigma^{-1},{\Vpol},p)\Rightarrow({\Vpol},p)$ and $(D_\sigma^{-1},{\Hpol},p)\Rightarrow({\Hpol},\sigma^{-1}(p))$
$\interp{D_\sigma^{-1}}(\Vpol,p)=((\Vpol,p),\epsilon)$ and $\interp{D_\sigma^{-1}}(\Hpol,p)=((\Hpol,\sigma^{-1}(p)),\epsilon)$.

For any $p\in[n]$, one has %$(C_{w,\sigma},{\Vpol},p)\xRightarrow{w_p\ }({\Vpol},p)$ and $(C_{w,\sigma},{\Hpol},p)\xRightarrow{w_{\sigma(p)}\ }({\Hpol},p)$
$\interp{C_{w,\sigma}}(\Vpol,p)=((\Vpol,p),w_p)$ and $\interp{C_{w,\sigma}}(\Hpol,p)=((\Hpol,p),w_{\sigma(p)})$. In particular, $C_{w,\sigma}$ is in $\mathcal P$, and for any $p\in[n]$, $w^{C_{w,\sigma}}_{{\Vpol},p}$ is the tail of $e_p$ and $w^{C_{w,\sigma}}_{{\Hpol},p}$ is the head of $e_p$.\footnote{See the end of \cref{defactionsem} for the definition of $w^{C_{w,\sigma}}_{c,p}$% and $p^P_{c,p}$
. Note that we identify words of length $1$ with their single letter.}
%\Acom{Comme ce sont des mots de longueur $1$, peut-être qu'on pourrait utiliser la notation $U^D_{c,p}$ ?}

Let $C_{w,\sigma}^{\mathrm{opt}}$ be a query-PBS-optimal diagram equivalent to $C_{w,\sigma}$. Up to applying the PGT procedure, which can be done in polynomial time and neither changes the gates nor increases the number of PBS, we can assume that $C_{w,\sigma}^{\mathrm{opt}}$ is in PGT form. %Moreover, up to choosing the good order in which to put the gates in Step \ref{putinsnailform} of the procedure, one can assume that $C_{w,\sigma}^{\mathrm{opt}}$ is of the form
That is, up to reordering some wires, it is of the form
\[\tikzfig{PGTw}\]
with $P$ in stair form. Since for every $c,p$, the word $w^{C_{w,\sigma}^{\mathrm{opt}}}_{c,p}$ has length $1$, $P$ is such that for any $c\in\hv$ and $p\in[n]$, one has %$(P,{\Vpol},p)\Rightarrow(c^p_{{\Vpol},p},p+n)$ and $(P,{\Vpol},p+n)\Rightarrow(c^p_{{\Vpol},p+n},p)$.
$p^P_{c,p}\in\{n,...,2n-1\}$ and $p^P_{c,p+n}\in[n]$.

By looking at the semantics of a generic diagram in stair form\Acom{mieux justifier, en s'appuyant sur la preuve du théorème \ref{stairsoptimal}}\Acom{Note that $\interp{\ptikzfig{escalierbsnoir-abrege}{0.375}{0.6}1:\top^{\oplus k}\to \top^{\oplus k}}=(c,p)\mapsto((c,p+1\bmod k),\epsilon)$, therefore it is easy to see ...}, it is easy to see that this implies that up to reordering the wires on the sides of $P$, we can write $C_{w,\sigma}^{\mathrm{opt}}$ in the form
\[\tikzfig{PGTwsplit}\]
where $P_1$ and $P_2$ are two diagrams in stair form. Up to a few more deformations, %we can then write
$C_{w,\sigma}^{\mathrm{opt}}$ is of the form
\[\tikzfig{P1wP2}.\]
Due to the semantics of $C_{w,\sigma}^{\mathrm{opt}}$, for any $c,c'\in\hv$ and $p,p'\in[n]$, if %$(P_1,c,p)\Rightarrow(c',p')$ then $(P_2,c',p')\Rightarrow(c,p)$
$\interp{P_1}(c,p)=((c',p'),\epsilon)$ then $\interp{P_2}(c',p')=((c,p),\epsilon)$. Hence, one can replace $P_1$ or $P_2$ by the horizontal reflection of the other without changing the semantics. This implies that $P_1$ and $P_2$ contain the same number of PBS (otherwise, by replacing the one with more PBS by the horizontal reflection of the other, one would obtain a diagram equivalent to $C_{w,\sigma}^{\mathrm{opt}}$ with strictly fewer PBS, which would contradict its query-PBS-optimality), and subsequently, that the diagram $C_{w,\sigma}^{\mathrm{opt}\prime}$ obtained by replacing $P_2$ by the horizontal reflection $P_1^{-1}$ of $P_1$ is still query-PBS-optimal.

Up to slightly deforming $P_1$, we can write it in the form
\[\tikzfig{superpetpermsnpext}\]
where $\sigma_1$ and $\sigma_2$ are permutations of the wires, the $C_k$ are of the form \ptikzfig{escalierbsnoir-abrege}{0.375}{0.6}1\nolinebreak, and \ptikzfig{negpotentiel-m}{0.4}{0.8}1 denotes either \ptikzfig{filcourt}{0.4}{0.8}1 or \ptikzfig{neg}{0.4}{0.8}1. Using this, we can write $C_{w,\sigma}^{\mathrm{opt}\prime}$ in the form
\[\tikzfig{P1wP1invsuperpetpermsnpext}\]
where given any gate-free diagram $D$, $D^{-1}$ denotes its horizontal reflection.

Since the diagram is symmetric, we can remove the negations in the middle without changing the semantics of the diagram or its query-PBS-optimality. This gives us
\[C_{w,\sigma}^{\mathrm{opt}\prime\prime}\coloneqq\tikzfig{P1wP1invsuperpetpermsnpextext}.\]
Let us consider the diagram
\[C_{w,\sigma}^{\mathrm{opt,\not\neg}}\coloneqq\tikzfig{P1wP1invsuperpetperms}\]
obtained by removing all negations on the sides of $C_{w,\sigma}^{\mathrm{opt}\prime\prime}$. For each $p\in[n]$ such that there was a negation on the $p$th input and output wire, one now has %$(C_{w,\sigma}^{\mathrm{opt,\not\neg}},{\Vpol},p)\xRightarrow{w_{\sigma(p)}\ }({\Vpol},p)$ and $(C_{w,\sigma}^{\mathrm{opt,\not\neg}},{\Hpol},p)\xRightarrow{w_p\ }({\Hpol},p)$
$\interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}({\Vpol},p)=(({\Vpol},p),w_{\sigma(p)})$ and $\interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}({\Hpol},p)=(({\Hpol},p),w_p)$. Let us consider the directed graph $\tilde G$ obtained by reversing the edge $e_p$ in $\vec G$ for every such $p$. For every $p\in[n]$, we denote by $\tilde e_p$ the $p$th edge of $\tilde G$, which is either $e_p$ or its reverse $(w_{\sigma(p)},w_p)$. Then for every $p\in[n]$, $w^{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}_{{\Vpol},p}$ is the tail of $\tilde e_p$ and $w^{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}_{{\Hpol},p}$ is the head of $\tilde e_p$.

$\tilde G$ can be edge-partitioned into $r$ cycles as follows: For each $k\in\{1,...,r\}$, let $n_k$ be such that $C_k:\top^{\oplus n_k}\to\top^{\oplus n_k}$. Let also $N_k\coloneqq\sum_{j=1}^{k-1}n_k$. By abuse of notation, we denote by $\sigma_1$ and $\sigma_2$ the permutations of $[n]$ respectively associated with %\Acom{induced by ?}
the diagrams $\sigma_1$ and $\sigma_2$, so that $\forall c,p, %(\sigma_1,c,p)\Rightarrow(c,\sigma_1(p))\text{ and }(\sigma_2,c,p)\Rightarrow(c,\sigma_2(p))$
\interp{\sigma_1}(c,p)=((c,\sigma_1(p)),\epsilon)$ and $\interp{\sigma_2}(c,p)=((c,\sigma_2(p)),\epsilon)$.%\footnote{\Acom{introduire une notation pour avoir qqch du genre $\interp{\sigma_1}_0(c,p)=(c,\sigma_1(p))$ ? (peut-être pas à cet endroit-là)}\Acom{définir $\epsilon$}}
Note that for %every $k$
any $k\in\{1,...,r\}$ and any $p\in[n_k]$, one has %$\interp{C_k}({\Vpol},p)=(({\Vpol},p),\epsilon)$ and $\interp{C_k}({\Hpol},p)=(({\Hpol},p+1\bmod n_k),\epsilon)$. Therefore, for each $k\in\{1,...,r\}$,  one has $\binoppenalty10000\forall i\in[n_k], \interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}({\Vpol},\sigma_1^{-1}(N_k+i))=(({\Vpol},\sigma_1^{-1}(N_k+i)),w_{\sigma_2(N_k+i)})$,\qquad $\binoppenalty10000\forall i\in[n_k-1],\allowbreak \interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}({\Hpol},\sigma_1^{-1}(N_k+i))=(({\Hpol},\sigma_1^{-1}(N_k+i)),w_{\sigma_2(N_k+i+1)})$,\qquad and\qquad $\binoppenalty10000\interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}({\Hpol},\sigma_1^{-1}(N_k+n_k-1))=(({\Hpol},\sigma_1^{-1}(N_k+n_k-1)),w_{\sigma_2(N_k)})$.
\begin{itemize}
\item $\forall i\in[n_k], \interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}({\Vpol},\sigma_1^{-1}(N_k+i))=\\
\hphantom{\forall i\in[n_k], \interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}(\negphantom{(}}(({\Vpol},\sigma_1^{-1}(N_k+i)),w_{\sigma_2(N_k+i)})$
\item $\forall i\in[n_k-1], \interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}({\Hpol},\sigma_1^{-1}(N_k+i))=\\
\hphantom{\forall i\in[n_k-1], \interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}(\negphantom{(}}(({\Hpol},\sigma_1^{-1}(N_k+i)),w_{\sigma_2(N_k+i+1)})$
\item $\interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}({\Hpol},\sigma_1^{-1}(N_k+n_k-1))=\\
\hphantom{\interp{C_{w,\sigma}^{\mathrm{opt,\not\neg}}}(\negphantom{(}}(({\Hpol},\sigma_1^{-1}(N_k+n_k-1)),w_{\sigma_2(N_k)})$.
\end{itemize}
Hence, there is a cycle $w_{\sigma_2(N_k)}\to w_{\sigma_2(N_k+1)}\to\cdots\to w_{\sigma_2(N_k+n_k-1)}\to w_{\sigma_2(N_k)}$ in $\tilde G$, associated with $C_k$. Considering the cycle associated with each $C_k$ gives us an edge-partition of $\tilde G$ into $r$ cycles, since these cycles are edge-disjoint and cover all edges of $\tilde G$.

It remains to prove that there is no orientation of the edges of $G$ such that the resulting directed graph can be edge-partitioned into more than $r$ cycles. Assume that there is such a directed graph $\dbtilde G$ that admits an edge-partition into $r'$ cycles with $r'>r$. We enumerate these cycles in an arbitrary order, and denote by $m_k$ the length of the $k$th cycle, for $k\in\{1,...,r'\}$. We denote by $\dbtilde e_p$ the $p$th edge of $\dbtilde G$, which is either $\tilde e_p$ or its reverse. Note that the in- and out-degree of each vertex are the same in $\dbtilde G$ as in $\vec G$ and $\tilde G$, so that there exist two permutations $\tau_1$ and $\tau_2$ of $[n]$ such that $\forall p\in[n], \dbtilde e_p=(w_{\tau_1(p)},w_{\tau_2(p)})$. Therefore, there exists an enumeration of $[n]$ as $(i^k_\ell)_{k\in\{1,...,r'\},\ell\in[m_k]}$%, where $m_k$ is the length of the $k$th cycle
, such that %the cycles can be enumerated as $w_{i_1^1}\xrightarrow{e_{i_1^1}}w_{i_2^1}\xrightarrow{e_{i_2^1}}\cdots \xrightarrow{e_{i_{m_1-1}^1}}w_{i_{m_1}^1}\xrightarrow{e_{i_{m_1}^1}}w_{i_1^1}, ..., w_{i_1^r'}\xrightarrow{e_{i_1^{r'}}}w_{i_2^{r'}}\xrightarrow{e_{i_2^{r'}}}\cdots \xrightarrow{e_{i_{m_1-1}^{r'}}}w_{i_{m_1}^{r'}}\xrightarrow{e_{i_{m_1}^{r'}}}w_{i_1^{r'}}$.
the $k$th cycle can be written $w_{\tau_1(i_0^k)}\xrightarrow{\dbtilde e_{i_0^k}}w_{\tau_1(i_1^k)}\xrightarrow{\dbtilde e_{i_1^k}}\cdots \xrightarrow{\dbtilde e_{i_{m_k-2}^k}}w_{\tau_1(i_{m_k-1}^k)}\xrightarrow{\dbtilde e_{i_{m_k-1}^k}}w_{\tau_1(i_0^k)}$.

Let $s$ be the permutation of $[n]$ such that $\forall k,\ell,s(i^k_\ell)=M_k+\ell$, where $M_k\coloneqq\sum_{j=1}^{k-1}m_k$. We make the same abuse of notation as for $\sigma_1$ and $\sigma_2$ by also denoting by $s$ the diagram that is a permutation of the wires according to $s$. We consider the following diagram, where for each $k\in\{1,...,r'\}$, $C'_k:\top^{\oplus m_k}\to\top^{\oplus m_k}$ is of the form \ptikzfig{escalierbsnoir-abrege}{0.375}{0.6}1, and for each $p\in[n]$, \ptikzfig{negpotentiel-m}{0.4}{0.8}1 on wire $p$ is \ptikzfig{filcourt}{0.4}{0.8}1 if $\dbtilde e_p$ and $\tilde e_p$ have the same direction, or \ptikzfig{neg}{0.4}{0.8}1 otherwise:
\[C_{w,\tau}\coloneqq\tikzfig{diagGdbtildesuperpetpermsnpext}.\]
For any $k\in\{1,...,r'\}$ and $\ell\in[m_k]$, if $\dbtilde e_p$ and $\tilde e_p$ have the same direction then one has $\interp{C_{w,\tau}}({\Vpol},i^k_\ell)=(({\Vpol},i^k_\ell),w_{\tau_1(i^k_\ell)})$ and $\interp{C_{w,\tau}}({\Hpol},i^k_\ell)=(({\Hpol},i^k_\ell),w_{\tau_1(i^k_{\ell+1\bmod m_k})})$, and if they have opposite directions then one has $\interp{C_{w,\tau}}({\Vpol},i^k_\ell)=\linebreak[4](({\Vpol},i^k_\ell),w_{\tau_1(i^k_{\ell+1\bmod m_k})})$ and $\interp{C_{w,\tau}}({\Hpol},i^k_\ell)=(({\Hpol},i^k_\ell),w_{\tau_1(i^k_\ell)})$. That is, in any case, $w^{C_{w,\tau}}_{{\Vpol},i^k_\ell}$ is the tail of $\tilde e_{i^k_\ell}$ and $w^{C_{w,\tau}}_{{\Hpol},i^k_\ell}$ is its head. Since the indices $i^k_\ell$ span $[n]$ entirely, this implies that $C_{w,\tau}$ has the same semantics as $C_{w,\sigma}^{\mathrm{opt,\not\neg}}$. But $C_{w,\tau}$ contains $n-r'$ PBS whereas $C_{w,\sigma}^{\mathrm{opt,\not\neg}}$ contains $n-r$ PBS, so that $C_{w,\tau}$ contains strictly fewer PBS than $C_{w,\sigma}^{\mathrm{opt,\not\neg}}$, which contradicts the query-PBS-optimality of $C_{w,\sigma}^{\mathrm{opt,\not\neg}}$.

This proves that the edge-partition of $\tilde G$ into cycles obtained from $C_{w,\sigma}^{\mathrm{opt,\not\neg}}$ has maximum number of cycles among all possible choices of orientation and partition. In other words, the undirected edge-partition of $G$ obtained by erasing the directions of the edges in this edge-partition of $\tilde G$ has maximum number of cycles. This finishes the reduction.

%\Acom{On peut aussi formaliser plus explicitement la correspondance graphe/diagramme stairs-gates-stairs et mettre comme lemme le fait que le nombre d'escalier crrespond au nombre de cycles.}
%\Acom{à relire, revoir les notations ($\sigma_1,\sigma_2$ vs $\sigma$, $C_{w,\sigma}^{\mathrm{opt,\not\neg}}$, ...)}

%We will prove that the problem is already NP-hard when we restrict the input diagram to the following family of diagrams:
%%We denote by $\mathcal W$ the set of \CPBS-diagrams $D:\top^{\oplus n}\to\top^{\oplus n}$ such that for every $c\in\hv$ and $p\in[n]$, there exists a single letter $a_{c,p}$ such that $(D,c,p)\xRightarrow{a_{c,p}\ }(c,p)$.
%%\Acom{alternative :}
%Given a word $w=w_0...w_{n-1}$ with $w_0,...,w_{n-1}\in\GG$ and a permutation $\sigma$ of $[n]$, we define $\sigma(w)$ as the rearranged word $w_{\sigma(0)}...w_{\sigma(n-1)}$.
%We denote by $\mathcal P$ the set of \CPBS-diagrams $D:\top^{\oplus n}\to\top^{\oplus n}$ such that there exists a word $w=w_0...w_{n-1}\in\V^n$ %\in\V^*$ of length $n$
%and a permutation $\sigma$ of $[n]$ such that for every $p\in[n]$, $(D,\Vpol,p)\xRightarrow{w_p\ }(\Vpol,p)$ and $(D,\Hpol,p)\xRightarrow{w_{\sigma(p)}\ }(\Hpol,p)$.
%We polynomially reduce to this restricted problem\Aout{/We prove that this restricted problem is equivalent to}\Acom{Pour avoir equivalence il faut en plus les conditions correspondant au fait que le graphe n'est pas un multigraphe. Voire celles correspondant au fait qu'il est connexe.} the \emph{maximum Eulerian cycle decomposition problem}, also called MAX-ECD \cite{caprara1999eulerian}, which consists of, given an Eulerian undirected graph $G$, finding a maximum-cardinality edge-partition of $G$ into cycles (that is, partitioning the set of edges of $G$ into the maximum number of cycles). The NP-hardness of MAX-ECD follows directly from the NP-hardness of the %\emph{triangle partition problem}
%problem of finding an edge-partition of $G$ into triangles, which is proved in \cite{holyer1981edgepartition} (it corresponds to the case of the edge-partition into copies of the complete graph $K_3$).
%The MAX-ECD problem is equivalent to the problem of, given an Eulerian graph $G$,
%%Let $G$ be an Eulerian graph. Finding an edge-decomposition of $G$ into cycles is equivalent to
%finding a suitable orientation of its edges \Acom{(that is, a direction for each edge)} together with an edge-partition of the resulting directed graph into directed cycles, so that the number of cycles is maximal among all possible choices of orientation and partition. Indeed, given these, it suffices to erase the directions of the edges to get an undirected edge-partition into cycles, and given such a partition, it suffices to choose, for each cycle, one of the two possible ways of orienting it.
%Given an Eulerian graph $G$, we construct a \Acom{PBS-}diagram of $\mathcal P$ \Acom{ou $\mathcal W$} as follows: first, we choose an arbitrary orientation of the edges of $G$ such that each vertex has in- and out-degree equal, so as to get an Eulerian directed graph $\vec G$%, and we associate a label, which is an element of $\V$, to each vertex of $G$, in such a way that any two distinct vertices bear distinct labels
%. Without loss of generality, we can assume that the vertices of $G$ are elements of $\V$. We enumerate the edges of $\vec G$ as
%$e_0,...,e_{n-1}$% be any order of the edges of $\vec G$
%. %Since $\vec G$ is Eulerian\Acom{peut-être justifier un peu plus en détails},
%In $\vec G$, each vertex has in- and out-degree equal, that is, each vertex appears as many times as the head of an arrow as as the tail of an arrow, so that there exists a permutation $\sigma$ of $[n]$ such that for any $p\in[n]$, $e_p$ is of the form $(w_p,w_{\sigma(p)})$. We consider the following diagram:
%where $D_\sigma$ is a $\xntikzfig{neg}$-free\Acom{, gate-free} PBS-diagram \Acom{that is, a \CPBS-diagram generated by $\ntikzfig{diagrammevide-s}$, $\ntikzfig{filcourt-s}$, $\xstikzfig{swap}$, $\xgtikzfig{gateU}$ and \xstikzfig{beamsplitter}} in stair form\footnote{\Acom{Note that a diagram in stair form is a PBS-diagram if and only if all of its \Acom{stairs} are of the form \ptikzfig{escalierbsnoir-abrege}{0.375}{0.6}1.}}
%such that for any $p\in[n]$, $(D_\sigma,{\Vpol},p)\Rightarrow({\Vpol},p)$ and $(D_\sigma,{\Hpol},p)\Rightarrow({\Hpol},\sigma(p))$, and $D_\sigma^{-1}$ is the horizontal reflection of $D_\sigma$, which therefore satisfies that for any $p\in[n]$, $(D_\sigma^{-1},{\Vpol},p)\Rightarrow({\Vpol},p)$ and $(D_\sigma^{-1},{\Hpol},p)\Rightarrow({\Hpol},\sigma^{-1}(p))$.
%For any $p\in[n]$, one has $(C_{w,\sigma},{\Vpol},p)\xRightarrow{w_p\ }({\Vpol},p)$ and $(C_{w,\sigma},{\Hpol},p)\xRightarrow{w_{\sigma(p)}\ }({\Hpol},p)$. In particular, $C_{w,\sigma}$ is in $\mathcal P$\Acom{and in $\mathcal W$}, and for any $p\in[n]$, $w^{C_{w,\sigma}}_{{\Vpol},p}$ is the tail of $e_p$ and $w^{C_{w,\sigma}}_{{\Hpol},p}$ is the head of $e_p$.\footnote{\Acom{See \cref{defwordpathsem} for the definition of $w^{C_{w,\sigma}}_{c,p}$, as well as of $p^P_{c,p}$. Note that we identify words of length $1$ with their single letter.}}
%Let $C_{w,\sigma}^{\mathrm{opt}}$ be a query-PBS-optimal diagram equivalent to $C_{w,\sigma}$. Up to applying the PGT procedure, which can be done in polynomial time and neither changes the gates nor increases the number of PBS, one can assume that $C_{w,\sigma}^{\mathrm{opt}}$ is in PGT form. %Moreover, up to choosing the good order in which to put the gates in Step \ref{putinsnailform} of the procedure, one can assume that $C_{w,\sigma}^{\mathrm{opt}}$ is of the form
%That is, up to reordering some wires, it is of the form
%with $P$ in stair form. Since for every $c,p$, the word $w^{C_{w,\sigma}^{\mathrm{opt}}}_{c,p}$ has length $1$, $P$ is such that for any $c\in\hv$ and $p\in[n]$, one has %$(P,{\Vpol},p)\Rightarrow(c^p_{{\Vpol},p},p+n)$ and $(P,{\Vpol},p+n)\Rightarrow(c^p_{{\Vpol},p+n},p)$.
%$p^P_{c,p}\in\{n,...,2n-1\}$ and $p^P_{c,p+n}\in[n]$.
%By looking at the semantics of a generic diagram in stair form\Acom{mieux justifier, en s'appuyant sur la preuve du théorème \ref{stairsoptimal}}, it is easy to see that this implies that up to reordering the wires on the sides of $P$, we can write $C_{w,\sigma}^{\mathrm{opt}}$ in the form
%where $P_1$ and $P_2$ are two diagrams in stair form. Up to a few more deformation, %we can then write
%$C_{w,\sigma}^{\mathrm{opt}}$ is of the form
%For any $c,c'\in\hv$ and $p,p'\in[n]$, if $(P_1,c,p)\Rightarrow(c',p')$ then $(P_2,c',p')\Rightarrow(c,p)$. Hence, one can replace $P_1$ or $P_2$ by the horizontal reflection of the other without changing the semantics. This implies that $P_1$ and $P_2$ contain the same number of PBS (otherwise, by replacing the one with more PBS by the horizontal reflection of the other, one would obtain a diagram equivalent to $C_{w,\sigma}^{\mathrm{opt}}$ with strictly fewer PBS, which would contradict its query-PBS-optimality), and subsequently, that the diagram $C_{w,\sigma}^{\mathrm{opt}\prime}$ obtained by replacing $P_2$ by the horizontal reflection $P_1^{-1}$ of $P_1$ is still query-PBS-optimal.
%Up to slightly deforming $P_1$, we can write it in the form
%where $\sigma_1$ and $\sigma_2$ are permutations of the wires, the $C_k$ are of the form \ptikzfig{escalierbsnoir-abrege}{0.375}{0.6}1\nolinebreak, and \ptikzfig{negpotentiel-m}{0.4}{0.8}1 denotes either \ptikzfig{filcourt}{0.4}{0.8}1 or \ptikzfig{neg}{0.4}{0.8}1. Using this, we can write $C_{w,\sigma}^{\mathrm{opt}\prime}$ in the form
%where given any gate-free diagram $D$, $D^{-1}$ denotes its horizontal reflection.
%Since the diagram is symmetric, we can remove the negations in the middle without changing the semantics of the diagram or its query-PBS-optimality. This gives us
%Let us consider the diagram
%obtained by removing all negations on the sides of $C_{w,\sigma}^{\mathrm{opt}\prime\prime}$. For each $p\in[n]$ such that there was a negation on the $p$th input and output wire, one now has $(C_{w,\sigma}^{\mathrm{opt,NF}},{\Vpol},p)\xRightarrow{w_{\sigma(p)}\ }({\Vpol},p)$ and $(C_{w,\sigma}^{\mathrm{opt,NF}},{\Hpol},p)\xRightarrow{w_p\ }({\Hpol},p)$. Let us consider the directed graph $\tilde G$ obtained by reversing the edge $e_p$ in $\vec G$ for every such $p$. For every $p\in[n]$, we denote by $\tilde e_p$ the $p$th edge of $\tilde G$, which is either $e_p$ or its inverse $(w_{\sigma(p)},w_p)$. Then for every $p\in[n]$, $w^{C_{w,\sigma}^{\mathrm{opt,NF}}}_{{\Vpol},p}$ is the tail of $\tilde e_p$ and $w^{C_{w,\sigma}^{\mathrm{opt,NF}}}_{{\Hpol},p}$ is the head of $\tilde e_p$.
%$\tilde G$ can be edge-partitioned into $r$ cycles as follows: For each $k\in\{1,...,r\}$, let $n_k$ be such that $c_k:\top^{\oplus n_k}\to\top^{\oplus n_k}$. Let also $N_k\coloneqq\sum_{j=1}^{k-1}n_k$. By abuse of notation, we denote by $\sigma_1$ and $\sigma_2$ the permutations of $[n]$ respectively associated with %\Acom{induced by ?}
%the diagrams $\sigma_1$ and $\sigma_2$, so that $\forall c,p, (\sigma_1,c,p)\Rightarrow(c,\sigma_1(p))\text{ and }(\sigma_2,c,p)\Rightarrow(c,\sigma_2(p))$. Note that for %every $k$
%any $k\in\{1,...,r\}$ and any $p\in[n_k]$, one has $(C_k,{\Vpol},p)\Rightarrow({\Vpol},p)$ and $(C_k,{\Hpol},p)\Rightarrow({\Hpol},p+1\bmod n_k)$. Therefore, for each $k\in\{1,...,r\}$,  one has $\forall i\in[n_k], (C_{w,\sigma}^{\mathrm{opt,NF}},{\Vpol},\sigma_1^{-1}(N_k+i))\xRightarrow{w_{\sigma_2(N_k+i)}\ }({\Vpol},\sigma_1^{-1}(N_k+i))$,\quad $\forall i\in[n_k-1], (C_{w,\sigma}^{\mathrm{opt,NF}},{\Hpol},\sigma_1^{-1}(N_k+i))\xRightarrow{w_{\sigma_2(N_k+i+1)}\ }({\Hpol},\sigma_1^{-1}(N_k+i))$,\quad and\quad $(C_{w,\sigma}^{\mathrm{opt,NF}},{\Hpol},\sigma_1^{-1}(N_k+n_k-1))\xRightarrow{w_{\sigma_2(N_k)}\ }({\Hpol},\sigma_1^{-1}(N_k+n_k-1))$. Hence, there is a cycle $w_{\sigma_2(N_k)}\to w_{\sigma_2(N_k+1)}\to\cdots\to w_{\sigma_2(N_k+n_k-1)}\to w_{\sigma_2(N_k)}$ in $\tilde G$, associated with $C_k$. Considering the cycle associated with each $C_k$ gives us an edge-partition of $\tilde G$ into $r$ cycles, since these cycles are edge-disjoint and cover all edges of $\tilde G$.
%It remains to prove that there is no orientation of the edges of $G$ such that the resulting directed graph can be edge-partitioned into more than $r$ cycles. Assume that there is such a directed graph $\dbtilde G$ that admits an edge-partition into $r'$ cycles with $r'>r$. We enumerate these cycles in an arbitrary order, and denote by $m_k$ the length of the $k$th cycle, for $k\in\{1,...,r'\}$. We denote by $\dbtilde e_p$ the $p$th edge of $\dbtilde G$, which is either $\tilde e_p$ or its inverse\Acom{reverse ?}. Note that the in- and out-degree of each vertex are the same in $\dbtilde G$ as in $\vec G$ and $\tilde G$, so that there exist two permutations $\tau_1$ and $\tau_2$ of $[n]$ such that $\forall p\in[n], \dbtilde e_p=(w_{\tau_1(p)},w_{\tau_2(p)})$. Therefore, there exists an enumeration of $[n]$ as $(i^k_\ell)_{k\in\{1,...,r'\},\ell\in[m_k]}$%, where $m_k$ is the length of the $k$th cycle
%, such that %the cycles can be enumerated as $w_{i_1^1}\xrightarrow{e_{i_1^1}}w_{i_2^1}\xrightarrow{e_{i_2^1}}\cdots \xrightarrow{e_{i_{m_1-1}^1}}w_{i_{m_1}^1}\xrightarrow{e_{i_{m_1}^1}}w_{i_1^1}, ..., w_{i_1^r'}\xrightarrow{e_{i_1^{r'}}}w_{i_2^{r'}}\xrightarrow{e_{i_2^{r'}}}\cdots \xrightarrow{e_{i_{m_1-1}^{r'}}}w_{i_{m_1}^{r'}}\xrightarrow{e_{i_{m_1}^{r'}}}w_{i_1^{r'}}$.
%the $k$th cycle can be written $w_{i_0^k}\xrightarrow{\dbtilde e_{i_0^k}}w_{i_1^k}\xrightarrow{\dbtilde e_{i_1^k}}\cdots \xrightarrow{\dbtilde e_{i_{m_k-2}^k}}w_{i_{m_k-1}^k}\xrightarrow{\dbtilde e_{i_{m_k-1}^k}}w_{i_0^k}$.
%Let $s$ be the permutation of $[n]$ such that $\forall k,\ell,s(i^k_\ell)=M_k+\ell$, where $M_k\coloneqq\sum_{j=1}^{k-1}m_k$. We make the same abuse of notation as for $\sigma_1$ and $\sigma_2$ by also denoting by $s$ the diagram that is a permutation of the wires according to $s$. We consider the following diagram, where for each $k\in\{1,...,r'\}$, $C'_k:\top^{\oplus m_k}\to\top^{\oplus m_k}$ is of the form \ptikzfig{escalierbsnoir-abrege}{0.375}{0.6}1, and for each $p\in[n]$, \ptikzfig{negpotentiel-m}{0.4}{0.8}1 on wire $p$ is \ptikzfig{filcourt}{0.4}{0.8}1 if $\dbtilde e_p$ and $\tilde e_p$ have the same direction, or \ptikzfig{neg}{0.4}{0.8}1 otherwise:
%For any $k\in\{1,...,r'\}$ and $\ell\in[m_k]$, if $\dbtilde e_p$ and $\tilde e_p$ have the same direction then one has $(C_{w,\tau},{\Vpol},i^k_\ell)\xRightarrow{w_{i^k_\ell}\ }({\Vpol},i^k_\ell)$ and $(C_{w,\tau},{\Hpol},i^k_\ell)\xRightarrow{w_{i^k_{\ell+1\bmod m_k}}\ }({\Hpol},i^k_\ell)$, and if they have opposite directions then one has $(C_{w,\tau},{\Vpol},i^k_\ell)\xRightarrow{w_{i^k_{\ell+1\bmod m_k}}\ }({\Vpol},i^k_\ell)$ and $(C_{w,\tau},{\Hpol},i^k_\ell)\xRightarrow{w_{i^k_\ell}\ }({\Hpol},i^k_\ell)$. That is, in any case, $w^{C_{w,\tau}}_{{\Vpol},i^k_\ell}$ is the tail of $\tilde e_{i^k_\ell}$ and $w^{C_{w,\tau}}_{{\Hpol},i^k_\ell}$ is its head. Since the indices $i^k_\ell$ span $[n]$ entirely, this implies that $C_{w,\tau}$ has the same semantics as $C_{w,\sigma}^{\mathrm{opt,NF}}$. But $C_{w,\tau}$ contains $n-r'$ PBS whereas $C_{w,\sigma}^{\mathrm{opt,NF}}$ contains $n-r$ PBS, so that $C_{w,\tau}$ contains strictly fewer PBS than $C_{w,\sigma}^{\mathrm{opt,NF}}$, which contradicts the query-PBS-optimality of $C_{w,\sigma}^{\mathrm{opt,NF}}$.
%This proves that the edge-partition of $\tilde G$ into cycles obtained from $C_{w,\sigma}^{\mathrm{opt,NF}}$ has maximum number of cycles among all possible choices of orientation and partition. In other words, the undirected edge-partition of $G$ obtained by erasing the directions of the edges in this edge-partition of $\tilde G$ has maximum number of cycles. This finishes the reduction.
%\Acom{On peut aussi formaliser plus explicitement la correspondance graphe/diagramme stairs-gates-stairs et mettre comme lemme le fait que le nombre d'escalier crrespond au nombre de cycles.}
%\Acom{à relire, revoir les notations ($\sigma_1,\sigma_2$ vs $\sigma$, $C_{w,\sigma}^{\mathrm{opt,NF}}$, ...)}

\subsubsection{Proof of \cref{gatePBSnegfreeNPhard}}\label{preuvegatePBSnegfreeNPhard}

We reduce this problem from the problem maxDCD of, given an Eulerian directed graph $\vec G$, finding a maximum-cardinality edge-partition of $\vec G$ into directed cycles. This problem is defined and proved to be NP-hard in \cite{amir2010permutation}.

The proof has the same structure as the proof of \cref{gatePBSNPhard} : we define $C_{w,\sigma}$ in the same way, and we consider an equivalent diagram $C_{w,\sigma}^{\mathrm{opt}}$ which is now query-PBS-optimal only among negation-free diagrams. Since the PGT procedure preserves the property of being negation-free, we can still assume that it is in PGT form. With the same arguments as in the proof of \cref{gatePBSNPhard}, we can do the same deformations and define $C_{w,\sigma}^{\mathrm{opt}\prime}$ in the same way. This time, $C_{w,\sigma}^{\mathrm{opt}\prime}$ is negation-free, so that $C_{w,\sigma}^{\mathrm{opt,\not\neg}}=C_{w,\sigma}^{\mathrm{opt}\prime}$ and $\tilde G=\vec G$, so %that
the construction of the proof of \cref{gatePBSNPhard} gives us an edge-partition of $\vec G$. To prove that this edge-partition has maximum cardinality, we only have to prove that there is no edge-partition of $\vec G$ into strictly more cycles, and the proof of this is the same as for \cref{gatePBSNPhard}, except that we necessarily have $\dbtilde G=\vec G$ (which allows for many simplifications).

\subsubsection{Proof of \cref{gateplusPBSNPhard}}\label{preuvegateplusPBSNPhard}

The proof relies on the following lemma:
\begin{lemma}\label{negfreeisbetter}
Given any diagram $D$ of $\mathcal P$ with at least one negation, there exists an equivalent negation-free diagram with the same gates %that contains
containing at most $\nopbs(D)+\noneg(D)-1$ PBS.
\end{lemma}
Given this lemma, the proof of \cref{gateplusPBSNPhard} is exactly the same as that of \cref{gatePBSnegfreeNPhard}, the only difference being that $C_{w,\sigma}^{\mathrm{opt}}$ is defined as being a diagram equivalent to $C_{w,\sigma}$ such that $\nopbs(C_{w,\sigma}^{\mathrm{opt}})+\alpha \noneg(C_{w,\sigma}^{\mathrm{opt}})$ is optimal, which %, by \cref{negfreeisbetter},
implies that $C_{w,\sigma}^{\mathrm{opt}}$ is negation-free. Indeed, if it has at least one negation, then by \cref{negfreeisbetter}, there exists an equivalent negation-free diagram $D$ with at most $\nopbs(C_{w,\sigma}^{\mathrm{opt}})+\noneg(C_{w,\sigma}^{\mathrm{opt}})-1$ PBS. Then one has $\nopbs(D)+\alpha \noneg(D)=\nopbs(D)\leq \nopbs(C_{w,\sigma}^{\mathrm{opt}})+\noneg(C_{w,\sigma}^{\mathrm{opt}})-1$, whereas $\nopbs(C_{w,\sigma}^{\mathrm{opt}})+\alpha \noneg(C_{w,\sigma}^{\mathrm{opt}})\geq \nopbs(C_{w,\sigma}^{\mathrm{opt}})+\noneg(C_{w,\sigma}^{\mathrm{opt}})$, which contradicts the optimality of $C_{w,\sigma}^{\mathrm{opt}}$.

During all the proof, we only work with negation-free diagrams, therefore comparing the number of PBS is equivalent to comparing $\nopbs(\cdot)+\alpha \noneg(\cdot)$. In particular, $C_{w,\sigma}^{\mathrm{opt}}$ is indeed query-PBS-optimal among negation-free diagrams.
%\Acom{revoir la structure de l'explication. inverser les deux dernieres phrases ?}

It remains to prove \cref{negfreeisbetter}:
\begin{proof}[Proof of \cref{negfreeisbetter}]
Let $D:\top^{\oplus n}\to\top^{\oplus n}$ be a diagram of $\mathcal P$. Let us first apply Step \ref{putinsnailform} of the PGT procedure, that is, by mere deformation, we put $D$ in the form
\[\tikzfig{PGTw}\]
with $P$ gate-free. Let $f(P)$ be the number of positions $p$ such that $c^P_{\Vpol,p}=\Hpol$ (note that this number does not depend of the way of deforming $D$). Since the semantics of $P$ applies a permutation to the couples $(c,p)$, there are the same number of positions $p$ such that $c^P_{\Hpol,p}=\Vpol$, so that there are $2f(P)$ couples $(c,p)$ such that $c^D_{c,p}\neq c$. Each photon that enters $P$ with a basis state corresponding to one of these couples gets its polarisation changed while traversing $P$, which means that it traverses at least one negation. Since each negation can be reached from at most two basis states, this implies that $f(P)\leq \noneg(D)$.

Note that additionally, due to the semantics of $D$, for any $c,c'\in\hv$ and $p,p'\in[2n]$, if $\interp{P}(c,p)=(c',p')$ then $p\in[n]$ if and only if $p'\in\{n,...,2n-1\}$ and vice-versa, and $\interp{P}(c',p')=(c,p)$. Hence, the number of positions $p$ such that $c^P_{\Vpol,p}=\Hpol$ (resp. such that $c^P_{\Hpol,p}=\Vpol$) is the same in $[n]$ and $\{n,...,2n-1\}$, and $f(P)$ is even.

By applying the rest of the PGT procedure, we put $P$ in stair form and thereby transform $D$ into a diagram $D'$ in PGT form. With a similar argument as in the proof of \cref{gatePBSNPhard}, we can put $D'$ in the form
\[\tikzfig{P1wP2}%\Acom{remplacer $w$ par $U$ ?}
\]
where $P_1$ and $P_2$ are in stair form (note that unlike in the proof of \cref{gatePBSNPhard}, the wires and the gates are not necessarily black). Since $D\in\mathcal P$, for any $c,c'\in\hv$ and $p,p'\in[n]$, if $\interp{P_1}(c,p)=((c',p'),\epsilon)$ then $\interp{P_2}(c',p')=((c,p),\epsilon)$. Hence, $P_1$ has the same semantics as the horizontal reflection of $P_2$ and vice-versa. By \cref{stairsoptimal}, this implies that $P_1$ and $P_2$ contain the same number of PBS. Therefore, by replacing %this of $P_1$ or $P_2$ that contains more negations\Acom{contrôler la formulation} by the horizontal reflection of the other
$P_2$ by the horizontal reflection of $P_1$, we get a diagram $D''$ which is still equivalent to $D$ and still has at most as many PBS. As in the proof of \cref{gatePBSNPhard}, we can write $D''$ in the form
\[\tikzfig{P1wP1invsuperpetpermsnpext}\]
where $\sigma_1$ and $\sigma_2$ are permutation of the wires, the $C_k$ are %each of the form $\ptikzfig{escalierbsnoir-abrege}{0.375}{0.6}1,\quad\ptikzfig{escalierbsrouge-label-abrege}{0.375}{0.6}1,\quad\ptikzfig{escalierbsbleu-label-abrege}{0.375}{0.6}1,\quad\ptikzfig{escalierbsrougemerge-label-abrege}{0.375}{0.6}1\,\ \text{ or }\,\ \ptikzfig{escalierbsrougemergeinverse-label-abrege}{0.375}{0.6}1$
staircases (see \cref{defNMF}), and given any gate-free diagram $E$, $E^{-1}$ denotes its horizontal reflection. Since $D''$ is symmetric, we can remove the negations in the middle without changing its semantics, which gives us
\[D'''\coloneqq\tikzfig{P1wP1invsuperpetpermsnpextext}.\]
\[L\coloneqq\tikzfig{superpetpermsnpextgauche}.\]
Let $d(D)$ be the number of positions $p$ such that for some $p_1,p_2$ one has $p^L_{\Vpol,p_1}=p^L_{\Vpol,p_2}=p$ and $w_{p}=U$. Since $D\in\mathcal P$, each letter $U\in\{w_0,...,w_{n-1}\}$ appears as many times among the $w^D_{\Vpol,p}$ as among the $w^D_{\Hpol,p}$. Since $\forall c,p, w^D_{c,p}=w_{p^L_{c,p}}$, this implies that the number of positions $p'$ such that for some $p'_1,p'_2$ one has $p^L_{\Hpol,p'_1}=p^L_{\Hpol,p'_2}=p'$ and $w_{p'}=U$ is also $d(D)$. We arbitrarily associate a position $p'$ of the second kind with each position $p$ of the first kind, so as to distribute these $2d(D)$ positions into $d(D)$ couples $(p,p')$.
%%Since the map $(c,p)\mapsto(c^L_{c,p},p^L_{c,p})$ is a bijection, for each couple of positions $p_1,p_2$ such that
%Since $D\in\mathcal P$, each letter $U\in\{w_0,...,w_{n-1}\}$ appears as many times among the $w^D_{\Vpol,p}$ as among the $w^D_{\Hpol,p}$. Hence, for each letter $U\in\{w_0,...,w_{n-1}\}$, there are as many positions $p$ such that for some $p_1,p_2$ one has $p^L_{\Vpol,p_1}=p^L_{\Vpol,p_2}=p$ and $w_{p}=U$, as positions $p'$ such that for some $p'_1,p'_2$ one has $p^L_{\Hpol,p'_1}=p^L_{\Hpol,p'_2}=p'$ and $w_{p'}=U$ (because $\forall c,p, w^D_{c,p}=w_{p^L_{c,p}}$). We denote the number of such positions $p$ by $d(D)$. We associate with each of them one of the $d(D)$ positions $p'$, so as to partition these $2d(D)$ positions into $d(D)$ couples $(p,p')$.

For each position $q$ among these $2d(D)$ positions, there is exactly one polarisation $c$ such that $c^L_{c,p}\neq c$. This property is not affected by appending negations at the right of $L$, so that there is also exactly one polarisation $c$ (for each $q$) such that $c^{P_1}_{c,q}\neq c$. By definition of $P_1$, there is also exactly one polarisation $c$ such that $c^{P}_{c,q}\neq c$. %Consequently,
Since all of these $2d(D)$ positions $q$ are in $[n]$, this implies that $\dfrac{f(P)}{2}\geq d(D)$. Since $f(P)\leq \noneg(D)$, this inequality implies that $2d(D)\leq \noneg(D)$.
%Note that since for each such couple there is at least two basis states for which the semantics of $L$ changes the polarisation, one has $d(D)\leq \noneg(D)$.\Acom{détailler ?}

For each of the $d(D)$ couples $(p,p')$, we do the following transformation in $D'''$ (up to deformation):
\[\tikzfig{gateUsurgateU}\ \to\ \tikzfig{bsUhUbbs}.\]
Each time, we put $L$ in stair form again and we apply the symmetric transformation to $L^{-1}$, and %since $D'''$ remains symmetric, we can remove any negations at the right of $L$ and at the left of $L^{-1}$.
we remove any negations at the right of $L$ and at the left of $L^{-1}$, which is possible because $D'''$ %remains
is still symmetric.
Note that if the PBS appended to $L$ is connected to two different $C_i$s, then %they are merged
this results in merging them together, so that the number of PBS stays the same, and %if both input wires of the PBS are connected to a single $C_i$ then it is split into two parts
if it is connected to a single $C_i$ then this results in splitting it into two staircases, so that the number of PBS in $L$ decreases by $2$ (the behaviour of $L^{-1}$ is symmetric). At the end, the total number of PBS is at most $\nopbs(D)+2d(D)$, and the equality can be reached only if at every step two $C_i$s have been merged.
This gives us a diagram
\[D''''\coloneqq\tikzfig{LwLinvprimes}\]
with $L'$ of the form
\[\tikzfig{superpetpermsnpextgaucheprimes}\]
in which there are no couples of positions $p_1,p_2$ such that $p^L_{\Vpol,p_1}=p^L_{\Vpol,p_2}$ anymore%, which means that the maps $p\mapsto p^L$
. In particular, for each position $p$ such that for some $p_1$, $\interp{L'}(\Vpol,p_1)=((\Hpol,p),\epsilon)$, there exists $p_2$ such that $\interp{L'}(\Hpol,p_2)=((\Vpol,p),\epsilon)$. For each of these positions, we apply the following transformation:
\[\tikzfig{gateU}\ \to\ \tikzfig{negUneg}\]
This gives us a diagram
\[D^{(5)}\coloneqq\tikzfig{LwLinvsecondes}\]
%with $L''$ of the form
with $L''$ such that for all $c,p$, $c^{L''}_{c,p}=c$. By putting $L''$ in normal form, then in stair form again, we get a diagram $L'''$ without negations and with at most as many $PBS$ as $L''$. In particular, %it
the resulting diagram $D^{(6)}$ contains at most $\nopbs(D)+2d(D)$ PBS. If it has strictly fewer PBS, or if $2d(D)< \noneg(D)$, then we have the desired result. If it has exactly $\nopbs(D)+d(D)$ PBS and $2d(D)=\noneg(D)$, then this means in particular that at each of the steps of the transformation of $D'''$ into $D''''$, two $C_i$s have been merged. Since $d(D)\geq 1$, this implies that there is at least one couple of gates in $D^{(5)}$ with the same label and connected to the same staircase. Then by applying to them the same transformation:
\[\tikzfig{gateUsurgateU}\ \to\ \tikzfig{bsUhUbbs}\]
and putting $L'''$ (and ${L'''}^{-1}$) in stair form again, we get a diagram with $\nopbs(D)+\noneg(D)-2$ PBS and no negations, which is equivalent to $D$.
%with $L''$ such that for all $c,p$, $c^{L''}_{c,p}=c$. By putting $L''$ in normal form, then in stair form again, we get a diagram $L'''$ without negations and with at most as many $PBS$ as $L''$. In particular, %it
%the resulting diagram $D^{(6)}$ contains at most $\nopbs(D)+2d(D)$ PBS. %If it has strictly fewer PBS, or if $d(D)< \noneg(D)$,
%%if $d(D)<\dfrac{f(P)}{2}$, then since $f(P)\leq \noneg(D)$,
%If at least one step of the transformation of $D'''$ into $D''''$, a $C_i$ have been split, then i$D^{(6)}$ contains at most $\nopbs(D)+2d(D)-4$ PBS, so that since $2d(D)\leq f(P)\leq \noneg(D)$,
%we have the desired result. If %it has exactly $\nopbs(D)+d(D)$ PBS and
%%$d(D)=\dfrac{f(P)}{2}$, then this means that
%at %each of the
%all steps% of the transformation of $D'''$ into $D''''$
%, two $C_i$s have been merged. Since $d(D)\geq 1$, this implies that there is at least one couple of gates in $D^{(5)}$ with the same label and connected to the same staircase. Then by applying to them the same transformation: