Rewriting modulo symmetric monoidal structure
Filippo Bonchi
Fabio Gadducci
Aleks Kissinger
Pawel Sobocinski
Fabio Zanasi
String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs). They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and control theory. An important role in many such approaches is played by equational theories of diagrams, typically oriented and applied as rewrite rules. This paper lays a comprehensive foundation of this form of rewriting. We interpret diagrams combinatorially as typed hypergraphs and establish the precise correspondence between diagram rewriting modulo the laws of SMCs on the one hand and double pushout (DPO) rewriting of hypergraphs, subject to a soundness condition called convexity, on the other. This result rests on a more general characterisation theorem in which we show that typed hypergraph DPO rewriting amounts to diagram rewriting modulo the laws of SMCs with a chosen special Frobenius structure. We illustrate our approach with a proof of termination for the theory of non-commutative bimonoids.
macro.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                           %
%  Pawel Macros                                            %
%                                                           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\DeclareMathOperator{\Cmp}{Cmp}

%PIPPOFABIOPAWEL MACROS
\def \catC {\mathbb{C}}%{\mf{C}}

\newcommand{\tr}[1]{\xrightarrow{#1}}    % --1-->
\newcommand{\tl}[1]{\xleftarrow{#1}}    % <--1--

\newcommand{\Span}[1]{\mathsf{Span}(#1)}
\newcommand{\Cospan}[1]{\mathsf{Cospan}(#1)}
\def \PROP {\mathbf{PROP}} % category of PROPs
\def \PRO {\mathbf{PRO}} % category of PROs

\def \F {\mf{F}}
\newcommand{\mf}{\mathbf}

\def \frob {\mf{Frob}}

\newcommand{\rewiring}[1]{\ulcorner #1 \urcorner}


\newcommand{\PERM}{\mathbf{P}}

\newcommand{\DPOstep}[1]{\rightsquigarrow_{#1}}

\newcommand\symNet{\lower3pt\hbox{$\includegraphics[width=20pt]{graffles/symmetryalt.pdf}$}}
\newcommand\Idnet{\lower3pt\hbox{$\includegraphics[width=20pt]{graffles/id.pdf}$}}




%COMPACT CLOSED STRUCTURE
\newcommand \coc[1] {{#1}^{\star}}
\newcommand\lccB{\lower5pt\hbox{$\includegraphics[width=25pt]{graffles/rccr.pdf}$}}
\newcommand\rccB{\lower5pt\hbox{$\includegraphics[width=25pt]{graffles/lccl.pdf}$}}
%\newcommand\lccn{\lower5pt\hbox{$\includegraphics[width=25pt]{graffles/lccn.pdf}$}}
%\newcommand\rccn{\lower5pt\hbox{$\includegraphics[width=25pt]{graffles/rccn.pdf}$}}
\newcommand\lccn{\lower5pt\hbox{$\includegraphics[width=20pt]{graffles/cup.pdf}$}}
\newcommand\rccn{\lower5pt\hbox{$\includegraphics[width=20pt]{graffles/cap.pdf}$}}
\def \df {\ \ensuremath{:\!\!=}\ }





\DeclareMathOperator{\Cmp}{\mathbf{Cmp}}
%\DeclareMathOperator{\Psd}{Psd}
%\DeclareMathOperator{\Cospan}{Cospan}
\DeclareMathOperator{\Cospani}{Cospan^{\cong}}
\DeclareMathOperator{\ILC}{ILC}
\DeclareMathOperator{\OLC}{OLC}
\DeclareMathOperator{\LC}{LC}
\DeclareMathOperator{\Psd}{\mathbf{Psd}}
\DeclareMathOperator{\PsdCocone}{\mathbf{PsdCocone}}
\DeclareMathOperator{\Ann}{Ann}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\ke}{ker}
%\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Spl}{Spl}
\DeclareMathOperator{\op}{op}
\DeclareMathOperator{\Ob}{ob}
\DeclareMathOperator{\Arr}{arr}
\DeclareMathOperator{\Cel}{cel}
\DeclareMathOperator{\Sh}{Sh}
\DeclareMathOperator{\germ}{germ}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\Mat}{Mat}
\DeclareMathOperator{\tw}{\mathit{tw}}
\DeclareMathOperator{\Nil}{Nil}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\Fix}{Fix}
\DeclareMathOperator{\Deck}{Deck}
\DeclareMathOperator{\Conn}{Conn}
\DeclareMathOperator{\Th}{\mathsf{Th}}
\DeclareMathOperator{\TTh}{\mathsf{2-Th}}
\DeclareMathOperator{\Root}{rt}
\DeclareMathOperator{\Char}{ch}
\DeclareMathOperator{\ord}{ord}
\DeclareMathOperator{\Bicolim}{Bic}
\DeclareMathOperator{\RBC}{RBC}
\DeclareMathOperator{\LTS}{LTS}
\DeclareMathOperator{\GLTS}{ATS}
\DeclareMathOperator{\CTS}{CTS}
\DeclareMathOperator{\SEW}{Sew}
\DeclareMathOperator{\FLTS}{FLTS}
\DeclareMathOperator{\STS}{STS}

\renewcommand{\P}{\mathcal{P}}
\newcommand{\eg}{\textit{e.g.\ }}
\newcommand{\cf}{\textit{cf.\ }}
\newcommand{\fig}[1]{{\textit{Fig.~}{#1}}}

\newcommand{\leakOut}[1]{\uparrow\!#1}
\newcommand{\leakIn}[1]{\downarrow\!#1}
\newcommand{\typedState}[2]{{\scriptstyle \left<#1\,|\,#2\right>}}
\newcommand{\Defeq}% definitional equality
 {\stackrel{\mathrm{def}}{=}}

\newcommand{\ctx}{\mathcal{C}}
\newcommand{\evCtx}{\mathcal{E}}
\newcommand{\nEvCtx}{\mathcal{X}}
\newcommand{\strCong}{\equiv}
\newcommand{\nStrCong}{\nequiv}
\newcommand{\rel}[1]{\mathrel{\mathcal{#1}}}

\newcommand{\sLambdaBind}[2]{\boldsymbol{\lambda} #1.\,#2}
\newcommand{\lambdaBind}[2]{\lambda #1.\,#2}
\newcommand{\reduction}{\,\rightarrow\,}
\newcommand{\mReduction}{\,\rightarrow^*\,}
\newcommand{\xRightarrow}[1]{\stackrel{#1}{\Rightarrow}}
\newcommand{\weakLabelledTransition}[1]{{\,\xRightarrow{#1}\,}}
\newcommand{\labelledTransition}[1]{{\,\xrightarrow{#1}\,}}
\newcommand{\derivationRule}[3]{{\prooftree{\scriptstyle #1}\justifies{\scriptstyle #2}\using\ruleLabel{#3}\endprooftree}}
\newcommand{\reductionRule}[2]{{\prooftree{\scriptstyle #1}\justifies{\scriptstyle #2}\endprooftree}}

\newcommand{\barbson}[1]{\!\downarrow_{#1}}
\newcommand{\weakbarbson}[1]{\!\Downarrow_{#1}}

\newcommand{\fresh}{\mathit{fr}}

\newcommand{\ent}{\vdash}
\newcommand{\typ}{\mathrel{:}}
\newcommand{\judgement}[2]{#1\;\vdash\;#2}


\newcommand{\outputPrefix}[2]{{#1}!{#2}}
\newcommand{\inputPrefix}[2]{{#1}?{#2}}
\newcommand{\outputLabel}[1]{{#1}!}
\newcommand{\inputLabel}[1]{{#1}?}
\newcommand{\leakLabel}[1]{{\##1}}
\newcommand{\boundOutput}[2]{{#1}!{(#2)}}

\newcommand{\transitionSpace}{\phantom{P\xsta{a}Q}}

\newcommand{\Input}{\mathscr{I}}
\newcommand{\Output}{\mathscr{O}}
\newcommand{\Process}{\mathscr{P}}
\newcommand{\Name}{\mathscr{N}}

\newcommand{\calc}{$\epsilon$cs}
\newcommand{\stran}{\raise1pt\hbox{$\centerdot$}}
\newcommand{\SEWC}{\SEW^{c}}

\newcommand{\ruleLabel}[1]{\textsc{\scriptsize{(#1)}}}
\newcommand{\ruleName}[1]{\ruleLabel{#1}}

\newcommand{\rring}[1]{\ensuremath{\mathbb{#1}}}
\newcommand{\field}[1]{\ensuremath{\mathbf{#1}}}
\renewcommand{\b}[1]{\ensuremath{\mathbf{#1}}}
\newcommand{\Z}{\rring{Z}}

%\newcommand{\C}{\rring{C}}

\newcommand{\R}{\rring{R}}

\newcommand{\Q}{\rring{Q}}

\newcommand{\N}{\rring{N}}

\newcommand{\T}{\rring{T}}

\renewcommand{\k}{\field{k}}

\newcommand{\K}{\field{K}}

\newcommand{\CF}{\mathcal{C}}

\newcommand{\fg}[1]{\pi_{1}(#1)}

\newcommand{\setn}[2]{\{\,{#1}\,\mid\,{#2}\,\}}

\newcommand{\pres}[2]{<\,#1\ |\ #2\,>}

\newcommand{\s}[2]{\stackrel{#1}{#2}}

\newcommand{\cm}{\circ}

\newcommand{\ra}{\to}

\newcommand{\la}{\gets}

\newcommand{\rra}{\rightrightarrows}

\newcommand{\lra}{\longrightarrow}

\newcommand{\Ra}{\Rightarrow}

\newcommand{\lmt}{\longmapsto}

\newcommand{\ob}[1]{\overline{#1}}

\newcommand{\rad}{\text{r}}

\newcommand{\ten}{\otimes}

\newcommand{\dsum}{\oplus}

\newcommand{\ds}{\oplus}

\newcommand{\iso}{\cong}

\newcommand{\Alg}[1]{#1\text{-}\cat{Alg}}
\newcommand{\Mod}[1]{#1\text{-}\cat{Mod}}
\newcommand{\kAlg}{\Alg{k}}
\newcommand{\KAlg}{\Alg{K}}
\newcommand{\kMod}{\Mod{k}}
\newcommand{\KMod}{\Mod{K}}
\newcommand{\TAlg}{\Alg{T}}
\newcommand{\CRng}{\cat{CRng}}
\newcommand{\Grp}{\cat{Grp}}
\newcommand{\Ab}{\cat{Ab}}
\newcommand{\al}{\alpha}
\newcommand{\Set}{\cat{Set}\xspace}
\newcommand{\Cat}{\cat{Cat}\xspace}
\newcommand{\Par}{\cat{Par}\xspace}
\newcommand{\Prl}{\cat{Prl}\xspace}
\newcommand{\GCat}{G\textrm{-}\cat{Cat}\xspace}
%\newcommand{\Top}{\cat{Top}}
\newcommand{\Topp}{\cat{Top_*}}
\newcommand{\Graph}{\cat{Graph}\xspace}
\newcommand{\Bun}{\cat{Bun}\xspace}
\newcommand{\ABun}{\cat{ABun}\xspace}
\newcommand{\Ord}{\cat{Ord}\xspace}

\newcommand{\CC}{\cat{C}\xspace}

\newcommand{\DD}{\cat{D}\xspace}

\newcommand{\EE}{\cat{E}\xspace}

\newcommand{\XX}{\cat{X}\xspace}



\newcommand{\SubZ}{\text{Sub($Z$)}\xspace}
\newcommand{\Sub}[1]{\text{Sub(${#1}$)}}
\newcommand{\Desp}{\text{Des($p$)}\xspace}



\newcommand{\diag}{\Delta}

\newcommand{\codiag}{\triangledown}

\newcommand{\LH}{\cat{LH}}

\newcommand{\emb}{\hookrightarrow}

\newcommand{\scr}[1]{\mathscr{#1}}

\renewcommand{\O}{\boldsymbol{\mathcal{O}}}
\renewcommand{\emptyset}{\varnothing}

\renewcommand{\c}{\cdot}
\renewcommand{\t}{\times}

\renewcommand{\binom}[2]{\left(\begin{smallmatrix} #1 \\ #2 \end{smallmatrix}\right)}

\newcommand{\trinom}[3]{\left(\begin{smallmatrix} #1 \\ #2 \\  #3 \end{smallmatrix}\right)}



\newcommand{\ladj}[2]{\ar@/^/[#1]^-{#2} \ar@{}[#1]|-%

{\ifthenelse{\equal{#1}{r}}{\bot}{%

{\ifthenelse{\equal{#1}{rr}}{\bot}{%

{\ifthenelse{\equal{#1}{l}}{\top}{%

{\ifthenelse{\equal{#1}{u}}{\dashv}{%

{\vdash}}}}}}}}}}



\newcommand{\radj}[2]{\ar@/^/[#1]^-{#2}}

\newcommand{\radjff}[2]{\ar@{_{(}->}[#1]^{#2}}

\newcommand{\pullbacktop}[4]{%

{#1} \ar@/_/[ddr]_{#4} \ar@/^/[drr]^{#2}%

\ar@{.>}[dr]|-{#3} \\}

\newcommand{\pullbackbot}[8]{%

& {#1} \ar[r]^{#2} \ar[d]^{#3} & {#4} \ar[d]^{#5} \\%

& {#6}  \ar[r]_{#7}  & {#8}}


\newtheorem{clm}{Claim}[section]

\theoremstyle{plain}
\newtheorem{cor}[clm]{Corollary}
\newtheorem{pro}[clm]{Proposition}
\newtheorem{lem}[clm]{Lemma}
\newtheorem{thm}[clm]{Theorem}
\newtheorem{sch}[clm]{Scholium}

\theoremstyle{definition}
\newtheorem{defn}[clm]{Definition}
\newtheorem{exm}[clm]{Example}
\newtheorem{cexm}[clm]{Counterexample}
\newtheorem{alg}[clm]{Algorithm}
\newtheorem{rmk}[clm]{Remark}

\theoremstyle{remark}
\newtheorem{exr}[clm]{Exercise}

\newcommand{\fancy}[1]{\mathbf{#1}}

\newcommand{\cat}[1]{\ensuremath{\mathbf{#1}}}
\newcommand{\precat}[1]{\ensuremath{\,{\acute{}}\mathbf{#1}}}

\newcommand{\catlim}{\varprojlim}

\newcommand{\catcolim}{\varinjlim}

%\newcommand{\xra}[1]{\xrightarrow{#1}}

\newcommand{\xra}[1]{\stackrel{#1}{\longrightarrow}}

%\newcommand{\xla}[1]{\xleftarrow{#1}}

\newcommand{\xla}[1]{\stackrel{#1}{\longleftarrow}}

\newcommand{\wt}[1]{\widetilde{#1}}

\newcommand{\wh}[1]{\widehat{#1}}

\newcommand{\equ}{\simeq}



\newcommand{\bsigma}{{\boldsymbol{\sigma}}}

\newcommand{\btau}{{\boldsymbol{\tau}}}

\newcommand{\biota}{{\boldsymbol{\iota}}}

\newcommand{\tuple}[1]{\left\langle {#1} \right\rangle}

\newcommand{\hra}{\hookrightarrow}

\newcommand{\smallxy}{\def\objectstyle{\scriptstyle}\def\labelstyle{\scriptstyle}}

\newcommand{\sm}[1]{\hbox{\tiny{$#1$}}}

%\newcommand{\Xsta}[1]{\stackrel{#1}{%
% \rlap{\rule[2.8pt]{1.5em}{0.3pt}}%
% \rule[0.8pt]{1.5em}{0.3pt}%
%\mkern-6mu\blacktriangleright}}

\newcommand{\xsta}[1]{\hbox{$\,\stackrel{\,#1}{\rule[2.2pt]{1.0em}{0.6pt}}%
\mkern-2mu\blacktriangleright\,$}}
\newcommand{\lxsta}[1]{\hbox{$\,\stackrel{#1}{\rule[2.2pt]{1.5em}{0.6pt}}\mkern-2mu\blacktriangleright\,$}}
\newcommand{\longxsta}[1]{\hbox{$\,\stackrel{#1}{\rule[2.2pt]{2.5em}{0.6pt}}%
\mkern-2mu\blacktriangleright\,$}}
\newcommand{\superlongxsta}[1]{\hbox{$\,\stackrel{#1}{\rule[2.2pt]{3.5em}{0.6pt}}%
\mkern-2mu\blacktriangleright\,$}}
\newcommand{\superduperlongxsta}[1]{\hbox{$\,\stackrel{#1}{\rule[2.2pt]{4.5em}{0.6pt}}%
\mkern-2mu\blacktriangleright\,$}}

\newcommand{\nrta}{\hbox{$\,\mathrel{\rule[2.2pt]{1.5em}{0.6pt}}%
\mkern-2mu\not\vartriangleright\,$}}
\newcommand{\rta}{\hbox{$\,\mathrel{\rule[2.2pt]{1.5em}{0.6pt}}%
\mkern-2mu\vartriangleright\,$}}
\newcommand{\sta}{\hbox{$\,\mathrel{\rule[2.2pt]{1.5em}{0.6pt}}%
\mkern-2mu\blacktriangleright\,$}}

\newcommand{\hco}{\circ}
\newcommand{\vco}{\,{\scriptstyle\bullet}\,}

\newcommand{\mmid}{\mathrel{\boldsymbol\mid}}
\newcommand{\zero}{\mathtt{0}}

\newenvironment{funnyMathDisp}{\par\noindent\rule\textwidth{0.8pt}%
\vskip-9pt\noindent\rule\textwidth{0.4pt}\[}
{\]\rule\textwidth{0.4pt}\vskip-9pt%

\noindent\rule\textwidth{0.8pt}\vskip\belowdisplayskip\noindent}


\let\from\colon

\newcommand\red{\mathit{red}}

\newcommand\blue{\mathit{blue}}

\newcommand\tra{\lesssim_{\mathrm{tr}}}

\newcommand\fail{\lesssim_{\mathrm{f}}}

\newcommand{\PB}{{\sf Pb}\xspace}

\newcommand{\PO}{{\sf Po}\xspace}

\newcounter{ncomm}
\newcommand{\olds}[1]{\oldstylenums{#1}}
\newcommand{\oldsb}[1]{{\bfseries\olds{#1}}}
\newcommand{\comment}[1]{\stepcounter{ncomm}%
\vbox to0pt{\vss\llap{\tiny\oldsb{\arabic{ncomm}}}\vskip6pt}%
\marginpar{\tiny\bf\raggedright%
{\oldsb{\arabic{ncomm}}}.\hskip0.5em#1}}

\newcommand{\ltsred}[1]
{ \setbox0=\hbox{$\ {}^{#1}\ $}
  \setbox1=\hbox{$\longrightarrow$}
  \loop\setbox1=\hbox{$-$\kern-0.3em\unhbox1}\ifdim\wd1<\wd0\repeat
  \hbox{$\ \ \mathop{\box1}\limits^{#1}\ \ $}
}

\newcommand{\arx}[2]{\!\xymatrix@=15pt{\ar[r]^{{#1}}_{{#2}}&}\!}

\newcommand{\Rar}{\Rightarrow}

\newcommand{\react}[1]{\mathbb{#1}}

\newcommand{\ehole}{0}

\newcommand{\ass}{a}

\newlength{\mylength}

\newenvironment{Framed}%
{\setlength{\fboxsep}{15pt}
\setlength{\mylength}{\linewidth}%
\addtolength{\mylength}{-2\fboxsep}%
\addtolength{\mylength}{-2\fboxrule}%
\Sbox
\minipage{\mylength}%
\setlength{\abovedisplayskip}{0pt}%
\setlength{\belowdisplayskip}{0pt}%
}%
{\endminipage\endSbox
\[\fbox{\TheSbox}\]}

\newcommand{\bnfSep}{\ |\ }
\newcommand{\bnfEq}{\ ::=\ }


\newcommand{\syntax}[1]{\mathbf{S}_{#1}}
\newcommand{\syntaxgr}[1]{\widehat{\mathbf{S}}_{#1}}
\newcommand{\FTerm}[1]{\mathbf{FTerm}_{#1}}
\newcommand{\Hyp}[1]{\mathbf{Hyp}_{#1}}


% ALEKS' MACROS

% \theoremstyle{definition}
% \newtheorem{theorem}{Theorem}
% \newtheorem*{theorem*}{Theorem}
% \newtheorem{corollary}[theorem]{Corollary}
% \newtheorem{lemma}[theorem]{Lemma}
% \newtheorem{proposition}[theorem]{Proposition}
% \newtheorem{conjecture}[theorem]{Conjecture}
% \newtheorem{definition}[theorem]{Definition}
% \newtheorem{fact}[theorem]{Fact}
% \newtheorem{example}[theorem]{Example}
% \newtheorem{examples}[theorem]{Examples}
% \newtheorem{example*}[theorem]{Example*}
% \newtheorem{examples*}[theorem]{Examples*}
% \newtheorem{remark}[theorem]{Remark}
% \newtheorem{remark*}[theorem]{Remark*}
% \newtheorem{question}[theorem]{Question}
% \newtheorem{assumption}[theorem]{Assumption}
% \newtheorem{convention}[theorem]{Convention}
% \newtheorem{justification}[theorem]{Justification}

% congruences and reductions for hopf algebras
\newcommand{\HC}[1]{\ensuremath{\textbf{HC}_{#1}}\xspace}
\newcommand{\HR}[1]{\ensuremath{\textbf{HR}_{#1}}\xspace}
\newcommand{\BA}[1]{\ensuremath{\textbf{NB}_{#1}}\xspace}

\newcommand{\precU} {\ensuremath{\preceq_{U}}\xspace}
\newcommand{\precM} {\ensuremath{\preceq_{M}}\xspace}
\newcommand{\precL} {\ensuremath{\preceq_{L}}\xspace}
\newcommand{\precmu}{\ensuremath{\preceq_{\mu}}\xspace}
\newcommand{\precnu}{\ensuremath{\preceq_{\nu}}\xspace}

\usepackage{color}
\def\bR{\begin{color}{red}}
\def\bB{\begin{color}{blue}}
\def\bM{\begin{color}{magenta}}
\def\bC{\begin{color}{cyan}}
\def\bW{\begin{color}{white}}
\def\bBl{\begin{color}{black}}
\def\bG{\begin{color}{green}}
\def\bY{\begin{color}{yellow}}
\def\e{\end{color}\xspace}


\newcommand{\cgr}[2][scale=0.45]{\raisebox{0.1em}{\begingroup
\setbox0=\hbox{\includegraphics[#1]{graffles/#2}}%
\parbox{\wd0}{\box0}\endgroup}}

\newcommand{\sink}[1]{\textrm{sink}(#1)}

%%%%%%%%%%%%
%%%%%%%%%%%%
%%%%%%%%%%%%
% FABIO Z. MACROS
%%%%%%%%%%%%
%%%%%%%%%%%%
%%%%%%%%%%%%
%%%%%%%%%%%%

\def \poi {\,\ensuremath{;}\,}
\def \df {\ensuremath{:=}}
\def \tns {\ensuremath{\oplus}}
\def \: {\colon}

\newcommand{\dws}[1]{{#1\!\downarrow}}
\newcommand{\ups}[1]{{#1\!\uparrow}}

\newcommand{\fznote}[1]{\marginpar{{\bf F.Z.} #1 }}    % Commento a lato, Fabio
\newcommand{\aknote}[1]{\marginpar{{\bf A.K.} #1 }}
\newcommand{\psnote}[1]{\marginpar{{\bf P.S.} #1 }}
\newcommand{\fgnote}[1]{\marginpar{{\bf F.G.} #1 }}
\newcommand{\fbnote}[1]{\marginpar{{\bf F.B.} #1 }}


\newcommand{\X}{\mathbf{X}}
\newcommand{\Y}{\mathbf{Y}}


\newcommand\Bmult{\lower4pt\hbox{$\includegraphics[width=17pt]{graffles/Bmult.pdf}$}}
\newcommand\Bcomult{\lower4pt\hbox{$\includegraphics[width=17pt]{graffles/Bcomult.pdf}$}}
\newcommand\Bunit{\lower4pt\hbox{$\includegraphics[width=14pt]{graffles/Bunit.pdf}$}}
\newcommand\Bcounit{\lower4pt\hbox{$\includegraphics[width=14pt]{graffles/Bcounit.pdf}$}}
%\newcommand\Wcomult{\lower5pt\hbox{$\includegraphics[width=20pt]{graffles/Wcomult.pdf}$}}

\newcommand\Wmult{\lower4pt\hbox{$\includegraphics[width=17pt]{graffles/Wmult.pdf}$}}
\newcommand\Wcomult{\lower4pt\hbox{$\includegraphics[width=17pt]{graffles/Wcomult.pdf}$}}
\newcommand\Wunit{\lower4pt\hbox{$\includegraphics[width=14pt]{graffles/Wunit.pdf}$}}
\newcommand\Wcounit{\lower4pt\hbox{$\includegraphics[width=14pt]{graffles/Wcounit.pdf}$}}

\newcommand{\SynToCsp}[1]{\ensuremath{\lfloor\!\lfloor{#1}\rfloor\!\rfloor}}    % Commento a lato, Fabio

\newcommand{\FTermSG}[1]{\mathbf{FTerm}_{\scriptscriptstyle \Sigma / #1}}
\newcommand{\HypSG}[1]{\mathbf{Hyp}_{\scriptscriptstyle \Sigma / #1}}
\newcommand{\Paths}[1]{\mathbf{HPath}_{\scriptscriptstyle #1}}
\newcommand{\ForgetSlice}{\mathcal{F}}
%\newcommand{\tr}[1]{\xrightarrow{#1}}    % --1-->
%\newcommand{\tl}[1]{\xleftarrow{#1}}    % <--1--

\newcommand{\rrule}[2]{\ensuremath{\langle #1,#2 \rangle}}

\def \frob {\mf{Frob}}
%\newcommand{\inp}[2][]{\mathsf{in}_{#1}^{#2}}
%\newcommand{\out}[2][]{\mathsf{out}_{#1}^{#2}}
\newcommand{\out}[1]{\mathsf{out}(#1)}
\newcommand{\inp}[1]{\mathsf{in}(#1)}
\newcommand{\lout}[1]{\mathsf{lout}(#1)}
\newcommand{\linp}[1]{\mathsf{lin}(#1)}
\newcommand{\rout}[1]{\mathsf{rout}(#1)}
\newcommand{\rinp}[1]{\mathsf{rin}(#1)}
\newcommand{\node}{\lower0pt\hbox{$\includegraphics[width=6pt]{graffles/node.pdf}$}}
\newcommand{\hyperedge}{\lower2pt\hbox{$\includegraphics[width=25pt]{graffles/hyperedge.pdf}$}}
\newcommand{\ZeronetT}{\lower4pt\hbox{$\includegraphics[width=14pt]{graffles/idzerocircuit.pdf}$}}
\def \Mon {\mathbf{M}}

\newcommand\idncircuit{\lower4pt\hbox{$\includegraphics[width=18pt]{graffles/idncircuit.pdf}$}}
\newcommand{\rigidDPOstep}[1]{\Rrightarrow_{#1}}
\def \dfop {\ \ensuremath{=:}\ }
\def \NCB {\mathbf{NB} }

rewriting.tex
%\documentclass[12pt]{article}
%\documentclass[preprint,nonatbib]{sigplanconf} nonatbib option makes \usepackage{cite} work!
%\documentclass[preprint]{sigplanconf}
\documentclass{article}

\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{enumitem}
\usepackage{xspace}
\usepackage{amsfonts}
\usepackage{mathrsfs}
\usepackage{multicol}
\usepackage{prooftree}
\usepackage[all,2cell]{xy}
%\usepackage{a4wide}
\CompileMatrices
\UseAllTwocells
\SilentMatrices
%\usepackage{gastex}
%\usepackage{psfrag}
\usepackage{graphicx}
%\usepackage{cite}
\usepackage{float}
\usepackage{fancybox}
\usepackage{hyperref}
\usepackage{enumitem}


\input{macro.tex}

\usepackage{comment}

%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% FABIO Z: Hack to fit five authors in a row
%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%
% \makeatletter
% \def \@vtitleauthors#1#2#3#4#5{%
%   \if \@andp{\@emptyargp{#2}}{\@emptyargp{#3}}%
%     \noindent \@setauthor{40pc}{#1}{\@false}\par
%   \else\if \@emptyargp{#3}%
%     \noindent \@setauthor{17pc}{#1}{\@false}\hspace{3pc}%
%               \@setauthor{17pc}{#2}{\@false}\par
%   \else\if \@emptyargp{#4}%
%     \noindent \@setauthor{17pc}{#1}{\@false}\hspace{3pc}%
%               \@setauthor{17pc}{#3}{\@false}\par
%   \else
%     \noindent \@setauthor{7.3333pc}{#1}{\@false}\hspace{1pc}%
%               \@setauthor{7.3333pc}{#2}{\@false}\hspace{1pc}%
%               \@setauthor{7.3333pc}{#3}{\@false}\hspace{1pc}%
%               \@setauthor{7.3333pc}{#4}{\@false}\hspace{1pc}%
%               \@setauthor{7.3333pc}{#5}{\@true}\par
%     \relax
%   \fi\fi\fi
%   \vspace{20pt}}
% \def \@maketitle {%
%   \begin{center}
%   \@settitlebanner
%   \let \thanks = \titlenote
%   {\leftskip = 0pt plus 0.25\linewidth
%    \rightskip = 0pt plus 0.25 \linewidth
%    \parfillskip = 0pt
%    \spaceskip = .7em
%    \noindent \LARGE \bfseries \@titletext \par}
%   \vskip 6pt
%   \noindent \Large \@subtitletext \par
%   \vskip 12pt
%   \ifcase \@authorcount
%     \@latex@error{No authors were specified for this paper}{}\or
%     \@titleauthors{i}{}{}\or
%     \@titleauthors{i}{ii}{}\or
%     \@titleauthors{i}{ii}{iii}\or
%     \@titleauthors{i}{ii}{iii}{iv}\or
%     \@vtitleauthors{i}{ii}{iii}{iv}{v}\or
%     \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}\or
%     \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}%
%                   \@titleauthors{vii}{}{}\or
%     \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}%
%                   \@titleauthors{vii}{viii}{}\or
%     \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}%
%                   \@titleauthors{vii}{viii}{ix}\or
%     \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}%
%                   \@titleauthors{vii}{viii}{ix}\@titleauthors{x}{}{}\or
%     \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}%
%                   \@titleauthors{vii}{viii}{ix}\@titleauthors{x}{xi}{}\or
%     \@titleauthors{i}{ii}{iii}\@titleauthors{iv}{v}{vi}%
%                   \@titleauthors{vii}{viii}{ix}\@titleauthors{x}{xi}{xii}%
%   \else
%     \@latex@error{Cannot handle more than 12 authors}{}%
%   \fi
%   \vspace{1.75pc}
%   \end{center}}
% \makeatother
%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% FABIO Z : end of the hack
%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Rewriting modulo symmetric monoidal structure}
\author{Filippo Bonchi, Fabio Gadducci, Aleks Kissinger \\
Pawel Sobocinski, Fabio Zanasi}

\begin{document}

\special{papersize=8.5in,11in}
\setlength{\pdfpageheight}{\paperheight}
\setlength{\pdfpagewidth}{\paperwidth}

% \conferenceinfo{LICS 2016}{July 5–8, 2016, New York City, USA}
% \copyrightyear{2016}
% \copyrightdata{}
% \doi{}

% OPTION 1
% \authorinfo{Filippo Bonchi}{CNRS, ENS Lyon}{filippo.bonchi@gmail.com}
% \authorinfo{Fabio Gadducci}{U. Pisa}{gadducci@di.unipi.it}
% \authorinfo{Aleks Kissinger}{Radboud U. Nijmegen}{aleks@cs.ru.nl}
% \authorinfo{Pawe{\l} Soboci{\'n}ski}{U. Southampton}{ps@ecs.soton.ac.uk}
% \authorinfo{Fabio Zanasi}{Radboud U. Nijmegen}{fzanasi@cs.ru.nl}

\maketitle

\begin{abstract}
String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs). They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and control theory.

An important role in many such approaches is played by equational theories of diagrams, typically oriented and applied as rewrite rules. This paper lays a comprehensive foundation of this form of rewriting. We interpret diagrams combinatorially as typed hypergraphs and establish the precise correspondence between diagram rewriting modulo the laws of SMCs on the one hand and double pushout (DPO) rewriting of hypergraphs, subject to a soundness condition called convexity, on the other. This result rests on a more general characterisation theorem in which we show that typed hypergraph DPO rewriting amounts to diagram rewriting modulo the laws of SMCs with a chosen special Frobenius structure.

We illustrate our approach with a proof of termination for the theory of non-commutative bimonoids.
\end{abstract}

\section{Introduction}
\input{source/intro.tex}

\section{Background}\label{sec:Background}
\input{source/Background.tex}


%\section{Hypergraphs and symmetric monoidal theories with Frobenius structure}
\section{Frobenius termgraphs}\label{sec:HypInterpretation}
\input{source/hypergraphs_and_smts.tex}


\section{DPO rewriting on Frobenius termgraphs}\label{sec:dpoRewriting}
\input{source/dpoRewriting.tex}


\section{The general symmetric monoidal case}\label{sec:SymMonDpoRewriting}

\input{source/SymMonDpoRewriting.tex}


\section{Case study: non-commutative bialgebras}\label{sec:terminationHopf}


\input{source/terminationHopf.tex}


%\section{Confluence for non-commutative bialgebras}\label{sec:terminationHopf}
%\input{source/confBialg.tex}



\section{Conclusions and future work}

Our approach centered on building a bridge between
algebraic and combinatorial descriptions of string diagrams, in the form of the isomorphism $\syntax{\Sigma}+\frob \cong \FTerm\Sigma$. We used it to spell out two fundamental ways in which rewriting in symmetric monoidal categories and DPO hypergraph rewriting are compatible.

%We exhibited an isomorphism between $\FTerm\Sigma$ and $\syntax{\Sigma}+\frob$, which serves as a bridge between algebraic and combinatorial descriptions of string diagrams, and used it to spell out two ways in which rewriting in symmetric monoidal categories and DPO hypergraph rewriting are compatible.

The first is that we can use DPO to rewrite SMCs generated by theories containing a special Frobenius structure. Theories of that kind are appearing in different research threads: they play a role in the compositional study of Petri nets ~\cite{Bruni2011,Sobocinski2014,Rathke2014a}, in the algebra of concurrent connectors~\cite{Bruni2006}, in signal flow diagrams~\cite{Bonchi2014b,Bonchi2015,BaezErbele-CategoriesInControl,Fong2015} and in the ZX-calculus~\cite{Coecke2008, Coecke2012}, just to mention a few examples. Our approach enables the use of the technology that has been developed for DPO in the last decades in those diverse areas.

The second approach -- convex DPO rewriting -- allows to rewrite in categories presented by arbitrary symmetric monoidal theories. Our results lay the theoretical foundations for the development of comprehensive tool support for reasoning about rewriting in SMCs. Emerging tools such as Globular~\cite{Globular} do not factor in the symmetric structure, whereas Quantomatic~\cite{Kissinger_quantomatic} relies on additional structure, requiring for example that the ambient category be traced. Our theory overcomes these limitations and can be effectively implemented: matching is efficient with respect to the size of the target hypergraph and the two conditions in the definition of a convex rewriting step -- convexity and boundary complement -- can be be automatically checked. Furthermore, under the encoding of hypergraphs as string graphs (the underlying theory used by Quantomatic), it is now possible to extend Quantomatic to support rewriting in a generic SMC. We leave the algorithmic details as future work.

Just as in term rewriting, commutative operators pose a interesting problem: naively encoding commutativity in a rule immediately yields a non-terminating system. We leave this issue as future work, but preliminary results suggest that the commutativity of some operators can be effectively encoded in the graphical structure.

From a theoretical point of view, we intend to build on this work to investigate the relationship between distributive laws of PROPs~\cite{Lack2004a} and rewriting. Compatibility conditions expressed by a distributive law come with an orientation, making natural to think of them as rewriting rules. Just as in our approach, these conditions are defined modulo the laws of SMCs: it thus appears promising to explore the correspondence between the two perspectives.

%As shown in Section \ref{sec:terminationHopf}, the fact that the laws of SMCs are implicit in the graphical representation pays off in that we obtain quite simple rewriting systems for fairly sophisticated theories: indeed the subsumption of permutations by the combinatorial structure often means many far fewer and simpler rules. \marginpar{Say here that this example is really important for quantum}

%\marginpar{Pawel: This last bit is a bit of a downer to end the paper on, maybe something a bit more upbeat and inspiring?}
%Just as in term rewriting, commutative operators pose a interesting problem: if we naively encode commutativity in a rule, we immediately ends up in a non-terminating system. We leave this issue as future work, but preliminary results suggest that the commutativity of some operators can be effectively encoded in the graphical structure.


%
%
%
%[Maybe that's a good spot for wishful thinking about algorithms..]
%One of the big advantages of using the combinatorial structure is that finding a match becomes pretty easy. It's simple to knock up an algorithm. For example: suppose we want to find a match of $l$ in $c$. We choose an edge of $t_l$ and scan the edges of $t_c$ looking for that edge. On finding it we try to extend the match and check whether it's legal. This simple algorithm one thinks of has time complexity $O(edges(l) \times edges(c))$, which is not bad in practice since $l$ will tend to be small. And I'm sure that there are standard optimisations to take this down further...
%
%Once a match is found, it is trivial to do the actual rewrite on the combinatorial structure. And it is not difficult to write down a recursive (on the set of edges) algorithm that takes a termgraph and spits out a term.
%
%\bigskip
%
%Other wishful thinking about algorithms:
%\begin{itemize}
%\item In general terms, the graphs in the image of $\phi$ are ordered. Intuitively they can be represented as list of pointers. Can this order be exploited to get more efficient algorithms? Let us call it \emph{ordered rewriting}. Is the algorithm for ordered rewriting more efficient than those for standard graph rewriting?
%\item Can we find a terminating rewriting system for Frobenius?
%\item If the answer to the two previous points is YES, then we might hope to get a novel efficient algorithm for standard graph rewriting. The idea is to translate any graph rewriting rules into a PROP rule (using the additional Fobrenius structure). Then add to the rewrite systems the rules for Frobenius and then use the algorithm for ordered rewriting.
%\end{itemize}
%


%\bibliographystyle{abbrvnat}
%\bibliographystyle{abbrv}
\bibliographystyle{akbib}
\bibliography{catBib3}
\newpage


\appendix
\section{Omitted proofs}\label{app:proofs}

\input{source/app_omittedproofs.tex}



\end{document}






app_omittedproofs.tex
\paragraph{Preliminaries on hypergraphs} The following terminology will be used throughout the proofs of this appendix. Given an hypergraph $G$, we write $N_G$ for its set of nodes and $E_G$ for the set of hyperedges. Given an hyperedge $h$ with $k$ (ordered) sources and $l$ (ordered) targets, we write $s_j(h)$ for the $j$-th source node of $h$ and $t_j(h)$ for the $j$-th target node of $h$.

For a pair of hyperedges $h,h'$ such that for some $i,j$ and node $v$, $t_i(h) = v = s_j(h)$, then $h$ is called a \textit{predecessor} of $h'$ and $h'$ a \textit{successor} of $h$.

    For a hypergraph $G$ and hyperedges $h,h'$, a \textit{directed path} $p$ from $h$ to $h'$ is a sequence of hyperedges $[h_1, \ldots, h_n]$ such that $h_1 = h$, $h_n = h'$, and for $i < n$, $h_{i+1}$ is a successor of $h_i$. We say $p$ starts at a subgraph $H$ if $H$ contains a node in the source of $h$, and terminates at a subgraph $H'$ if $H'$ contains a node in the target of $h'$. We say $p$ starts at a subgraph $H$ if there exists some $i$ such that $s_i(h) \in H$, and terminates at a subgraph $H'$ if there exists some $j$ where $t_j(h') \in H'$.

Note that, by regarding nodes as single-node subgraphs, it clearly makes sense to talk about directed paths from/to nodes as well.


\begin{proof}[Proof of Lemma~\ref{lemma:convexfact}]
    Let $C_1$ be the smallest sub-hypergraph containing the inputs of $G$ and every hyperedge $h$ which is not in $L$, but has a path to it. Let $C_2$ then be the smallest sub-hypergraph containing the outputs of $G$ such that $C_1 \cup L \cup C_2 = G$. By construction, $C_1$ and $L$ share no hyperedges. If $C_2$ shared a hyperedge with $C_1$ or $L$, then there would exist a smaller $C_2'$ such that $C_1 \cup L \cup C_2' = G$, so $C_2$ shares no hyperedges with either $C_1$ or $L$. Hence, the three sub-hypergraphs only overlap on nodes. Now let:
    \begin{align*}
        i & := N_{C_1} \cap N_L \\
        j & := N_{C_2} \cap N_L \\
        k & := (N_{C_1} \cap N_{C_2}) \backslash N_L
    \end{align*}
    Since $p$ is disjoint from $m'$ and $n'$, it follows that:
    \[
        k + i = N_{C_1} \cap (N_L \cup N_{C_2})
        \qquad
        k + j = N_{C_2} \cap (N_L \cup N_{C_1})
    \]
    Now, define the following cospans, where arrows are all inclusions:
    \[ n \rightarrow C_1 \leftarrow k + i \]
    \[ i \rightarrow L \leftarrow j \]
    \[ k + j \rightarrow C_2 \leftarrow m \]
    Then \eqref{eq:snd-factor} is computed as the colimit of the following diagram:
    \[ n \rightarrow C_1 \leftarrow k + i
         \rightarrow k + L \leftarrow k + j
         \rightarrow C_2 \leftarrow m \]
    The two spans identify precisely those nodes from $G$ which occur in more than one sub-hypergraph, so this amounts to simply taking the union:
    \[ n \rightarrow C_1 \cup L \cup C_2 \leftarrow m \ =\ n \rightarrow G \leftarrow m \]

    $C_1, C_2$, and $L$ are all directed acyclic because $G$ is, so it only remains to show each of these cospans is monogamous. $C_1$ and $C_2$ follow straightforwardly from the observation that $C_1$ is closed under predecessors and $C_2$ under successors.

    %If $h$ has a path to $L$ and $h'$ is a predecessor of $h$, then $h'$ also has a path to $L$. Hence $C_1$ is closed under taking predecessors. Thus, a node $v$ in $C_1$ has no in-hyperedge if and only of it is in $m$. If $v$ has no out-hyperedge in $C_1$, then it is either an output, in which case it is in $C_3$, or it has an out-hyperedge in $C_2$ or $L$. Hence it has no out-hyperedge if and only if it is in $p + m'$. $C_2$ is closed under taking successors, so the monogamy of its cospan follows similarly.

    The interesting case is $L$, which relies on convexity. Suppose $v$ does not have a in-hyperedge in $L$. Then either $v$ is an input or there exists a hyperedge with a path to $v$. One of these two is true precisely when $v \in i$. Suppose $v$ does not have an out-hyperedge in $L$. Then, either $v$ is an ouput or it has an out-hyperedge in $C_1$ or $C_2$. But, if it has an out-hyperedge $h$ in $C_1$, then there is a path from $v$ to another node $v'$, going through $h$. But by convexity, $h$ must then be in $L$, which is a contradiction. Hence $v \in C_2$, which is true if and only if $v \in j$.
\end{proof}



We now introduce the necessary ingredients for the proof of Proposition~\ref{prop:faithful}. The initial object in the category $\PROP$ is the PROP $\PERM$ of permutations: arrows $n \to m$ in $\PERM$ exist only if $m = n$, in which case they are the permutations of the finite ordinal with $n$ elements.
Given a PROP $\X$, the unique PROP morphism $\PERM \to\X$ need not be, in general, faithful; an extreme example is the terminal prop $\mathbf{1}$ where all hom-sets are singletons.
We will say that $\X$ is \emph{faithful} if $\PERM \to\X$ is faithful. Roughly speaking, faithfulness says that no two different permutations are identified. Proposition~\ref{prop:faithful} will follow as corollary of the next lemma about faithful PROPs.

\begin{lem}\label{lem:faithfulCoproducts}
Coproducts of faithful PROPs are faithful and have faithful coproduct injections.
\end{lem}
\begin{proof}
We use the fact that the category of PROPs can be identified with a full subcategory of the coslice $\PERM /\PRO$, see~e.g.\cite[Prop.~2.8]{ZanasiThesis}. Here $\PRO$ is the category of PROs, with: (i) object strict monoidal categories that have the natural numbers as the set of objects, where monoidal product on objects is addition, and (ii) arrows strict monoidal identity-on-objects functors. Since $\PERM$ is symmetric monoidal, $\PROP$ is then the full subcategory of $\PERM /\PRO$ with objects the \emph{symmetric} monoidal functors.

To calculate the coproduct $\X+\Y$ of two faithful PROPs $\X$ and $\Y$ in $\PROP$ is to take the following pushout in $\PRO$.
\[
\xymatrix@R=10pt{
& \PERM \ar[dl]_x \ar[dr]^y \\
\X \ar[dr]_-{i_1} & & \Y \ar[dl]^-{i_2} \\
& \X+\Y
}
\]
Since $x$ and $y$ are symmetric monoidal, it follows that $i_1$ and $i_2$ are symmetric monoidal~\cite[Prop.~2.10]{ZanasiThesis}. It thus remains to show that they are faithful.

Here we use a result of MacDonald and Scull~\cite[Th.~3.3]{MacDonald2009} about amalgamation in the category of categories $\mathbf{Cat}$. Indeed, since $x$ and $y$ are identity-on-objects, $i_1$ and $i_2$ are also identity-on-objects. It suffices to show that $x$ and $y$ satisfy the so-called 3-for-2 property: for $x$, this requires that given $h=g\circ f$ in $\mathbb{X}$, if any two of $f,g,h$ are in the image of $x$ then so is the third.
It is enough to consider $x$ since the argument for $y$ is identical. And here the 3-for-2 property trivially holds, since every arrow of $\PERM$ is an isomorphism.
\end{proof}

\begin{proof}[Proof of Proposition~\ref{prop:faithful}]
Immediate from Lemma~\ref{lem:faithfulCoproducts} since the top row of~\eqref{eq:fterm} is a coproduct diagram in $\mathsf{PROP}$, and $\syntax{\Sigma}$, $\frob$ are both faithful.
\end{proof}

\begin{figure}\caption{Pushout of diagram~\eqref{eq:decomp} \label{fig:bigpushout}}
\centering
    \[
\xymatrix@R=15pt@C=10pt{
n \ar[dr]_{f} & & N+\tilde{n} \ar@{}[dd]|(.8){\wedge}
\ar[dl]_{[id\ j]} \ar[dr]^{id\oplus i_1}
& & {N+\tilde{m}} \ar@{}[dd]|(.8){\wedge}
\ar[dl]_{id\oplus i_2} \ar[dr]^{[id\ p]} & & m. \ar[dl]^{g}
\\
&  N \ar[dr]_{i_1} & & N + \tilde{n} + \tilde{m} \ar@{}[dd]|(.8){\wedge}
 \ar[dl]_{[id \ j]\oplus id }
\ar[dr]^-{([id\ p] \oplus id)\sigma_{\tilde{n},\tilde{m}}}
& & N \ar[dl]^{i_1}
\\
& & N+\tilde{m} \ar[dr]_{[id\ p]}& & N + \tilde{n} \ar[dl]^{[id\ j]}
\\
& & & N
}
\]
\end{figure}


\begin{proof}[Proof of Proposition~\ref{thm:uniquenessBoundaryCompl}]
    Since $\Hyp{\Sigma}$ is a presheaf category, a pushout of hypergraphs consists of pushouts on the underlying sets of nodes and hyperedges and an appropriate choice of source and target maps. Hence the underlying sets of $L^\perp$ must give pushout complements in $\F$:
    \[
    \xymatrix{
    N_L \ar[d]_{f_V} &  i + j \ar[l]_{a_V} \ar[d]^{c_V} \ar@{}[dl]|(.8){\text{\large $\urcorner$}}  \\
    N_G & N_{L^\perp} \ar[l]_{g_V}  \\
    }
    \qquad
    \xymatrix{
    E_L \ar[d]_{f_E} & 0 \ar[l] \ar[d] \ar@{}[dl]|(.8){\text{\large $\urcorner$}}  \\
   E_G & E_{L^\perp} \ar[l]_{g_E}  \\
    }
    \]
    Since $i + j$ is discrete, $E_G$ is a disjoint union, so $E_{L^\perp}$ must be $E_G \backslash E_L$. Since these are diagrams in $\F$, and $c,f$ are mono, we can rewrite the left pushout square as:
    \[
    \xymatrix{
    l + x \ar[d]_{f_V} &  i + j \ar[l]_{a_V} \ar[d]^{c_V} \ar@{}[dl]|(.8){\text{\large $\urcorner$}}  \\
    l + x + y & i + j + z \ar[l]_{g_V}  \\
    }
    \]
    where the two downward arrows are coproduct injections and $l$ is the image of $a_V$. One can easy verify that $l + x + z$ also gives a pushout for the given span, so we obtain a commuting isomorphism $l + x + y \cong l + x + z$, from which we conclude $y \cong z$ and that, up to isomorphism, the pushout complement on nodes must be:
    \[
    \xymatrix{
   l + x \ar[d]_{f_V}  &  i + j \ar[l]_{a_V} \ar[d]^{c_V} \ar@{}[dl]|(.8){\text{\large $\urcorner$}}  \\
    l + x + y  &  i + j + y \ar[l]^{g_V} \\
    }
    \]
    from whence it follows that $g_V = a_V + id_n$.

\medskip
So far, we have proved that the set of nodes $N_{L^\perp}$ and $E_{L^\perp}$ are defined uniquely by the property of being a pushout complement. The only thing that remains is the source $s_p\: E_{L^\perp} \to N_{L^\perp}$ and target $t_p\: E_{L^\perp} \to N_{L^\perp}$ maps.
Since $g$ is a homomorphism, we have that for all hyperedges $h$:
    \[ g_V(s_p(h)) = s_p(g_E(h)) \ \implies\ s_p(h) \in g_V^{-1}(s_p(g_E(h))) \]
    Since $g_V$ is of the form $[(a_1)_V, (a_2)_V] + 1_n$, where $a_1$ and $a_2$ are mono, the inverse image $g_V^{-1}(s_p(g_E(h)))$ contains at most two elements. In the case where it has 1 element, $s_p$ is uniquely fixed, so consider when it has two. It must then be the case that:
    \[ g_V^{-1}(s_p(g_E(h))) = \{ v_1 \in i, v_2 \in j \} \]

But monogamicity of \eqref{eq:boundary} says that the image of $i$ in $L^\perp$ cannot be the source of any hyperedge. Therefore, it must be $s_p(h) = v_2$. Similarly if:
    \[ g_V^{-1}(t_p(g_E(h))) = \{ v_1 \in i, v_2 \in j \} \]
    then $t_p(h)$ must be $v_1$. Since there is at most one choice of source and target maps for $L^\perp$ making $g$ a homomorphism, $L^\perp$ must be unique.
\end{proof} 

\begin{proof}[Proof of Theorem~\ref{th:adequacyRigidSMT}]
We report here the argument for the only if direction of the statement, which is not detailed in the main text. Our assumption gives that
\begin{eqnarray*}
%
 \cgr{circuitd.pdf} & =& \cgr{factl.pdf} \\
 \cgr{circuite.pdf} & =& \cgr{factr.pdf}.
\end{eqnarray*}
whence the following equalities hold in $\syntax{\Sigma} + \frob$, see~\eqref{eq:rewd}-\eqref{eq:rewe}.
\begin{eqnarray}
  \cgr{rewd1.pdf} & =& \cgr{rewd4.pdf} \label{eq:rewcompld}\\
    \cgr{rewe1.pdf} & =& \cgr{rewe4.pdf} \label{eq:rewcomple}
\end{eqnarray}
We now define
\begin{eqnarray*}
 \left( 0 \tr{} D \tl{[q_1,q_2]} n+m\right) & \df & \Phi(\rewiring{d}) = \Phi \left( \cgr[height=.6cm]{rewd1.pdf} \right) \\
 \left( 0 \tr{} E \tl{[p_1,p_2]} n+m\right) & \df & \Phi(\rewiring{e}) = \Phi \left( \cgr[height=.6cm]{rewe1.pdf} \right) \\
 \left( 0 \tr{} L \tl{[a_1,a_2]} i+j\right) & \df & \Phi(\rewiring{l}) = \Phi \left( \cgr[height=.6cm]{rewl.pdf} \right) \\
 \left( 0 \tr{} R \tl{[b_1,b_2]} i+j\right) & \df & \Phi(\rewiring{r}) = \Phi \left( \cgr[height=.6cm]{rewr.pdf} \right) \\
 \left( i+j \tr{} C \tl{} n+m \right) & \df & \Phi \left( \cgr[height=1.1cm]{SplittedContext.pdf} \right). \\
\end{eqnarray*}
By these definitions and \eqref{eq:rewcompld}-\eqref{eq:rewcomple} it follows that
\begin{eqnarray*}
\left( 0 \tr{} D \tl{} n+m \right) = \left( 0 \tr{} L \tl{} i+j\right) \poi \left( i+j \tr{} C \tl{} n+m\right) \\
\left( 0 \tr{} E \tl{} n+m \right) = \left( 0 \tr{} R \tl{} i+j\right) \poi \left( i+j \tr{} C \tl{} n+m\right).
\end{eqnarray*}
Since composition of cospans is defined by pushout, we have a commutative diagram with two pushouts as in~\eqref{eq:dpo3}. It remains to check that the matching $L \to D$ is convex and that $C$ is a boundary complement: these conditions can be verified by definition of the involved components. Therefore, $\Phi(\rewiring{d}) \rigidDPOstep{\Phi(\rewiring{\mathcal{R}})} \Phi(\rewiring{e})$ by application of the rule $\rrule{\Phi(\rewiring{l})}{\Phi(\rewiring{r})}$.
\end{proof} 
Background.tex
% -*- root: ../rewriting.tex -*-

\paragraph{Notation.}
%$\catC[a,b]$ is the set of arrows from $a$ to $b$ in a small category $\catC$, composition of $f \: a \to b$, $g\: b \to c$ is written $f\poi g \: a \to c$.
We write $f\poi g \: a \to c$ for composition of $f \: a \to b$ and $g\: b \to c$ in a category $\catC$.
For $\catC$ a symmetric monoidal category (SMC), $\tns$ is its monoidal product and $\sigma_{a,b} \: a \tns b \to b \tns a$ is the symmetry associated with $a,b \in \catC$. %Given $\funF \: \catC_1 \to \catC_2$, we denote with $\funF^{\op} \: \catC_1^{\op}\to \catC_2^{\op}$ the induced functor on the opposite categories of $\catC_1, \catC_2$.
Given $\catC$ with pushouts, its cospan bicategory has the objects of $\catC$ as $0$-cells, cospans of arrows of $\catC$ as $1$-cells and cospan morphisms as $2$-cells. We denote with $\Cospan{\catC}$ the \emph{category} obtained by identifying the isomorphic $1$-cells and forgetting the $2$-cells.

\medskip


\begin{figure}[t]
 $$
\begin{array}{rcl}
(c \poi c') \poi d = c \poi (c' \poi d) & &
id_n \poi c = c = c\poi id_m\\
%
(c \tns c') \tns d = c \tns (c' \tns d) & &
id_0 \tns c = c  = c \tns id_0\\
%
\end{array} $$
$$
\begin{array}{c}
(c \poi c') \tns (d \poi d') = (c \tns d) \poi (c' \tns d')\\
\sigma_{1,1}\poi\sigma_{1,1}=id_2 \\
(c\tns id_z) \poi \sigma_{m,z} = \sigma_{n,z} \poi (id_z \tns c)
\end{array} $$
\caption{Laws of SMCs instantiated to a PROP $\X$.}\label{fig:axSMC}\end{figure}


\paragraph{SMTs and PROPs.} A standard way of expressing the algebraic structure borne in SMCs is through the notion of \emph{symmetric monoidal theory} (SMT). A one-sorted SMT is determined by $(\Sigma, E)$ where $\Sigma$ is the \emph{signature}: a set of \emph{generators} $o \: n\to m$ with \emph{arity} $n$ and \emph{coarity} $m$ where $m,n\in\N$. The set of $\Sigma$-terms is obtained by combining generators in $\Sigma$, the unit $\id \: 1\to 1$ and the symmetry $\sigma_{1,1} \: 2\to 2$ with $;$ and $\tns$. This is a purely formal process: given $\Sigma$-terms $t \: k\to l$, $u \: l\to m$, $v \: m\to n$, we construct new $\Sigma$-terms $t \poi u \: k\to m$ and $t \tns v \: k+n \to l+n$.  The set $E$ of \emph{equations} contains pairs of $\Sigma$-terms of the form $(t,t' \: i\to j)$; the only requirement is that $t$ and $t'$ have the same arity and coarity.

Just as regular (cartesian) algebraic theories have a categorical rendition as Lawvere categories~\cite{hyland2007category}, the corresponding (linear) notion for SMTs is the one of PROP~\cite{MacLane1965} (\textbf{pro}duct and \textbf{p}ermutation category). %SMTs are presentations of PROPs~\cite{MacLane1965} (\textbf{pro}duct and \textbf{p}ermutation categories).
A PROP is a symmetric strict monoidal category with objects the natural numbers, where $\tns$ on objects is addition. Morphisms between PROPs are identity-on-objects strict symmetric monoidal functors. PROPs and their morphisms form a category $\PROP$.
Any SMT $(\Sigma,E)$ freely generates (presents) a PROP by letting the arrows $n\to m$ be the $\Sigma$-terms $n\to m$ modulo the laws of symmetric monoidal categories (in Figure~\ref{fig:axSMC}) and the (smallest congruence containing the) equations $t=t'$ for any $(t,t')\in E$.

When the set of equations $E$ is empty, we use $\syntax{\Sigma}$ to denote the PROP freely generated by $(\Sigma,E)$.
%Its arrows can be thought of as (symmetric monoidal) syntax: they are just $\Sigma$ terms, modulo the laws of symmetric monoidal categories. We will commonly refer to them as \emph{string diagrams}, or more simply diagrams.
There is a natural graphical representation of these terms as string diagrams, which we now sketch referring to~\cite{Selinger2009} for the details. A $\Sigma$-term $n \to m$ is pictured as a box with $n$ ports on the left and $m$ ports on the right, to which we shall refer with top-bottom enumerations $1,\dots,n$ and $1,\dots,m$. Composition via $\poi$ and $\tns$ are rendered graphically by horizontal and vertical juxtaposition of boxes, respectively.
    \begin{eqnarray}\label{eq:graphlanguage}
t \poi s \text{ is drawn }
\lower5pt\hbox{$\includegraphics[height=.4cm]{graffles/seqcompterms.pdf}$}
\quad
t \tns s \text{ is drawn }
\lower10pt\hbox{$\includegraphics[height=.8cm]{graffles/parcompterms.pdf}$}
\end{eqnarray}
%, which we illustrate below with some examples.
    There are specific diagrams for the $\Sigma$-terms generating the underlying symmetric monoidal structure: these are $\id_1 \: 1 \to 1$, represented as $\Idnet$, the symmetry $\sigma_{1,1} \: 1+1 \to 1+1$, represented as $\symNet$, and the unit object for $\tns$, that is, $\id_0 \: 0 \to 0$, whose representation is an empty space $\ZeronetT$. Graphical representation for arbitrary identities $\id_n$ and symmetries $\sigma_{n,m}$ are generated according to the pasting rules in~\eqref{eq:graphlanguage}. Note that, of the equations displayed in Figure~\ref{fig:axSMC}, the first five are implicit in the diagrammatic language.

It will be sometimes convenient to represent $\id_n$ with the shorthand diagram $\idncircuit$ and, similarly, $t \: n \to m$ with $\lower5pt\hbox{$\includegraphics[height=15pt ]{graffles/circuitt.pdf}$}$.

\begin{exm}\label{exm:props}~
\begin{enumerate}[label=(\alph*)]
\item \label{ex:cmonoids} A basic example is the theory $(\Sigma_M,E_M)$ of \emph{commutative monoids}. The signature $\Sigma_M$ contains two generators:  \emph{multiplication} --- which we depict as the string diagram $\Bmult \: 2 \to 1$ --- and \emph{unit}, represented as $\Bunit \: 0 \to 1$.
 %Graphically, the generation of $\Sigma_M$-terms amounts to ``tiling'' $\Wmult$ and $\Wunit$ together with the circuit $\symNet$ (representing $\sigma_{1,1}\: 2 \to 2$) and $\Idnet$ (representing $\id_1 \: 1 \to 1$).
 Equations in $E_M$ are given in the leftmost column of Figure~\ref{fig:EQFrobenius}: they assert commutativity, associativity and unitality. We call $\Mon$ the PROP freely generated by the SMT $(\Sigma_M,E_M)$. A useful observation is that we can give a concrete representation to $\Mon$: it is isomorphic to the PROP $\F$ with arrows $n \to m$ the functions $\{0,\dots, n-1\}\to \{0, \dots, m-1\}$, see e.g.~\cite{Lack2004a} for details.
\item \label{ex:frob} An example which will play a key role in our exposition is the theory $(\Sigma_F,E_F)$ of \emph{special Frobenius monoids}.
The signature $\Sigma_F$ contains four generators:  $\Bmult \: 2 \to 1$, $\Bunit \: 0 \to 1$, $\Bcomult \: 1\to 2$ and $\Bcounit \: 1\to 0$. %Graphically, the generation of $\Sigma_F$-terms amounts to ``tiling'' the four generators together with the circuit $\symNet$ ($\sigma_{1,1}\: 2 \to 2$) and $\Idnet$ ($\id_1 \: 1 \to 1$).
Equations $E_F$ are displayed in Figure~\ref{fig:EQFrobenius}. They subsume the theory of commutative monoids, in the leftmost column.

Dually, the middle equations state that $\Bcomult$ and $\Bcounit$ form a cocommutative comonoid. Finally, the two rightmost equations describe the interaction between these two structures. %the three axioms on the top-left column assert that $\Bmult$ and $\Bunit$ form a commutative monoid  (from top to bottom, they states commutativity, associativity and identity laws);
%dually, the axioms on the top-left state that $\Bcomult$ and $\Bcounit$ form a cocommutative comonoid; the two bottommost axioms express the interaction between these two structures.
We call $\frob$ the PROP freely generated by $(\Sigma_F,E_F)$. Just as $\Mon$, also $\frob$ enjoys a concrete representation: it is isomorphic to the PROP $\Cospan{\F}$ of cospans in $\F$~\cite{Lack2004a}. %A useful observation (see e.g.~\cite{Lack2004a}) is that there is an isomorphism $\xi$ between $\frob$ and the PROP $\Cospan{\F}$ of cospans in $\F$, where $\F$ is the PROP with arrows $n \to m$  functions $\{0,\dots, n-1\}\to \{0, \dots, m-1\}$.
The isomorphism $\xi\colon \frob \to \Cospan{\F}$ is the unique PROP morphism defined as follows on the generators of $\Sigma_F$.
%\begin{align}\label{eq:frobcospan}
%\Bmult  \longmapsto & \left( 2\rightarrow 1 \leftarrow 1 \right)&
%\Bunit \longmapsto & \left( 0\rightarrow 1\leftarrow 1 \right)\\
%\Bcomult \longmapsto & \left( 1\rightarrow 1 \leftarrow 2 \right)&
%\Bcounit \longmapsto & \left( 1\rightarrow 1 \leftarrow 0\right)
%\end{align}
\begin{equation*}%\label{eq:frobcospan}
\begin{array}{rclrcl}
\Bmult & \longmapsto & \left( 2\rightarrow 1 \leftarrow 1 \right) & \Bunit & \longmapsto & \left( 0\rightarrow 1\leftarrow 1 \right)\\
\Bcomult & \longmapsto & \left( 1\rightarrow 1 \leftarrow 2 \right) & \Bcounit & \longmapsto & \left( 1\rightarrow 1 \leftarrow 0\right)
\end{array}
\end{equation*}

\item \label{ex:ncbialgebras} The theory of \emph{non-commutative bimonoids} consists of a signature:
\[ \{\Wmult,\Wunit,\Wcomult,\Wcounit\}\]
and the following equations:
\begin{equation} \label{eq:ncbialgebralaws}
\lower55pt\hbox{$\includegraphics[height=3.7cm]{graffles/Bialgebrasaxioms.pdf}$}
\end{equation}
We call $\NCB$ the PROP freely generated by these data. Section~\ref{sec:terminationHopf} will show that the induced rewriting system terminates. For this purpose, it will be sometimes convenient to use labels $\mu,\eta,\nu,\epsilon$ resepctively to refer to the four generators of the signature.
\end{enumerate}
\end{exm}
 \begin{figure}[t]\label{fig:frob}
\[
\includegraphics[height=2cm]{graffles/Frobeniusaxioms.pdf}
\]
\caption{The equations $E_F$ of special Frobenius monoids.}\label{fig:EQFrobenius}
\end{figure}

%\begin{figure}\label{fig:Hopf}
%$$\cgr[height=2cm]{hopfalgebra.pdf}$$\caption{The equations $E_B$ of non-commutative bialgebra.}\label{fig:EQBialgebra}
%\end{figure}

\paragraph{Compact-closedness.} SMTs containing a Frobenius monoid will play a special role in our work. We say that an SMT $(\Sigma, E)$ is equipped with a \emph{chosen special Frobenius structure} if $\Sigma = \Sigma' + \Sigma_F$ and $E= E'+E_F$ for some signature $\Sigma'$ and set of equations $E'$. It is relevant for us that PROPs freely generated by such SMTs possess a self-dual compact closed structure~\cite{Kelly1980}. This amounts to the existence, for each $n$, of ``cups'' $\lccn \: n+n \to 0$ and ``caps'' $\rccn \: 0 \to n+n$, subject to the condition that
 \begin{align}\label{eq:snake}
 \lower9pt\hbox{$\includegraphics[height=.8cm]{graffles/snakel.pdf}$} \ = \  \lower1pt\hbox{$\includegraphics[height=.25cm]{graffles/idncircuitNoFrame.pdf}$}  \ = \  \lower9pt\hbox{$\includegraphics[height=.8cm]{graffles/snaker.pdf}$}.
 \end{align}
 The equations of a Frobenius monoid allow to prove~\eqref{eq:snake} with cups defined according to the following pattern
 \begin{multicols}{2}
 \noindent
 \begin{eqnarray*}
\hspace{-.4cm}\lower8pt\hbox{$\includegraphics[width=18pt]{graffles/cup0.pdf}$} & \lower4pt\hbox{$\df$} & \quad  \lower4pt\hbox{$\ZeronetT$}
  \end{eqnarray*}
   \begin{eqnarray*}
  \lower0pt\hbox{$\includegraphics[width=18pt]{graffles/cup2.pdf}$} & \raise4pt\hbox{$\df$} & \lower6pt\hbox{$\includegraphics[height=.9cm]{graffles/epsilondue.pdf}$}
 \end{eqnarray*}
   \begin{eqnarray*}
 \hspace{-.3cm}\lower4pt\hbox{$\includegraphics[width=18pt]{graffles/cup1.pdf}$} & \df & \ \ \lower7pt\hbox{$\includegraphics[height=.7cm]{graffles/rccr.pdf}$}
   \end{eqnarray*} \vspace{-.5cm}
   \begin{eqnarray*}
  \lower4pt\hbox{$\includegraphics[width=18pt]{graffles/cup3.pdf}$} & \df & \lower12pt\hbox{$\includegraphics[height=1.1cm]{graffles/epsilontre.pdf}$}
   \end{eqnarray*}
 \end{multicols}
\noindent and similarly for caps, using instead $\Bcomult$ and $\Bunit$. %By composing $\Bmult$ with $\Bcounit$, one obtains $\lccB$ serving as the counit $\eta_1 \: 0\to 2$. There are similar arrows $\eta_n \: 0 \to 2n$ for arbitrary $n$.
% \begin{multicols}{5}
%\noindent
%  \begin{eqnarray*}
%       \lower18pt\hbox{$
%   \epsilon_0 \df \! \! \! \ZeronetT
%   $}
%    \end{eqnarray*}
%  \begin{eqnarray*}
%       \lower18pt\hbox{$
%   \epsilon_1 \df \! \! \! \lower7pt\hbox{$\includegraphics[height=.7cm]{graffles/rccr.pdf}$}
%   $}
%    \end{eqnarray*}
%  \begin{eqnarray*}
%         \lower18pt\hbox{$
%   \epsilon_2 \df \! \! \! \lower13pt\hbox{$\includegraphics[height=1.2cm]{graffles/epsilondue.pdf}$}
%      $}
%   \end{eqnarray*}
%     \begin{eqnarray*}
%   \ \ \ \epsilon_3 \df \! \! \! \lower15pt\hbox{$\includegraphics[height=1.5cm]{graffles/epsilontre.pdf}$}
%   \end{eqnarray*}
%     \begin{eqnarray*}
%        \lower18pt\hbox{$\dots$}
%   \end{eqnarray*}
%    \end{multicols}
%One can define the unit $\eta_n \: 0 \to 2n$ symmetrically, starting from $\eta_1 \df \rccB \: 0 \to 2$.
The compact-closed structure also yields a contravariant PROP morphism $\coc{\cdot}$ (\emph{cf.} \cite[Rmk~2.1]{Selinger07DaggerCC}) defined as
\begin{align*}%\label{eq:defstar}
 \lower8pt\hbox{$\includegraphics[height=.7cm]{graffles/circuitc.pdf}$} \ \ \ \ \mapsto \ \  \ \ \lower8pt\hbox{$\includegraphics[height=.7cm]{graffles/circuitcstar.pdf}$} \ \df \  %\lower18pt\hbox{$\includegraphics[height=1.3cm]{graffles/circuitsnakenospace.pdf}$}.
 \lower10pt\hbox{$\includegraphics[height=.8cm]{graffles/circuitsnake.pdf}$}.
 \end{align*}
 %mapping $c \: n \to m$ into
%\[\includegraphics[height=1cm]{graffles/circuitsnakenospace.pdf}.\]
%where \lccn is notation for $\eta_n$ and \rccn for $\epsilon_n$.

\medskip



\paragraph{Rewriting in a PROP.}  We now fix an arbitrary PROP $\X$. A rewriting \emph{rule} is a pair $\rrule{l}{r}$ where $l,r \: i \to j $ are arrows of $\X$ with the same source and target. We say that $i\to j$ is \emph{the type} of the rule $\rrule{l}{r}$, and sometimes write $\rrule{l}{r} \: (i,j)$. A \emph{rewriting system} $\mathcal{R}$ is a set of rewriting rules. The rewriting step $d \Ra_\mathcal{R} e$ is defined for any two arrows $d,e \: n \to m$ in $\X$ as   $d \Ra_{\mathcal{R}} e $ iff
$\exists \rrule{l}{r} \: (i,j) \in\mathcal{R}, c_1: n\to k+i, c_2: k+j \to n$ such that $d = c_1 \poi (id_k \tns r) \poi c_2$ and $e = c_1 \poi (id_k \tns r) \poi c_2$, i.e., diagrammatically:
\begin{eqnarray*}%\label{eq:contextshape}
%
 \cgr{circuitd.pdf} &=& \cgr[height=.75cm]{factl.pdf} \\
 \cgr{circuite.pdf} &=& \cgr[height=.75cm]{factr.pdf}.
\end{eqnarray*}

%\includegraphics[height=1cm]{graffles/rewritingstep.pdf}


When the PROP under consideration $\X$ is $\syntax{\Sigma}$ for some signature $\Sigma$, the above notion of rewriting step can be equivalently reformulated  as follows: in order to apply a rewrite rule $\langle l,r \rangle \: (i,j)$ to a diagram $d$ in $\syntax{\Sigma}$
we need to find a match of $l$ in $d$. This means that we need to find a \emph{context} $C$, namely a term in $\syntax{\Sigma + \{\bullet \: i \to j\}}$ with exactly one occurrence of $\bullet$, such that $d = C[l/\bullet]$.
%\begin{equation}
%\label{eq:match}
%d = C[l/\bullet]\text{.}
%\end{equation}
The rewrite then takes $d\Ra_\mathcal{R} e$, where $e = C[r/\bullet]$.
%A rewriting \emph{rule} is a pair $\langle l , r\rangle$ where $l,r \: i \to j $ are arrows of $\syntax{\Sigma}$ with the same arity $m$ and coarity $n$. We say that $m\to n$ is \emph{the type} of the rule $\langle l,r\rangle$, and sometimes write $\langle l,r\rangle :(i,j)$.
%A \emph{rewriting system} $\mathcal{R}$ is a set of rewriting rules.
%
%To apply a rewrite rule $\langle l,r \rangle $ of type $i\to j$ to a diagram $d$
%we need to find a match of $l$ in $d$. This means that we need to find a \emph{context} $C$, namely a term in $\syntax{\Sigma + \{\bullet \: i \to j\}}$ with exactly one occurrence of $\bullet$, such that
%\begin{equation}
%\label{eq:match}
%d = C[l/\bullet]\text{.}
%\end{equation}
%The rewrite then takes $d\Ra_\mathcal{R} e$, where $e = C[r/\bullet]$. The rewriting relation $\Ra_\mathcal{R}$ can be characterised in a very simple way.
%
%\marginpar{Do we need a proof for this?}
%\begin{lem}\label{lemma:rewriting}
% Let $d,e \: n \to m$. Then $d \Ra_{\mathcal{R}} e $ iff
%$\exists \langle l,r \rangle :(i,j)\in\mathcal{R}, c_1: n\to i+k, c_2: j+k \to n$ such that
%$$d = c_1 \mathrel{;} (l\oplus id_k) \mathrel{;}c_2 \,\wedge\, \\ e = c_1 \mathrel{;} (r \oplus id_k) \mathrel{;}c_2
%$$
%\end{lem}

\begin{rmk}
Another common way of viewing a rewrite system on (the arrows) a monoidal category is a to view a collection
of rules $\rrule{l}{r}:(i,j)$ as a computad~\cite{Street-computads} or polygraph~\cite{Burroni1993}. One can then consider the free 2-category on this data, in a similar way to how one obtains a free category on a directed graph.
\end{rmk}


With these definitions, diagrammatic reasoning can now be seen as a special case of rewriting. Given an arbitrary SMT $(\Sigma,E)$
we can obtain a rewriting system $\mathcal{R}_E$ as
\[
\mathcal{R}_E = \{\, \langle t,t'\rangle \,|\, (t,t') \in E \} \cup \{\, \langle t',t\rangle  \,|\, (t,t')\in E \,\}.
\]
%The following relates equality of arrows in the free prop on $(\Sigma,E)$ with rewriting in
%$\syntax{\Sigma}$.
\begin{pro}\label{pro:diagrammaticreasoning}
Let $c,d$ be two diagrams in $\syntax{\Sigma}$. Then $c = d$ in the PROP freely generated by $(\Sigma,E)$ iff
$c \Ra_{\mathcal{R}_E}^* d$.
\end{pro}

%\fznote{Discuss/maybe move to the intro}
%The tricky part -- algorithmically speaking -- is that in \eqref{eq:match} equality means ``equal as arrows of $\syntax{\Sigma}$'', i.e. modulo the equations of symmetric monoidal categories. It's far from clear how to find matches, working with pure syntactic terms. To implement this, we need to develop a theory of rewriting modulo symmetric monoidal structure.
%This is the remit of this work.

%\bigskip

%\bigskip


confBialg.tex
% -*- root: ../rewriting.tex -*-

Before proceeding to the confluence proof, we need to develop a bit of critical pair theory for convex rewriting. For simplicity of the presentation, we will only consider \textit{left-mono} rules, i.e. rules $L \xleftarrow{a} i + j \xrightarrow{b} R$ where $a$ is mono. This means, for instance, that identities are excluded from the LHS of a rewrite rule.

\begin{defn}\label{def:critical-pair}
  Consider a convex rewrite system $\mathcal R$ containing a pair of left-mono rewrite rules:
  \[ L \xleftarrow{a} i + j \xrightarrow{b} R \qquad\qquad L' \xleftarrow{a'} i' + j' \xrightarrow{b'} R' \]
  a \textit{critical pair} consists of a hypergraph $H$ and a pair of convex matchings $f : L \to H$ and $f' : L' \to H$ such that:
  \begin{enumerate}
    \item[(i)] $[f,f'] : L + L' \to H$ is epi, and
    \item[(ii)] the induced morphism from the pullback of $(a \poi f, a' \poi f')$ to the pullback of $(f,f')$ is not an isomorphism.
  \end{enumerate}
\end{defn}

Condition (i) states that $L$ and $L'$ should cover $H$, and condition (ii) that they should overlap non-trivially (i.e. not just on their boundary). Already condition (i) is enough to guarantee that there exist finitely many critical pairs for a certain $L$, $L'$.

Let $H', H''$ be the graphs obtained by rewriting $H$ in \eqref{def:critical-pair} using the two distinct matchings $f, f'$. We say $H$ is \textit{joinable} in $\mathcal R$ if it is possible to rewrite $H'$ and $H''$ into isomorphic cospans using the rules in $\mathcal R$.

\begin{defn}
  A convex rewrite system $\mathcal R$ is \textit{locally confluent} if for any $n \rightarrow G \leftarrow m$, and any single-step rewrites $G \rigidDPOstep{\mathcal{R}} G'$ and $G \rigidDPOstep{\mathcal{R}} G''$ it is possible to rewrite $G'$ and $G''$ into isomorphic cospans using the rules in $\mathcal R$.
\end{defn}

By Newman's Lemma~\cite{Baader1998}, any rewrite system that is locally confluent and terminating is confluent, and hence has unique normal forms. So, how do we lift join-ability of critical pairs to local confluence? If we have $G \rigidDPOstep{\mathcal{R}} G'$ and $G \rigidDPOstep{\mathcal{R}} G''$, then its either the case that the images of the matchings $f$, $f'$ which produced these rewrites have no non-trivial overlap (i.e. they are `parallel-independent'~\cite{HandbookGrammar1997}), in which case they are trivially joinable, or the subgraph $H := \im(f) \cup \im(f')$ yields a critical pair.

Suppose we rewrite $H' \rigidDPOstep{\mathcal{R}} H'_1$ at a matching $f$, with a rule $L \leftarrow i+j \rightarrow R$. Then if the embedding $e : H' \to G'$ is convex, then so too is $e \poi f$, so we can lift the rewrite on $H'$ to a rewrite on $G'$:
\begin{equation}\label{eq:cp-lift}
  \xymatrix{
L \ar[d]_f &
i + j
  \ar@{}[dl]|(.8){\text{\large $\urcorner$}}
  \ar@{}[dr]|(.8){\text{\large $\ulcorner$}}
  \ar[l] \ar[r] \ar[d] &
R \ar[d] \\
H' \ar[d]_e &
C \ar@{}[dl]|(.8){\text{\large $\urcorner$}}
  \ar@{}[dr]|(.8){\text{\large $\ulcorner$}}
  \ar[l] \ar[r] \ar[d] &
H'_1 \ar[d]^{e_1} \\
G' & D \ar[l] \ar[r] & G'_1
}
\end{equation}
and furthermore, we have a convex embedding $e_1 : H'_1 \to G'_1$.
Hence we can lift a sequence of rewrites from $H'$ to $G'$. In particular, we can lift the sequence of rewrites that joins $H'$ and $H''$:
\[ H' \rigidDPOstep{\mathcal{R}} H'_1 \rigidDPOstep{\mathcal{R}} H'_2 \rigidDPOstep{\mathcal{R}} \cdots \rigidDPOstep{\mathcal{R}} K \]
\[ H'' \rigidDPOstep{\mathcal{R}} H''_1 \rigidDPOstep{\mathcal{R}} H''_2 \rigidDPOstep{\mathcal{R}} \cdots \rigidDPOstep{\mathcal{R}} K \]
...to one that joins $G'$ and $G''$:
\[ G' \rigidDPOstep{\mathcal{R}} G'_1 \rigidDPOstep{\mathcal{R}} G'_2 \rigidDPOstep{\mathcal{R}} \cdots \rigidDPOstep{\mathcal{R}} M \]
\[ G'' \rigidDPOstep{\mathcal{R}} G''_1 \rigidDPOstep{\mathcal{R}} G''_2 \rigidDPOstep{\mathcal{R}} \cdots \rigidDPOstep{\mathcal{R}} M \]

However, there is a (not so) little subtlety here: the embedding of $H'$ into $G'$ need not be convex. However, in nice cases it is:

\begin{defn}
  A $i \rightarrow H \leftarrow j$ is called \textit{strongly convex} if for any monogamous, acyclic hypergraph $G$, any embedding $e : H \to G$ is convex.
\end{defn}

There is an easy way to characterise strongly convex cospans:

\begin{lem}
  $i \rightarrow H \leftarrow j$ is strongly convex if any only if there is at least one path from each of its inputs to each of its outputs.
\end{lem}

\begin{proof}
  Suppose there exists one path from every input to every output in $H$, and $H \subseteq G$. Then let $p$ be a path in $G$ from a vertex in $H$ to another vertex in $H$ and suppose this path contains a hyperedge not in $h$. Then, the path must pass out an output $y$ of $H$ and in an input $x$ of $H$, which means there must exist a path from $y$ to $x$. However, there must already be a path from $x$ to $y$, so this would violate acyclicity of $G$. Hence $H$ must be convex. Conversely, if there is not a path from an input $x$ to an output $y$, then we can make a monogamous acyclic graph $H'$ by adding a new hyperedge to $H$ with $y$ as its source and $x$ as its target. Then $H$ is not convex in $H'$.
\end{proof}

If the hypergraph associated to a critical pair is strongly convex, the embedding in \eqref{eq:cp-lift} is automatically convex, so the following is immediate:

\begin{thm}
  A convex rewrite system $\mathcal R$ is locally confluent if all of its critical pairs are strongly convex and joinable.
\end{thm}


From this, we have the necessary theory in place to do critical pair analysis on \BA{}. Enumerating the critical pairs for \BA{} gives 34 distinct critical pairs (see Fig.~\ref{fig:cp}), all of which are strongly convex and joinable. For example, here is the joining of the single critical pair between \BA{1} and \BA{9}:
\[
\cgr[height=3.2cm]{critical}
\]



\begin{figure*}\caption{Critical pairs for \BA{}\label{fig:cp}}
  \medskip
  \centering
  \begin{tabular}{rcccccccccc}
          & \BA{1} & \BA{2} & \BA{3} & \BA{4} & \BA{5} & \BA{6} & \BA{7} & \BA{8} & \BA{9} & \BA{10} \\
   \BA{1} &    2   &   0    &   1    &    0   &    2   &    0   &    0   &    1   &    1   &    0    \\
   \BA{2} &        &   2    &   0    &    1   &    0   &    2   &    1   &    0   &    1   &    0    \\
   \BA{3} &        &        &   1    &    0   &    1   &    0   &    0   &    1   &    1   &    0    \\
   \BA{4} &        &        &        &    1   &    0   &    1   &    1   &    0   &    1   &    0    \\
   \BA{5} &        &        &        &        &    1   &    0   &    0   &    1   &    1   &    0    \\
   \BA{6} &        &        &        &        &        &    1   &    1   &    0   &    1   &    0    \\
   \BA{7} &        &        &        &        &        &        &    1   &    0   &    0   &    0    \\
   \BA{8} &        &        &        &        &        &        &        &    1   &    0   &    0    \\
   \BA{9} &        &        &        &        &        &        &        &        &    1   &    0    \\
  \BA{10} &        &        &        &        &        &        &        &        &        &    1    \\
\end{tabular}
\end{figure*}
% counting one trivial critical pair with itself for everything --- 34 critical pairs (24 not counting self-match)

dpoRewriting.tex
% -*- root: ../rewriting.tex -*-


%The isomorphism of Theorem \ref{} makes an interesting connection between diagrams and hypergraphs. In this section, we lift this correspondence to the corresponding rewriting theory. Indeed rewriting of hypergraphs have been extensively studied in literature \cite{}

In this section, we exploit Theorem~\ref{thm:coproduct} to establish an equivalence between rewriting in a PROP and \emph{DPO rewriting}, defined below.

\begin{defn}[DPO rewriting]\label{defn:dpo}
A \emph{DPO rule} is a span $L \xleftarrow{} j \xrightarrow{} R$  in $\Hyp{\Sigma}$ where $j$ is a  discrete hypergraph.
A \emph{DPO rewriting system} $\mathcal{R}$ is a set of DPO rules.
%
Given $d,e\colon 0\to m$ in $\FTerm\Sigma$, namely $d = 0 \to G\stackrel{}{\leftarrow} m$ and $e = 0\to H\stackrel{}{\leftarrow} m$, we write that $d \DPOstep{\mathcal{R}} e$ if there exist a rule $L \xleftarrow{ } j  \xrightarrow{} R$ in $\mathcal{R}$ and a cospan
$j \rightarrow D \leftarrow m$ such that the following diagram in $\Hyp{\Sigma}$ commutes and the two squares are pushouts.
\begin{equation}\label{eq:dpo2}
\raise25pt\hbox{$
\xymatrix@R=10pt@C=20pt{
L \ar[d]   &  j \ar[d]
\ar@{}[dl]|(.8){\text{\large $\urcorner$}}
\ar@{}[dr]|(.8){\text{\large $\urcorner$}}
\ar[l] \ar[r]  & R \ar[d] \\
 G &  C \ar[l] \ar[r]  & H \\
&  m \ar[u] \ar[ur]_q  \ar[ul]^p
}$}
\end{equation}
The arrow $L \to G$ is called a \emph{matching} of $L$ in $G$.
\end{defn}
The above definition, already appearing in~\cite{Ehrig2004}, extends the standard one~\cite{Ehrig1976} with the ``interface'' $m$: the standard definition can be retrieved by simply taking $m$ to be the empty graph $0$. For examples, we refer the reader to Example~\ref{ex:unsoundcontext} and~\ref{ex:ncbialgebrasrewriting}.

\medskip

The first step in relating PROP and DPO rewriting consists in observing that the latter coincides with \emph{ground} PROP rewriting.
\begin{defn}\label{defn:ground}
A \emph{ground} rewriting system on a PROP $\X$ is a collection of
rules $\rrule{l}{r} \: (i,j)$ with $i = 0$.
\end{defn}
%\begin{defn}[Ground rewriting step]\label{defn:groundStep}
%Let $u,v\colon 0\to n$ be in $\mathbf{X}$. We say that $u\Rightarrow_{\mathcal{R}} v$ if there is a rule $\langle l,r\rangle \in \mathcal{R}$ such that
%$u = D[l/\bullet]$ and $v = D[r/\bullet]$.
%\end{defn}
\begin{lem}\label{lemma:groundrewritingfact}
Let $\mathcal{R}$ be a ground rewriting system on a PROP $\X$ and $d,e: 0 \to m$ be in $\X$. Then
$d \Ra_{\mathcal{R}} e$ if and only if there are $\rrule{l}{r} \: (0,j)\in\mathcal{R}$ and $c:\ j \to m $ such that %$d =  l \poi c$ and $e = r\poi c$.
\begin{equation}\label{eq:rewriting}
  d =  l \poi c \quad \text{ and } \quad e = r  \poi c \text{.}
\end{equation}
\end{lem}
\begin{proof}
Suppose that $d \Ra_{\mathcal{R}} e$. By definition $d$ is like below left. It is equal to the diagram below right by the equations of SMCs. We define the context $c \: j \to m$ as the dashed diagram.
$$\includegraphics[height=1cm]{graffles/groundrewritingproof1.pdf} \qquad \qquad \qquad
\includegraphics[height=1.1cm]{graffles/groundrewritingproof2.pdf}
$$
Similarly, we have $e = r \poi c$. The other direction is trivial.
\end{proof}


%The following relates dpo rewriting
%(Definition~\ref{defn:dpo})
%with ground rewriting in $\FTerm{\Sigma}$
%(Definition~\ref{defn:ground}).
%It is very closely related to the work by Gadducci and Heckel.
%\begin{thm}[Gadducci and Heckel]
%Suppose that $\mathbf{C}$ is a category with pushouts and that
%$\mathcal{R}$ is a ground rewriting system on $\Cospan \mathbf{C}$.
%Then $G \rightarrow_{(l,r)} H$
%iff
%blah
%\end{thm}

Observe that there is a 1-1 correspondence between ground systems in $\FTerm{\Sigma}$  and DPO systems. Indeed, any DPO rule
$L\xleftarrow{} j \xrightarrow{}R$
uniquely induces, by initiality of $0$ in $\Hyp{\Sigma}$, a ground rule $\rrule{0\rightarrow L \xleftarrow{}j}{0\rightarrow R\xleftarrow{}j}$, and viceversa. Moreover, this correspondence lifts to the rewrite relations.


\begin{thm}\label{thm:gadducciheckel}
Let $\mathcal{R}$ be a ground rewriting system in $\FTerm\Sigma$.
Then,
$ d \Ra_{\mathcal{R}} e$ iff $ d \DPOstep{\mathcal{R}} e$.
\end{thm}
\begin{proof}
The conditions in~\eqref{eq:dpo2} are the same as those on \eqref{eq:rewriting}: it is enough to take $c$ in \eqref{eq:rewriting} as $j \rightarrow C \leftarrow m$ in~\eqref{eq:dpo2} and recall that composition in $\FTerm{\Sigma}$ is defined by pushout.
\end{proof}

This correspondence can be further extended to arbitrary -- not necessarily  ground -- rewriting systems. Indeed, in PROPs freely generated by an SMT equipped with a chosen Frobenius structure, for any rewriting system there exists an equivalent ground one. The idea is to bend  a rule $\langle l, r \rangle$ of type $n \to m$ into a ground rule of type $0 \to n+m$ by exploiting the compact closed structure introduced in Section \ref{sec:Background}. To make this intuition formal, for any morphism $c\: n \to m$, we define $\rewiring{d} \: 0 \to n+m$ as% $\eta_n  \poi (id_n \tns c ) $.
\[
\cgr[height=.9cm]{rewd1.pdf}.
\]
%INSERT FIGURE
%\[
%\mathsf{R}: \lower12pt\hbox{$\includegraphics[height=1cm]{graffles/rewiring.pdf}$}
%\quad
%\leadsto
%\quad
%\lower18pt\hbox{$\includegraphics[height=1.5cm]{graffles/curvedbox.pdf}$}
%\]
Then, for a system $\mathcal{R}$, we define the ground rewrite system $\rewiring{\mathcal{R}}$ as
$$\{ \rrule{\rewiring{l}}{\rewiring{r}} \mid \rrule{l}{r}  \in \mathcal{R} \}$$ which, as stated by the following result, is equivalent to $\mathcal{R}$.
%\begin{lem}\label{lem:frobeniusground}
%Let $\mathcal{R}$ be a rewrite system on the PROP freely generated by a symmetric monoidal theory with chosen special Frobenius structure.
%Define the ground rewrite system $\rewiring{\mathcal{R}}$ as
%$$\{ \langle \rewiring{l},\rewiring{r}  \rangle \mid \langle l,r\rangle  \in \mathcal{R} \}$$.
%\end{lem}
%Then, $d\Rightarrow_{\mathcal{R}} e$ iff $\rewiring{d}\Rightarrow_{\rewiring{\mathcal{R}}} \rewiring{v}$.
%\begin{proof}
\begin{lem}\label{lem:frobeniusground}
Let $\mathcal{R}$ be a rewriting system on a PROP freely generated by an SMT equipped with a special Frobenius structure. Then,
$d\Rightarrow_{\mathcal{R}} e$ iff $\rewiring{d}\Rightarrow_{\rewiring{\mathcal{R}}} \rewiring{e}$.
\end{lem}
\begin{proof} For the left-to-right direction, let $\rrule{l}{r} \: i \to j$ be the applied rule. That means, for some $c_1$, $c_2$ and $k$,
\begin{eqnarray}
  \cgr{circuitd.pdf} & =& \cgr[height=.75cm]{factl.pdf} \nonumber \\
 \cgr{circuite.pdf} & =& \cgr[height=.75cm]{factr.pdf}. \label{eq:facteasr}
\end{eqnarray}
Now, using the compact-closed structure and the laws of SMCs we can transform $\rewiring{d}$ as
\begin{eqnarray}
  \cgr{rewd1.pdf} & =& \cgr{rewd2.pdf} \nonumber\\
  & =& \cgr{rewd3.pdf} \label{eq:rewd}\\
  & =& \cgr{rewd4.pdf}. \nonumber
\end{eqnarray}
There is an analogous computation for $\rewiring{e}$ exploiting~\eqref{eq:facteasr}.
\begin{eqnarray}
  \cgr{rewe1.pdf} & =& \cgr{rewe4.pdf} \label{eq:rewe}
\end{eqnarray}
%and similarly for $\rewiring{e}$.
%\begin{eqnarray}
%  \cgr{rewe1.pdf} & =& \cgr{rewe2.pdf} \nonumber\\
%  & =& \cgr{rewe3.pdf} \label{eq:rewe}\\
%  & =& \cgr{rewe4.pdf}\nonumber
%\end{eqnarray}
To conclude, observe that the outcome of \eqref{eq:rewd} rewrites into the outcome of \eqref{eq:rewe} with the rule $\rrule{\rewiring{l}}{\rewiring{r}} \: i \to j$.

For the converse direction, suppose that $\rewiring{d}\Rightarrow_{\rewiring{\mathcal{R}}} \rewiring{e}$ via $\rrule{\rewiring{l}}{\rewiring{r}} \: i \to j$. By Lemma~\ref{lemma:groundrewritingfact} this means that, for some $c$,
\begin{eqnarray}
  \cgr{named.pdf} & =& \cgr{namelcontext.pdf} \label{eq:groundfactdasl}\\
 \cgr{namee.pdf} & =& \cgr{namercontext.pdf}. \label{eq:groundfacteasr}
\end{eqnarray}

Now, by~\eqref{eq:groundfactdasl} we can suitably shape $d$ as follows using the compact-closed and symmetric monoidal structure.
\begin{eqnarray}
  \cgr{circuitd.pdf} & =& \cgr[height=.9cm]{undorewd2.pdf} \nonumber\\
  & =& \cgr{undorewd3.pdf} \label{eq:undorewd}\\
  & =& \cgr{undorewd4.pdf} \nonumber
\end{eqnarray}
We act analogously on $e$ exploiting~\eqref{eq:groundfacteasr}.
\begin{eqnarray}
  \cgr{circuite.pdf} & =& \cgr{undorewe4.pdf} \label{eq:undorewe}
\end{eqnarray}
%\begin{eqnarray}
%  \cgr{circuite.pdf} & =& \cgr{undorewe2.pdf} \nonumber\\
%  & =& \cgr{undorewe3.pdf} \label{eq:undorewe}\\
%  & =& \cgr{undorewe4.pdf} \nonumber
%\end{eqnarray}
Note that the outcome of \eqref{eq:undorewd} is of shape $d_1 \poi (\id \tns r) \poi d_2$ and the one of \eqref{eq:undorewe} is of shape $d_1 \poi (\id \tns r) \poi d_2$, whence $d\Rightarrow_{\mathcal{R}} e$ by application of rule $\rrule{l}{r}$.
\end{proof}

%Recall the isomorphism $\Phi\colon \syntax{\Sigma}+\frob \to \FTerm{\Sigma}$; For a rewriting system $\mathcal{R}$ in
%\syntax{\Sigma}+\frob$, we denote by $\Phi(\matchcal{R})$ the rewrite system on $\FTerm{\Sigma}$ defined as $\{ \langle \Phi(l),\Phi(r)  \rangle \mid \langle l,r\rangle  \in \mathcal{R} \}$.

We now combine the insights provided by Theorem~\ref{thm:gadducciheckel}
and Lemma~\ref{lem:frobeniusground} into
the following theorem, which gives a tight correspondence between rewriting in $\syntax{\Sigma}+\frob$ and DPO rewriting in $\FTerm{\Sigma}$. First, given a rewriting system $\mathcal{R}$ on
$\syntax{\Sigma}+\frob$, we define the system $\Phi(\mathcal{R})$ on $\FTerm{\Sigma}$ as $\{ \rrule{\Phi(l)}{\Phi(r)} \mid \rrule{l}{r}  \in \mathcal{R} \}$ where $\Phi \colon \syntax{\Sigma}+\frob \to \FTerm{\Sigma}$ is the iso of Theorem \ref{thm:coproduct}.


\begin{thm}\label{thm:frobeniusrewriting}%[Rewriting modulo symmetric monoidal axioms + Frobenius structure]
Let $\mathcal{R}$ be any rewriting system on $\syntax{\Sigma}+\frob$. Then,
\[
d \Rightarrow_\mathcal{R} e  \quad \text{ iff } \quad \Phi(\rewiring{d}) \DPOstep{\Phi(\rewiring{\mathcal{R}})}  \Phi(\rewiring{d})\text{ .}
\]
\end{thm}
\begin{proof}
The proof follows immediately by Lemma~\ref{lem:frobeniusground} and Theorems \ref{thm:coproduct},~\ref{thm:gadducciheckel}.
\end{proof}

%\begin{thm}[\label{thm:frobeniusrewriting}Rewriting modulo symmetric monoidal axioms + Frobenius structure]
%Suppose that
%$$\mathbf{F}_\Sigma = (\Sigma+\{\Bmult,\Bunit,\Bcomult,\Bcounit\}, Frob)$$
%is a symmetric monoidal theory with
%chosen Frobenius structure and no additional equations. Suppose that $\mathcal{R}$ is an
%arbitrary rewriting system on $\mathbf{F}_\Sigma$. Then there is a corresponding dpo system $\mathcal{D}$
%in $\FTerm{\Sigma}$ satisfying:
%\[
%u \Rightarrow_\mathbf{R} v  \quad \Longleftrightarrow \quad \mathsf{R}(\Phi u) \Rightarrow_\mathcal{D} \mathsf{R}(\Phi v)
%\]
%\end{thm}
%\begin{proof}
%The system $\mathcal{R}$ is taken to the dpo system
%\[
%\mathcal{D}\Defeq
%\{\, L \leftarrow m+n \rightarrow R \,|\, (m\rightarrow L\leftarrow n, m\rightarrow R\leftarrow n)
%\in\mathcal{R}\,\}
%\]
%\end{proof}

A wide corpus of theorems, algorithm and tools has been developed in the last decade for DPO rewriting on \emph{adhesive} categories \cite{Lack2005}. These can be reused to deal for rewriting SMTs equipped with a Frobenius structure because of Theorem~\ref{thm:frobeniusrewriting} and the following.
\begin{pro}
$\Hyp{\Sigma}$ is adhesive.
\end{pro}
\begin{proof}
The PROP $\F$ of functions is adhesive for the same reasons that $\Set$ is.
Adhesivity of $\Hyp{\Sigma}$ then follows since it is a functor category over $\F$, see~\cite[Prop. 3.5]{Lack2005}.
\end{proof}

The theory of adhesive categories says that pushout complements for a DPO rewriting as in~\eqref{eq:dpo2} are uniquely defined when the arrow $j \to L$ is mono. However, this situation is not enforced by our approach, as shown by the following example.

\begin{exm}\label{ex:unsoundcontext}
Consider $\Sigma = \{ e_1 \: 0 \to 1, e_2 \: 1\to 0, e_3 \: 1 \to 1\}$ and a rewriting system $\mathcal{R}$ with the rule $\rrule{\cgr{id-noframe.pdf}}{\cgr{circuit-e3.pdf}} \: (1,1).$ It gets interpreted in $\FTerm{\Sigma}$ as the DPO rule
$$\cgr{multiplecontexts-dporule.pdf}.$$
The left leg of the span is not mono, and therefore pushout complements are not necessarily unique for the application of this rule, as testified by the following two DPO rewriting steps.
\begin{equation}\label{eq:multiplecontext-goodoutcome}
\vcenter{
\xymatrix@=15pt{
{\cgr[width=7pt]{node.pdf}} \ar[d] & \ar@{}[dl]|(.75){\text{\large $\urcorner$}} {\cgr{wrongcontext-twodots.pdf}} \ar[d]_{g} \ar[l] \ar[r] \ar@{}[dr]|(.75){\text{\large $\ulcorner$}} & {\cgr[height=13pt]{wrongcontext-R.pdf}} \ar[d] \\
{\cgr[height=13pt]{wrongcontext-G.pdf}} & \ar[l] {\cgr[height=13pt]{wrongcontext-PC.pdf}} \ar[r] & {\cgr[height=13pt]{wrongcontext-goodoutcome.pdf}}
}
}
\end{equation}
\begin{equation}\label{eq:multiplecontext-badoutcome}
\vcenter{
\xymatrix@=15pt{
{\cgr[width=7pt]{node.pdf}} \ar[d]   & \ar@{}[dl]|(.75){\text{\large $\urcorner$}} {\cgr[height=13pt]{wrongcontext-twodots.pdf}} \ar[d]_{g'} \ar[l] \ar[r] \ar@{}[dr]|(.75){\text{\large $\ulcorner$}} & {\cgr[height=13pt]{wrongcontext-R.pdf}} \ar[d] \\
{\cgr[height=13pt]{wrongcontext-G.pdf}} & \ar[l] {\cgr[height=13pt]{wrongcontext-PC.pdf}} \ar[r] & {\cgr[height=27pt]{wrongcontext-badoutcome.pdf}}
}
}
\end{equation}
The different outcome is due to the fact $g$ maps $0$ to the leftmost and $1$ to the rightmost node, whereas $g'$ swaps the assignments. Note that, as guaranteed by Theorem~\ref{thm:frobeniusrewriting}, both rewriting steps can be mimicked at the syntactic level in $\syntax{\Sigma} + \frob$. In the second case, one needs to use the compact closed structure.
\begin{eqnarray*}
&\cgr[height=13pt]{multiplecontext1.pdf} \qquad \qquad \Rightarrow_\mathcal{R}& \cgr[height=13pt]{multiplecontext11.pdf} \\ \\
&\cgr[height=13pt]{multiplecontext1.pdf}= \cgr[height=22pt]{multiplecontext22.pdf}= \cgr[height=20pt]{multiplecontext21.pdf} \ \ \ \Rightarrow_\mathcal{R}& \cgr[height=25pt]{multiplecontext23.pdf}
\end{eqnarray*}
%\fznote{This is a placeholder, insert better speech based also on the intro}
%We like to think of this multiplicity of contexts as a feature, rather than a flaw:
%it reveals the flexibility of rewriting with a chosen Frobenius structure.
 \end{exm}
 
 
 \begin{exm}\label{ex:ncbialgebrasrewriting}
In a similar fashion we would like to study the rewriting theory of the SMTs introduced in Example \ref{exm:props}, in particular the case of non-commutative bialgebras (Ex.\ref{exm:props}.\ref{ex:ncbialgebras}). First, we orient left-to-right the equations~\eqref{eq:ncbialgebralaws}, creating a rewriting system $\mathcal{R}_{\scriptscriptstyle \NCB}$. We then obtain the ground rewriting system $\rewiring{\mathcal{R}_{\scriptscriptstyle \NCB}}$ by bending each rule in $\mathcal{R}_{\scriptscriptstyle \NCB}$ and, finally, via the translation $\Phi \: \syntax{\Sigma}+\frob \tr{\cong} \FTerm{\Sigma}$ we obtain the DPO system  $\Phi(\rewiring{\mathcal{R}_{\scriptscriptstyle \NCB}})$ --- see Figure \ref{fig:hopf}. In Section \ref{sec:terminationHopf}, we will show termination of $\Phi(\rewiring{\mathcal{R}_{\scriptscriptstyle \NCB}})$. However, for this to work we first need a rewriting procedure that is sound and complete for rewriting in SMTs, like $\NCB$, that miss the extra Frobenius structure required in Theorem~\ref{thm:frobeniusrewriting}. This extension of our approach is the content of the next section.
\end{exm}


%Cloning rules (i.e., rules such that the left-morphism is not injective) are a well-known issue in the operational presentation of DPO rewriting precisely for the lack of uniqueness of the pushout complement. To this end, various alternative proposals have been put forward, e.g. sesqui-pushouts \cite{Heindel-sesquipushout06}. What is noteworthy of our approach is that \emph{all} possible DPO rewrites can be matched using the compact-closed structure.

%
%We can now give a couple of examples of Theorem~\ref{thm:frobeniusrewriting} in action. In particular,
%we can use Proposition~\ref{pro:diagrammaticreasoning} and show how checking equality in more complex theories can be reduced to performing double pushout rewrite steps.
%
%\begin{exm}[Corelational Frobenius monoids]\label{exm:corelationalfrobenius}
%In the work on quantum, as well as our stuff on signal flow graphs, the Frobenius monoids come equipped with the additional equation bone equation
%$\lower6pt\hbox{$\includegraphics[height=.6cm]{graffles/bone.pdf}$} = \epsilon$. We
%will call such structures \emph{corelational Frobenius monoids}:
%just as the theory of special Frobenius monoids is isomorphic to cospans of functions, the theory of
%\emph{corelational} Frobenius monoids is isomorphic to corelations: jointly surjective cospans of functions\footnote{See recent work by Brendan Fong.}.
%In terms of DPO, following the recipe in the proof of Theorem~\ref{thm:frobeniusrewriting},
% the additional equation is captured as the dpo rule.
%\[
%\lower7pt\hbox{$\includegraphics[height=.7cm]{graffles/blackbone.pdf}$} \quad \leadsto \quad
%\lower8pt\hbox{$\includegraphics[height=.8cm]{graffles/blackbonedpo.pdf}$}
%\]
%\end{exm}
%
%
%\begin{exm}[Interacting Hopf monoids over $\Z_2$]
%This is the symmetric monoidal theory from our FoSSaCS`14 paper, and the phase-free ZX calculus.
%We obtain the dpo rules of Figure~\ref{fig:Z2}, in addition to the rule from Example~\ref{exm:corelationalfrobenius}.
%\begin{figure*}\caption{Dpo rules for Interacting Hopf monoids over $\Z_2$}\label{fig:Z2}
%\[
%  \lower18pt\hbox{$\includegraphics[height=1.5cm]{graffles/bialg.pdf}$} \quad \leadsto \quad
%\lower25pt\hbox{$\includegraphics[height=2cm]{graffles/bialgdpo.pdf}$}
%\]
%\[
%\lower12pt\hbox{$\includegraphics[height=1cm]{graffles/bialg2.pdf}$} \quad \leadsto \quad
%\lower18pt\hbox{$\includegraphics[height=1.7cm]{graffles/bialg2dpo.pdf}$}
%\]
%\[
%\lower7pt\hbox{$\includegraphics[height=.7cm]{graffles/mixedbone.pdf}$} \quad \leadsto \quad
%\lower8pt\hbox{$\includegraphics[height=.8cm]{graffles/mixedbonedpo.pdf}$}
%\]
%\[
%\lower12pt\hbox{$\includegraphics[height=1cm]{graffles/comm.pdf}$} \quad \leadsto \quad
%\lower18pt\hbox{$\includegraphics[height=1.7cm]{graffles/commdpo.pdf}$}
%\]
%\[
%\lower16pt\hbox{$\includegraphics[height=1.3cm]{graffles/assoc.pdf}$} \quad \leadsto \quad
%\lower25pt\hbox{$\includegraphics[height=2cm]{graffles/assocdpo.pdf}$}
%\]
%\[
%\lower12pt\hbox{$\includegraphics[height=1cm]{graffles/unitrule.pdf}$} \quad \leadsto \quad
%\lower16pt\hbox{$\includegraphics[height=1.5cm]{graffles/unitruledpo.pdf}$}
%\]
%\[
%\lower18pt\hbox{$\includegraphics[height=1.5cm]{graffles/frobrule.pdf}$} \quad \leadsto \quad
%\lower25pt\hbox{$\includegraphics[height=2cm]{graffles/frobruledpo.pdf}$}
%\]
%\[
%\lower7pt\hbox{$\includegraphics[height=.7cm]{graffles/whitebone.pdf}$} \quad \leadsto \quad
%\lower8pt\hbox{$\includegraphics[height=.8cm]{graffles/whitebonedpo.pdf}$}
%\]
%\[
%\lower12pt\hbox{$\includegraphics[height=1cm]{graffles/cc.pdf}$} \quad \leadsto \quad
%\lower18pt\hbox{$\includegraphics[height=1.7cm]{graffles/ccdpo.pdf}$}
%\]
%\[
%\lower12pt\hbox{$\includegraphics[height=1cm]{graffles/z2.pdf}$} \quad \leadsto \quad
%\lower12pt\hbox{$\includegraphics[height=1cm]{graffles/z2dpo.pdf}$}
%\]
%\end{figure*}
%\end{exm}


hypergraphs_and_smts.tex
% -*- root: ../rewriting.tex -*-

In order to implement rewriting of string diagrams, we shift our focus away from viewing them as essentially a shorthand for terms, in favour of considering them as combinatorial hypergraph-like structures. In the following let $\F$ be the PROP of functions, introduced in Example~\ref{exm:props}.\ref{ex:cmonoids}. We start by defining the category of hypergraphs.
\begin{defn}[Hypergraphs]
The category of finite directed hypergraphs $\Hyp{}$
is the functor category $\F^{\mathbf{I}}$ where
${\mathbf{I}}$ has as objects pairs of natural numbers $(k,l) \in \N \times \N$ together with one extra object $\star$. % has objects the pairs of natural numbers $(k,l)$ together with one extra object $\star$: $\{(k,l)\,|\,k,l\in\N\}\cup\{\star\}$.
 For each $k,l\in\N$, there are $k+l$ arrows from $(k,l)$ to $\star$.
\end{defn}

The idea is that an object $f$ of $\F^{\mathbf{I}}$ is the hypergraph with set of \emph{nodes} $f(\star)$
and, for each $k,l$, $f(k,l)$ the set of \emph{hyperedges} with $k$ (ordered) sources and $l$ (ordered) targets.
We shall visualise hypergraphs as follows: $\node$ is a node and $\hyperedge$ is an hyperedge, with tentacles attached to the left boundary linking to sources and the ones on the right linking to targets. Here is an example.
\[\lower12pt\hbox{$\includegraphics[height=1cm]{graffles/exhypergraph.pdf}$}\]

In order to serve as an interpretation for string diagrams, we need to extend such vanilla hypergraphs in two ways, leading to the notion of \emph{Frobenius termgraph} (Def.~\ref{def:frobtermgraph}). The first is to assign hyperedges to the generators in a given signature. Formally, this is achieved as follows. Any symmetric monoidal signature $\Sigma$  can be considered as a hypergraph with a single node, in the obvious way. We can then express $\Sigma$-typed hypergraphs as the objects of the slice category $\Hyp{\Sigma} \Defeq \Hyp{}/\Sigma$. The typing is represented pictorially by labeling hyperedges with generators in $\Sigma$.
\[\lower12pt\hbox{$\includegraphics[height=1cm]{graffles/extypedhyp.pdf}$}\]

Henceforward we shall only work in the slice, thus referring to its objects directly as ($\Sigma$-)hypergraphs.

The second piece of data needed to properly represent string diagrams is to identify the ``left and right dangling wires''. A natural solution is to use \emph{discrete cospans}, that is, the full subcategory of $\Cospan{\Hyp{\Sigma}}$ (the \emph{category} of cospans)\footnote{Since $\F$ has pushouts, so does $\Hyp{}$, where they are calculated pointwise in the usual way.} with objects discrete hypergraphs, i.e. those hypergraphs with no edges.

Such discrete cospans can encode terms, termgraphs~\cite{TermGraphSurvey,GadducciCorradini-termgraph} (where variable sharing can occur), but also cyclic structures where, for example, an output of an operation can be fed back as an input. As we shall see (Theorem~\ref{thm:coproduct}), there is a deep connection with the theory of special Frobenius monoids; for this reason, we will refer to these discrete cospans as \emph{Frobenius termgraphs}.

\begin{defn}[Frobenius termgraphs] \label{def:frobtermgraph}
The PROP $\FTerm{\Sigma}$ of $\Sigma$-\emph{Frobenius termgraphs}
is the full subcategory of $\Cospan{\Hyp{\Sigma}}$ with objects the discrete hypergraphs.
 Discrete hypergraphs are in 1-1 correspondence with the objects of $\mathbf{F}$, i.e. the natural numbers, whence $\FTerm{\Sigma}$ is a PROP for the same reasons as $\Cospan{\F}$.% is a PROP.
%Actually, by restricting the objects to $[m]=\{0,1,\dots,m-1\}$, this thing is a PROP.
\end{defn}
%Let $\mathbf{Frob}$ denote the SMT of special Frobenius monoids, with the equations illustrated in Fig.~\ref{fig:frob}.
%\begin{figure}\label{fig:frob}
%\[
%\includegraphics[height=5cm]{graffles/special.pdf}
%\]
%\caption{The equations $Frob$ of special Frobenius monoids.}
%\end{figure}
%Now $\syntax{\Sigma}$ and $\frob$ both enjoy presentations as SMTs, and a coproduct of two such PROPs can also be understood as presented by an SMT through taking the disjoint union of the generators and equations. Then the conclusion of Theorem~\ref{thm:coproduct} means that the PROP $\FTerm{\Sigma}$ of Frobenius termgraphs has as its presentation the SMT with generators from $\Sigma$ and no equations, together with an additional special Frobenius structure.

The terminology \emph{Frobenius termgraph} is justified by the following algebraic characterisation of $\FTerm{\Sigma}$.
\begin{thm}\label{thm:coproduct}
$\FTerm{\Sigma} \cong \syntax{\Sigma} + \frob$
\end{thm}
Theorem~\ref{thm:coproduct} is crucial for our exposition as it serves as a bridge between algebraic and combinatorial structures. It provides a presentation by generators and relation for the PROP $\FTerm{\Sigma}$, which is the union of the SMTs generating $\syntax{\Sigma}$ and $\frob$.

We remark that Theorem 3.3 generalises results already appearing in the literature (see e.g.
 ~\cite[Proposition 3.2]{Rosebrugh2005} and~\cite[Theorem 12]{Gadducci1998}, and the references therein)
 which however dealt only with operations of type $1\rightarrow 1$. Here we consider operations
with arbitrary (co)arities, thus drawing a tighter connection with PROPs.

%We remark that Theorem~\ref{thm:coproduct} generalises a similar result of Rosebrugh, Sabadini and Walters~\cite[Proposition 3.2]{Rosebrugh2005}, which dealt only with operations of type $1\rightarrow 1$; instead we consider operations with arbitrary arities and coarities.
%
\begin{proof}[Proof of Theorem~\ref{thm:coproduct}]
It suffices to verify that $\FTerm{\Sigma}$ satisfies the universal property of coproducts in $\PROP$. First we define morphisms
\[
\SynToCsp{\cdot} \: \mathbf{S}_\Sigma \to \FTerm{\Sigma} \text{ and }
\psi: \frob \to \FTerm{\Sigma}.\]
 Since $\syntax{\Sigma}$ is the PROP freely generated by an SMT with no equations, it suffices to define $\SynToCsp{\cdot}$ on the generators: for each $o \: n \to m$ in $\Sigma$, we let $\SynToCsp{o}$ be the following cospan of type $n \to m$.
\begin{equation}\label{eq:phi}
\cgr[height=1.3cm]{basiccospanFZ.pdf}
\end{equation}
%where the labeling indicates the type of the hyperedge (i.e. to which element of $\Sigma$ it is mapped in the slice $\Hyp{\Sigma}$).
For the definition of $\psi$, recall the isomorphism $\frob \tr{\cong} \Cospan{\F}$ of Example~\ref{exm:props}.\ref{ex:frob}. We let $\psi$ be its composition with the trivial embedding $\Cospan{\F} \to \FTerm{\Sigma}$ given by regarding a set as a discrete graph.
Now, given a PROP $\mathbf{X}$ and morphisms $\alpha:\syntax{\Sigma}\to\mathbf{X}$, $\beta: \mathbf{Frob}\to \mathbf{X}$ we must show that there exists a unique morphism $\upsilon: \FTerm{\Sigma} \to \mathbf{X}$ making the following diagram commute.
\begin{equation}\label{eq:fterm}
\vcenter{\xymatrix@R=16pt{
{\syntax{\Sigma}} \ar[dr]_\alpha \ar[r]^-{\SynToCsp{\cdot}} &
{\FTerm{\Sigma}} \ar@{.>}[d]^<<<\upsilon
& \ar[l]_-{\psi} {\mathbf{Frob}} \ar[dl]^\beta \\
& {\mathbf{X}}
}}
\end{equation}
To do this, we decompose---in an essentially unique way---any Frobenius termgraph into an expression where all the basic constituents lie in the image of $\phi$ and $\psi$. This is possible because we are working with discrete cospans: all of the action happens on the nodes, that intuitively serve as coat-hangers for the edges.

Let  $n \xrightarrow{f} G \xleftarrow{g} n$
be in $\FTerm{\Sigma}$.
Then $G=(N,E,\tau)$ where $N$ is the ordinal of nodes,
$E=\bigcup_{k,l\in \N} E_{k,l}$ is a family of (typed) hyperedges
and $\tau \: E\to \Sigma$ is the type morphism.
Since $n,m$ are discrete, we actually have a cospan of \emph{functions}
$n\xrightarrow {f} N \xleftarrow{g} m$.


Given a hyperedge $e\in E$, $\SynToCsp{\tau e}$ is as illustrated in~\eqref{eq:phi}.
Define
\begin{equation}
\label{eq:decompE}
\tilde{n}\xrightarrow{i} \tilde{E} \xleftarrow{o} \tilde{m} \ \df \ \bigoplus_{e\in E} \SynToCsp{\tau e}.
\end{equation}
 Intuitively, $\tilde{E}$ is the collection of the hyperedges of $G$, but disconnected, and
 $\tilde{n}$ and $\tilde{m}$ are the finite ordinals of
all the inputs and outputs, concatenated. There are the induced canonical maps $j:\tilde{n}\to N$ and
$p:\tilde{m}\to N$ that send a ``disconnected'' input or output node to the corresponding node in $N$.
Now consider the following composition of three arrows in $\FTerm{\Sigma}$.
%\begin{multline}\label{eq:decomp}
%n \xrightarrow{f} V \xleftarrow{[id\ j]} V+\tilde{n} \xrightarrow{id \tns i} V\tns\tilde{E}
%\\
% \xleftarrow{id \tns o} V + \tilde{m} \xrightarrow{[id\ p]} V \xleftarrow{g} m
%\end{multline}
\begin{equation}\label{eq:decomp}
%\vcenter{\xymatrix@R=20pt@C=22pt{
%n \ar[r]^{f} & V & \ar[l]_{[id\ j]} V+\tilde{n} \ar[r]^{id \tns i} & V \tns \tilde{E} \\
%& & & \ar[u]_{id \tns o} V + \tilde{m} \ar[r]^{[id\ p]} & V & \ar[l]_g m
%}}
\vcenter{\xymatrix@R=11pt@C=10pt{
& N & & N \tns \tilde{E} & & N\\
n \ar[ur]^{f} & & \ar[ul]_{[id\ j]} N+\tilde{n} \ar[ur]_{id \tns i} & & \ar[ul]^{id \tns o} N + \tilde{m} \ar[ur]^{[id\ p]} & & \ar[ul]_g m
}}
\end{equation}
%\begin{multline}\label{eq:decomp}
%n \xrightarrow{f} V \xleftarrow{[id\ j]} V+\tilde{n} \xrightarrow{id \tns i} V\tns\tilde{E}
%\\
% \xleftarrow{id \tns o} V + \tilde{m} \xrightarrow{[id\ p]} V \xleftarrow{g} m
%\end{multline}

It is straightforward to compute the resulting pushouts in $\F$ and conclude that we obtain
$n \xrightarrow{f} G \xleftarrow{g} m$ as a result. Indeed, it suffices to focus on the nodes (see Fig. \ref{fig:bigpushout} in appendix). Since the constituents of~\eqref{eq:decomp} are all in the image of $\phi$ and $\psi$, this means that
we can define $\upsilon$ on $G$: this assignment is well-defined and moreover unique since the decomposition is unique up-to permutation of $\tilde{E}$, and $\mathbf{X}$ is symmetric monoidal.
\end{proof}

We are interested in $\FTerm{\Sigma}$ as a combinatorial universe for rewriting in $\syntax{\Sigma}$. In the remainder of this section we thus focus on the coproduct injection $\SynToCsp{\cdot} \: \mathbf{S}_\Sigma \to \FTerm{\Sigma}$. Our first observation is that $\SynToCsp{\cdot}$ is \emph{faithful}; we refer the reader to Appendix~\ref{app:proofs} for the proof, which relies on properties of coproducts in $\PROP$.

\begin{pro}\label{prop:faithful}
$\SynToCsp{\cdot} \: \syntax{\Sigma} \to \FTerm{\Sigma}$ is faithful.
\end{pro}


%So $\SynToCsp{\cdot}$ goes some way to explain the dual ``syntactic term - combinatorial object'' nature of terms of symmetric monoidal theories! The rest of the paper is devoted to making this correspondence more precise.

%\fznote{$\mathbf{F}_\Sigma$ is a prop, not an SMT}
%\begin{defn}
%An SMT $\mathbf{F}_\Sigma$ is said to be equipped with a
%\emph{chosen special Frobenius structure} if it
%can be presented as
%\[(\Sigma+\{\Bmult,\Bunit,\Bcomult,\Bcounit\},E+Frob)\]
%where $Frob$ is the set
%of equations of Fig.~\ref{fig:frob}.
%\end{defn}
%
%The following now follows from the statement of Theorem~\ref{thm:coproduct}.
%\begin{cor}
%Suppose that $\mathbf{F}_\Sigma$ has a chosen special Frobenius structure and no other equations.
%Then there is an isomorphism of props $\Phi: \mathbf{F}_\Sigma \to \mathbf{FTerm}_\Sigma$, defined
%on the (non-Frobenius) generators as in~\eqref{eq:phi}, and on the Frobenius generators as follows:
%\[
%\Bmult \qquad\longmapsto\qquad 2\rightarrow 1 \leftarrow 1
%\]
%\[
%\Bunit \qquad\longmapsto\qquad 0\rightarrow 1\leftarrow 1
%\]
%\[
%\Bcomult \qquad\longmapsto\qquad 1\rightarrow 1 \leftarrow 2
%\]
%\[
%\Bcounit \qquad\longmapsto\qquad 1\rightarrow 1 \leftarrow 0
%\]
%\end{cor}
%\begin{proof}
%Clearly
%$\mathbf{F}_\Sigma\cong \syntax{\Sigma} + \frob$
%and by Theorem~\ref{thm:coproduct}, $\syntax{\Sigma}+\frob\cong \FTerm{\Sigma}$.
%The definition of $\Phi$ above is just the combination of $\SynToCsp{\cdot}$ and $\psi$, taking into account that
%$\frob$ is a presentation of $\Cospan{\F}$.
%\end{proof}


We conclude this section with a combinatorial characterisation of the image of $\SynToCsp{\cdot}$. A preliminary series of definitions introduces the relevant hypergraph notions: \emph{monogamicity} and \emph{acyclicity}.

\begin{defn}[Degree of a node]
The \textit{indegree} of a node $v$ in hypergraph $G$ is the number of pairs $(h,i)$ where $h$ is an hyperedge with $v$ as its $i$-th target. Similarly, the \textit{outdegree} of $v$ is the number of pairs $(h,j)$ where $h$ is an hyperedge with $v$ as its $j$-th source.
  %Let the \textit{in-arity} of a node $v$ in hypergraph $G$ be the number of pairs $(h,i)$ with $h \in E_G$, $i \in \mathbb N$ where $t_i(h) = v$. Similarly, let the \textit{out-arity} be the number of pairs $(h,j)$ where $s_j(h) = v$.
\end{defn}

\begin{defn}[Monogamicity] \label{def:monogamous} Given $m \tr{f} G \tl{g} n$ in $\FTerm{\Sigma}$, let $\inp{G}$ be the image of $f$ and $\out{G}$ the image of $g$. We say that $G$ is \emph{monogamous} if $f$ and $g$ are mono and, for all nodes $v$ of $G$,
\begin{align*}
\textrm{the indegree of $v$ is } & \begin{cases} 0 &\mbox{if } v \in \inp{G} \\
1 & \mbox{otherwise.} \end{cases} \\
\textrm{the outdegree of $v$ is } & \begin{cases} 0 &\mbox{if } v \in \out{G} \\
1 & \mbox{otherwise} \end{cases}
\end{align*}
\end{defn}
\begin{exm}
The following three cospans are \emph{not} monogamous.
\[1 \tr{} \cgr{nonmog1.pdf} \tl{} 1 \quad 1 \tr{} \cgr{nonmog2.pdf} \tl{} 1 \quad 1 \tr{} {\raise2pt\hbox{$\cgr{nonmog3.pdf}$}} \tl{} 1.\]
\end{exm}

\begin{rmk}%\fznote{Is this true?}
There is a more compact characterisation of monogamicity that uses the decomposition~\eqref{eq:decomp}: the factorised cospan is monogamous precisely when
\[
[ f \ p ] \: n+\tilde{m} \to V \text{ and }[ g\ j ] \: m+\tilde{n} \to V
\]
 are bijections.
\end{rmk}




%MOVED TO APPENDIX
%\begin{defn}
%    For a pair of hyperedges $h,h'$, we call $h$ a \textit{predecessor} of $h'$ and $h'$ a \textit{successor} of $h$ if there exists a node $v$ in the target of $h$ and in the source of $h'$.
%    %For a pair of hyperedges $h,h'$ such that for some $i,j$ and node $v$, $t_i(h) = v = s_j(h)$, then $h$ is called a \textit{predecessor} of $h'$ and $h'$ a \textit{successor} of $h$.
%\end{defn}
%
%\begin{defn}[Directed path]
%    For a hypergraph $G$ and hyperedges $h,h'$, a \textit{directed path} $p$ from $h$ to $h'$ is a sequence of hyperedges $[h_1, \ldots, h_n]$ such that $h_1 = h$, $h_n = h'$, and for $i < n$, $h_{i+1}$ is a successor of $h_i$. We say $p$ starts at a subgraph $H$ if $H$ contains a node in the source of $h$, and terminates at a subgraph $H'$ if $H'$ contains a node in the target of $h'$. We say $p$ starts at a subgraph $H$ if there exists some $i$ such that $s_i(h) \in H$, and terminates at a subgraph $H'$ if there exists some $j$ where $t_j(h') \in H'$.
%\end{defn}
%
%By regarding nodes as single-node subgraphs, it clearly makes sense to talk about directed paths from/to nodes as well.

The standard notion of \emph{directed path} from a node $v$ to a node $v'$ in a directed graph generalises to (directed) hypergraphs in the expected way. See Appendix~\ref{app:proofs} for the details.

\begin{defn}[Acyclicity] \label{def:directedacyclic}
    A hypergraph $G$ is \textit{directed acyclic} if there exists no directed path from a node to itself. We also call a cospan $n \tr{} G \tl{} m$ directed acyclic if the property holds for $G$.
\end{defn}


\begin{defn}[Convex sub-hypergraph] \label{def:convexsubhyp}
A sub-hypergraph $H \subseteq G$ is \textit{convex} if, for any nodes $v, v'$ in $H$ and any directed path $p$ from $v$ to $v'$, every hyperedge in $p$ must also be in $H$.
\end{defn}


\begin{lem}\label{lemma:convexfact}
    Let $m \rightarrow G \leftarrow n$ be a monogamous directed acyclic cospan and $L$ a convex sub-hypergraph. Then $L$ extends to a unique cospan $i \rightarrow L \leftarrow j$ such that $G$ factors as:
    \begin{equation}\label{eq:snd-factor}
    \left( n \tr{} C_1 \tl{} i\!+\!k \right) \poi\!\!\!\!\!
    \begin{array}{cc}
    \left( k \tr{id} k \tl{id} k \right)\\
    \tns \\
    \left( i \tr{} L \tl{} j \right)
    \end{array}
    \!\!\!\!\!\poi
    \left( j\!+\!k\tr{} C_2 \tl{} m \right)
    \end{equation}
    where all cospans in~\eqref{eq:snd-factor} are monogamous directed acyclic.
\end{lem}




\begin{thm}\label{thm:charactImage} $n \tr{} G \tl{} m$ in $\FTerm{\Sigma}$ is in the image of $\SynToCsp{\cdot}$ if and only if $n \tr{} G \tl{} m$ is monogamous directed acyclic. \end{thm}
\begin{proof}
The only if direction is easily verifiable by induction on $d$ such that $\SynToCsp{d} = n \tr{} G \tl{} m$. For the converse direction, we can reason by induction on the number of hyperedges in $G$. If $G$ does not contain any, then monogamicity and acyclicity imply that $n\tr{}G$ and $m\tr{}G$ are bijections, so that $n \tr{} G \tl{} m$ is in the image of an arrow only consisting of identities and symmetries.
%then the assumption of monogamicity and acyclicity guarantees that it is in the image of an arrow in $\syntax{\Sigma}$ only consisting of identities and symmetries.
Otherwise, suppose that $G$ consists of a single hyperedge $E$: it must have a $\Sigma$-type, say the generator $o \in \Sigma$. Because $n \tr{} G \tl{} m$ is monogamous directed acyclic, $o$ must have source $n$ and target $m$ as an arrow of $\syntax{\Sigma}$ and $\SynToCsp{o \: n \to m} = n \tr{} G \tl{} m$.

For the inductive step, we pick any hyperedge $E$ of $G$. By monogamicity and acyclicity, $E$ must be a convex sub-hypergraph of $G$. Hence, by Lemma~\ref{lemma:convexfact}, $n \tr{} G \tl{} m$ factors as~\eqref{eq:snd-factor}, with $L$ being $E$.
%\begin{equation*}
%    \left( n \tr{} C_1 \tl{} i\!+\!k \right) \poi\!\!\!\!\!
%    \begin{array}{cc}
%    \left( k \tr{id} k \tl{id} k \right)\\
%    \tns \\
%    \left( i \tr{} E \tl{} j \right)
%    \end{array}
%    \!\!\!\!\!\poi
%    \left( j\!+\!k\tr{} C_2 \tl{} m \right).
%    \end{equation*}
    The lemma guarantees that all the above cospans are monogamous directed acyclic. Therefore, by inductive hypothesis they are in the image of $\SynToCsp{\cdot}$, allowing us to conclude by functoriality that the same holds for $n \tr{} G \tl{} m$.
%For the converse direction, since $G$ is supposed to be acyclic it admits a ranking $R_0, \dots, R_k$ in which each rank $R_i$ contains exactly one hyperedge. Each rank $R_i$ yields as a cospan $n_i \tr{} G_i \tl{} m_i$ such that \[ n \tr{} G \tl{} m = \left(n_0 \tr{} G_0 \tl{} m_0 \right) \poi \dots \poi \left(n_k \tr{} G_k \tl{} m_k \right)\] By monogamicity, for each $i$ we have $n_i \tr{} G_i \tl{} m_i = \SynToCsp{d_i}$, with $d_i = \id \tns o \tns \id$ for some generator $o$ in $\Sigma$. We then conclude by functoriality that $\SynToCsp{d_0 \poi \dots \poi d_k} = n \tr{} G \tl{} m$.
\end{proof} 
intro.tex
% -*- root: ../rewriting.tex -*-
\enlargethispage{\baselineskip}
\enlargethispage{\baselineskip}
\enlargethispage{\baselineskip}

 Symmetric monoidal categories (SMCs) are algebraic structures that feature sequential ($\poi$) and parallel ($\tns$) composition. This phenomenon seems commonplace, and indeed SMCs have found many applications in computer science, physics and related fields. Focussing on computer science, they have recently featured in concurrency theory, where they describe the concurrent nature of
 executions of Petri nets~\cite{Meseguer1990} as well as serving as their compositional algebra~\cite{Bruni2011, Sobocinski2014}, quantum information, where they have been used to model quantum circuits~\cite{Coecke2008, Coecke2012}, and in systems theory, where they provide a calculus of signal flow graphs~\cite{Bonchi2014b,Bonchi2015,BaezErbele-CategoriesInControl}. %, Fong2015}.

In each case, the algebra of SMCs gives us a syntax to talk about domain-specific artefacts. However,
 the two composition operations in an SMC are related by functoriality, and symmetries are natural: this imposes a non-trivial structural equality relation on terms from the outset---something that researchers in process algbera might refer to as a \emph{structural congruence}---that makes using ordinary tree-like syntax ineffectual. Functoriality, in particular, means that, given terms $A, B, C, D$ where $A$,$B$ and $C$,$D$ can be composed sequentially, we have that
\[ (A \tns C) \poi (B\oplus D)
=
(A \poi B) \tns (C \poi D).
\]
This equation is sometimes reffered to as the \emph{middle-four interchange}.
%
As a consequence, the syntax is intrinsically 2-dimensional, and for this reason diagrams---in this context often referred to as \emph{string diagrams}---are a more efficient representation for arrows of SMCs. Using string diagrams, both sides of the equation above are represented diagrammatically as
\[
\cgr[height=1cm]{middlefour.pdf}
\]
and so middle four interchange is built into the representation, along with other equational properties such as associativity of both composition operations.

String diagrams has been pioneered by Feynman and Penrose, but they remained just a tool for calculations, ultimately excluded from papers. This was likely due to a
lack of foundational
results that justified the soundness of their use: the careful mathematician checked each step
in a diagrammatic proof using standard term-based means.
%
%
%String diagrams has been pioneered by Feynman and Penrose, but they remained just a tool for calculations, ultimately excluded from papers. This was likely due to a lack of appropriate typesetting technology, but the dearth of foundational results that justified the soundness of their use must have also played a part: the careful mathematician checked each step in a diagrammatic proof using standard term-based means.
%
This changed with the 1991 paper~\cite{Joyal1991} of Joyal and Street who formalised diagrams as topological structures and understood diagrammatic manipulation as homotopy.  Their framework allowed them to show that the resulting diagrams-up-to-homotopy-equivalence served as a description for the arrows of free braided monoidal categories, of which SMCs are a special case. Subsequently, the use of diagrammatic notation exploded, see e.g. the survey~\cite{Selinger2009}.
%The use of string diagrams has an interesting history. Originally pioneered by Feynman and Penrose for tensor calculations, they remained for several decades as quasi trade-secret house notation, employed for calculations, but ultimately excluded from papers. This was surely due in part to a lack of appropriate typesetting technology, but the dearth of foundational results that justified the soundness of their use must have also played a part: the careful mathematician checked each step in a diagrammatic proof using standard term-based means. This changed with the 1991 paper ~\cite{Joyal1991} of Joyal and Street who formalised diagrams as topological structures and understood diagrammatic manipulation---such as the equality of the diagrams below, which is an instance of naturality of symmetry---as homotopy.  Their framework allowed them to show that the resulting diagrams-up-to-homotopy-equivalence served as a description for the arrows of free braided monoidal categories, of which SMCs are a special case. Subsequently, the use of diagrammatic notation exploded, even meriting a survey paper by Selinger~\cite{Selinger2009}.
% \[
% \cgr[height=.8cm]{naturality.pdf}
% \]
The results of Joyal and Street mean that we have a formal description of the nature of 2-dimensional syntax, and so of the arrows of free braided monoidal categories.

Most applications, however, do not feature free categories but rather rely on the presence of additional equations: for example, algebraic structures such as bimonoids and Frobenius monoids are commonplace.
Adding equations to a theory of string diagrams means that diagrammatic proofs include \emph{rewriting}: if the left hand side of an equation can be found in a larger string diagram, it can be deleted and replaced with its right hand side. Rewriting plays a similar role if string diagrams represent the topology of a system that may change dynamically during execution. From a mathematical point of view, one can formulate rewrite rules as generator 2-cells (this data structure is variously called a \emph{computad}~\cite{Street-computads} or a \emph{polygraph}~\cite{Burroni1993}) and consider the resulting free 2-category, where the 2-cells witness the possible rewriting trajectories. This does not solve the problem of how to \emph{implement} rewriting, and the approach of Joyal and Street does not offer an immediate solution either; we do not have an off-the-shelf rewriting theory for their diagrams.

One of the fundamental difficulties with working with terms modulo the laws of SMCs is finding matches. For example, consider the following rewrite rule
\[
\cgr[height=.7cm]{examplerule.pdf}
\]
then, using naturality, we ought to be able to find a match in
\[
\cgr[height=1.7cm]{exampleterm.pdf}
\]
which, viewed as a term, does not contain the left hand side as a subterm, and requires a non-trivial deformation in order for this to be the case.

\medskip

Our approach is to think of string diagrams neither as terms nor as topological entities, but rather as combinatorial structures: i.e. as certain ``open'' (hyper-)graphs. Roughly speaking---since we are considering the symmetric monoidal case---the geometry of diagrams is discarded, and only connectivity information remains. Rewriting of diagrams then becomes an instance of graph rewriting, in particular the double pushout (DPO) approach, a well-trodden research topic that goes back to the 1970s~\cite{Ehrig1976}. The correspondence between rewriting modulo the laws of SMC and DPO is surprisingly tight, as we explain below.

To establish the connection between rewriting of string diagrams on the one hand and graph rewriting on the other, we extend and connect together two existing research threads. First, there has been work on understanding the algebraic nature of cospans of graphical structures e.g.~\cite{Rosebrugh2005}, where the algebra of special Frobenius monoids was shown to play a crucial role. In a cospan  $n \to G \leftarrow m$, the open nature of graphs is given by the `�nterfaces'' $n$ and $m$ which, like ``dangling wires'' in string diagrams, allow composition on the left and on the right.
%We extend this work and show that categories of cospans of hypergraphs are isomorphic to free SMCs together with a \emph{chosen special Frobenius structure}; these categories have been called well-supported compact closed categories by Walters and others~\cite{Walters-lecture-WSCC}.

%Second, there has been work connecting rewriting of cospans~\cite{Sassone2005a,Gadducci1998} and DPO graph rewriting: essentially, to give a \emph{ground} rewriting system on cospans of graphs is to consider a DPO graph rewriting system, extended in an obvious way to account for the boundaries.
\noindent \begin{minipage}{0.85\linewidth}
Second, there has been work connecting computads in cospans~\cite{Sassone2005a,Gadducci1998} and DPO graph rewriting:
the key observation is that DPO
rules, which are usually presented as spans of graphs $L\leftarrow j \rightarrow R$, corresponds to rewrite rules in the cospan category as displayed on the right, where $0$ is the initial object in the category of graphs.
%$$\xymatrix{ & L \ar@{=>}[dd] & \\
%0 \ar[ur] \ar[dr] & & j \ar[ul] \ar[dl] \\
%& R &
%} $$
\end{minipage}
\begin{minipage}{0.15\linewidth}
\vspace{-0.5cm}
$$\xymatrix@C=0.02cm@R=0.3cm{ & j   \ar@/^/[dr] \ar@/_/[dl] & \\
L   \ar@{=>}[rr] & & R\\
& 0 \ar@/^/[ul] \ar@/_/[ur] &
} $$
\end{minipage}

Our starting point is the extension of the result in~\cite{Rosebrugh2005} from graphs to hypegraphs. This is essential to tackle arbitrary symmetric monoidal signatures $\Sigma$: the category of cospans of hypergraphs with type $\Sigma$ is isomorphic to the free \textit{hypergraph category}, that is the SMC freely generated by $\Sigma$ together with a chosen special Frobenius structure. Hypergraph categories have previously been called well-supported compact closed categories by Walters~\cite{Walters-lecture-WSCC}.

By connecting this result with the observations in~\cite{Sassone2005a,Gadducci1998}, we are able to show that DPO is just rewriting modulo the laws of SMCs ``plus'' Frobenius. More formally, a DPO system on hypergraphs of type $\Sigma$ amounts to a rewriting system on the free SMC generated by $\Sigma$ together with a chosen special Frobenius structure. Intuitively speaking, the special Frobenius structure brings a self-dual compact closed structure, which in turn allows us to bend rules around: an arbitrary rewriting rule of cospans, as below on the left, can always be transformed into the DPO rule on the right.
$$
\xymatrix@C=0.02cm@R=0.2cm{ & j   \ar@/^/[dr] \ar@/_/[dl] & \\
L   \ar@{=>}[rr] & & R\\
& i \ar@/^/[ul] \ar@/_/[ur] &
} \qquad \qquad \qquad
\xymatrix@C=0.001cm@R=0.2cm{ & i+ j   \ar@/^/[dr] \ar@/_/[dl] & \\
L   \ar@{=>}[rr] & & R\\
& 0 \ar@/^/[ul] \ar@/_/[ur] &
}
$$
Next we tackle rewriting modulo the equations of SMCs in isolation. We can still consider DPO, but we must be more careful about rule application: since we may not have a compact closed structure on the algebraic side, it may be the case that a graph rewriting rule is unsound when considered as a rewrite of string diagrams. We introduce a restricted form of DPO rewriting, called convex DPO rewriting, and we prove that it is sound and complete with respect to rewriting modulo symmetric monoidal structure.
\[
\hspace{-.5cm}\cgr[height=3.7cm,width=9.5cm]{bullshitpicture.pdf}
\]
We conclude the paper with an illustrative example of our approach. We show termination for the theory of \emph{non-commutative bimonoids} (a.k.a. bialgebras). As any non-commutative group yields a bialgebra whose multiplication is non-commutative, these play an important role in representation theory, and the case where neither the multiplication nor the comultiplication is commutative forms the basis of the study of quantum groups~\cite{Kassel-quantumgroups2012}.

%
%The motivation for our approach is twofold:
%\begin{itemize}
%\item to lay the theoretical foundations needed for the development of comprehensive tool support for reasoning about rewriting in SMCs. Already existing tools such as Quantomatic~\cite{Kissinger_quantomatic} rely on additional structure, requring for example that the ambient category be compact closed, or do not factor in the symmetric structure, such as Globular~\cite{Globular} \fznote{Is this right?}.
%\item to develop a setting where standard problems regarding rewriting systems in SMCs---such as verifying confluence and/or termination---can be expressed in a clear, rigorous way that is amenable to established practice; e.g. the employment of a well-founded order in order to prove termination.
%\end{itemize}

\paragraph{Related work.}

The correspondence between terms of algebraic structures with sequential and parallel composition (ultimately representing arrows of a free SMC) and flow diagrams (i.e., suitable hyper-graphs) has been recognized early on in computer science, and formalized at least since the work of Stefanescu (see the references in the survey~\cite{Selinger2009}). After~\cite{Joyal1991}, and especially after the paper on traced monoidal categories by Joyal, Street and Verity~\cite{Joyal_tracedcategories}, there has been a flourishing of interest in 2-dimensional diagrams. A 2-categorical equivalent for rewriting has also been devised almost immediately after, including the aforementioned correspondence with DPO rewriting~\cite{Gadducci1998}, even if usually for restricted kinds of diagrams. Our results duly extend those previous works.
On the one-side, the correspondence between string diagrams and SMCs (and their rewriting theories) is put on a theoretical firm
foundation, paving the way for a general theory encompassing different kind of diagrams, e.g. by enforcing constraints on the input and output degrees of nodes. On the other, it clearly recast the current development of PROP rewriting, establishing a fruitful link with the well-established, operational world of DPO rewriting.


A long tradition, pioneered by the work of Burroni on polygraphs~\cite{Burroni1993}, generalises term rewriting to higher dimensions, including the three-dimensional case of string diagram rewriting --- see e.g.~\cite{Mimram14} for a survey. In these works, the laws of SMCs are usually encoded as rewriting rules, resulting in rather elaborated rewriting systems whose analysis is often challenging (see e.g. \cite{Lafont2003,DBLP:journals/corr/abs-math-0612083}).
%
On the one hand, this traditional approach is far more general than ours that only deals with SMCs. On the other hand, our graphical representation allows to abstract away all the laws of SMCs, so to reduce considerably the number of rewriting rules and simplify the analysis of the rewriting systems.

In~\cite{open_graphs1}, the authors use cospans of \textit{string graphs} (a.k.a. open graphs) to encode morphisms in a symmetric monoidal category and reason equationally via DPO rewriting. There is an evident encoding of the hypergraphs we use to string graphs, which yields an equivalence between the category of directed cospans from~\cite{open_graphs1} and our subcategory of monogomous acyclic cospans in $\FTerm{\Sigma}$ (characterised in Theorem~\ref{thm:charactImage}). However, the notion of rewriting considered by those authors is more permissive, and is only sound in general when there is at least traced structure on the SMC.


%\marginpar{Aleks, INSERT HERE comment about Dixon Kissinger}




\paragraph{Structure of the paper.} Section~\ref{sec:Background} provides some background on SMCs and the rewriting of the associated diagrams. Section~\ref{sec:HypInterpretation} introduces the combinatorial structures for interpreting diagrams and characterise them algebraically in terms of Frobenius monoids. Section~\ref{sec:dpoRewriting} properly establishes the correspondence between DPO rewriting and rewriting in a free SMC with a chosen special Frobenius monoid. Section~\ref{sec:SymMonDpoRewriting} characterises a restriction of DPO rewriting, called \emph{convex}, that is adequate for rewriting in any free SMC. Section~\ref{sec:terminationHopf} shows termination for the theory of non-commutative bimonoids. Appendix~\ref{app:proofs} contains the proofs omitted in the main text.

%Suppose that  $\syntax{\Sigma}$ is the symmetric monoidal theory on some signature $\Sigma$, with no equations. This is a free prop, where the arrows can be thought of as (symmetric monoidal) syntax: that is, they are terms constructed from the elements of $\Sigma$ using $;$ and $\oplus$, modulo the laws of symmetric monoidal categories.
%
%A rewriting system $\mathcal{R}$ is a set of pairs $\langle l , r\rangle$,  each  consisting of type-compatible arrows of
%$\syntax{\Sigma}$: that is, for each pair $\langle l,r\rangle \in\mathcal{R}$ there exist $m,n\in\N$ such that $l,r:m\to n$ in $\syntax{\Sigma}$. We say that $m\to n$ is \emph{the type} of the rule $\langle l,r\rangle$, and sometimes write
%$\langle l,r\rangle :(m,n)$.
%
%To apply a rewrite rule $\langle l,r \rangle $ of type $m\to n$ to an arrow $c$
%we need to find a match of $l$ in $c$. This can be formalised by saying that we need to find a \emph{context} $D$: a term in $\syntax{\Sigma + \{\bullet:m\to n\}}$ with exactly one occurrence of $\bullet$, such that
%\begin{equation}
%\label{eq:match}
%c = D[l/\bullet]
%\end{equation}
%the rewrite then takes $c\Ra_\mathcal{R} c'$, where $c' = D[r/\bullet]$.
%
%\begin{lem}\label{lemma:rewriting}
%The rewriting relation can be characterised in a very
%simple way. Suppose that $u,v: n \to m$, then: $u \Ra_{\mathcal{R}} v $ iff
%$\exists \langle l,r \rangle :(i,j)\in\mathcal{R}, c1: n\to i+k, c_2: j+k \to n$ such that
%$$u = c_1 \mathrel{;} (l\oplus id_k) \mathrel{;}c_2 \,\wedge\, \\ v = c_1 \mathrel{;} (r \oplus id_k) \mathrel{;}c_2
%$$
%\end{lem}
%
%
%Diagrammatic reasoning can be seen as a special case of rewriting. Given a symmetric monoidal theory $(\Sigma,E)$
%we can obtain a rewriting system $\mathcal{R}_E$ by taking the symmetric closure of $E$:
%\[
%\mathcal{R}_E = \{\, \langle t,t'\rangle \,|\, (t,t') \in E \} \cup \{\, \langle t',t\rangle  \,|\, (t,t')\in E \,\}
%\]
%The following relates equality of arrows in the free prop on $(\Sigma,E)$ with rewriting in
%$\syntax{\Sigma}$.
%\begin{pro}\label{pro:diagrammaticreasoning}
%$t = t'$ in the symmetric monoidal theory $(\Sigma,E)$ iff
%there exists a finite chain of rewrite steps in $\mathcal{R}_E$, with each $t_i$ considered as
%syntax, i.e. an arrow of $\syntax{\Sigma}$.
%\[
%t=t_1\Ra t_2\Ra \dots\Ra t_k
%\]
%\end{pro}
%
%
%The tricky part---algorithmically speaking---is that in \eqref{eq:match} the $=$ means equal as arrows of $\syntax{\Sigma}$, i.e. modulo its symmetric monoidal structure. It's far from clear how to find matches, working with pure syntactic terms. To implement this, we need to develop a theory of rewriting modulo symmetric monoidal structure, along the lines of what already exists for rewriting modulo associativity, commutativity etc.
%This is the remit of this work.
%

SymMonDpoRewriting.tex
% -*- root: ../rewriting.tex -*-

In the general case, where there is no chosen special Frobenius structure, we can still use $\FTerm{\Sigma}$ for rewriting, but we need to careful about how we find \emph{legal}
contexts. For instance, the context in~\eqref{eq:multiplecontext-badoutcome} relies on the extra Frobenius structure being present.  %: those that respect the ordering imposed by composition.
%Indeed, we may be able to perform rewriting steps at the hypergraph level which are not allowed at the syntactic level. Here is a counterexample.

%What we do have is a completeness result, which still holds over from Theorem~\ref{thm:frobeniusrewriting}.
%
%\begin{cor}[Completeness]\label{cor:comp}
%Suppose that $\syntax{\Sigma}$ is a symmetric monoidal theory with a rewriting system $\mathcal{R}$.
%Then there exists a dpo system $\mathcal{D}$ satisfying:
%\[
%\text{if }c\Rightarrow_{\mathcal{R}}d \text{ then }\SynToCsp{c} \Rightarrow_{\mathcal{D}} \SynToCsp{d}.
%\]
%\end{cor}
%\begin{proof}
%It's the same one as defined in the proof of Theorem~\ref{thm:frobeniusrewriting}, and completeness
%follows by the same argument.
%\end{proof}
%
%The inverse (soundness) does not hold in general. A counterexample is the following.


%Intuitively, the problem with the above rewriting is that matching in $\FTerm{\Sigma}$ may happen in contexts which are not legal for matching in $\syntax{\Sigma}$. Another counterexample stems from Example~\ref{ex:unsoundcontext}: in there, \eqref{eq:multiplecontext-goodoutcome} can be mimicked by rewriting in $\syntax{\Sigma}$, while \eqref{eq:multiplecontext-badoutcome} cannot.

The remit of this section is to tailor a suitable restriction of DPO rewriting that adheres to rewriting for an SMT, just as generalised DPO rewriting corresponds to rewriting for an SMT with a chosen Frobenius structure (Theorem~\ref{thm:frobeniusrewriting}).


%\begin{exm}
%We would like to check equivalence of terms of the theory $(\Sigma_B, E_B)$ of non commutative bialgebras (Example \ref{exm:props}.\ref{ex:ncbialgebras}).
%First, we transform the equations in $E_B$ into a rewriting systems $\mathcal{R}_B$ by giving them a left to right orientation. Then we obtain the ground rewriting system  $\rewiring{\mathcal{R}_B}$ by bending each rule in $\mathcal{R}_B$ and, finally, we obtain the DPO system  $\Phi(\rewiring{\mathcal{R}_B})$ by translating via $\Phi$ diagrams into cospans of graphs. The resulting rewriting system is displayed in Figure \ref{fig:hopf}. In Section \ref{sec:terminationHopf}, we will show confluence and termination of $\Phi(\rewiring{\mathcal{R}_B})$ meaning that rewriting is effective to test equivalence with respect to $E_B$. However, first we need a rewriting procedure that is sound and complete with respect to rewriting in $\syntax{\Sigma_B}$ in isolation, without the extra Frobenius structure that is necessary for Theorem~\ref{thm:frobeniusrewriting}.
%\end{exm}


%We obviate to the problem of Example~\ref{ex:unsound} with the notion of \emph{convex} matching (Definition~\ref{def:convexmatching}). As we saw in Example~\ref{ex:unsoundcontext}, even a convex matching allows for the choice of multiple context: we introduce the notion of \emph{boundary complement} (Definition~\ref{def:boundarycomplement}) to mean a context that is sound for rewriting in $\syntax{\Sigma}$. Boundary complements are well-behaved: when they exist, they are uniquely defined up-to isomorphism (Theorem~\ref{thm:uniquenessBoundaryCompl}). A convex matching guarantees that a boundary complement can be always chosen when performing a dpo rewriting step. We call \emph{rigid} a dpo rewriting step with these properties (Definition~\ref{def:rigidDpoRewriting}). The main result of the section is the adequacy of rigid dpo rewriting for rewriting in an SMT (Theorem~\ref{th:adequacyRigidSMT}).

%Our diagnosis is that the problem lies in the generosity of matching in $\FTerm{\Sigma}$. We shall now characterise a certain family of matchings in $\FTerm{\Sigma}$ --- called \emph{sound}, see Definition~\ref{def:soundmatching} below, which mimic the more restrictive notion of matching in $\syntax{\Sigma}$.

\begin{comment}
SOUND CONTEXT REPLACED BY THE NOTION OF BOUNDARY COMPLEMENT


\marginpar{Pawel: I thought it's supposed to be mono only on the injections, since if we impose mono tout court then we can't do identity}
We call \emph{context} a morphism $i+j \tr{p} C \tl{q} n+m$ of $\FTerm{\Sigma}$ in which both $p$ and $q$ are mono. For such $C$, we partition nodes in the image of $p$ and $q$ as follows. The set $\linp{C}$ of \emph{left inputs} is the $p$-image of $j$ and the set \emph{right inputs} $\rinp{C}$ is the $q$-image of $m$. The set $\inp{C}$ of \emph{inputs} is the union of $\linp{C}$ and $\rinp{C}$. Similarly, we write $\lout{C}$ for the $p$-image of $i$ (the \emph{left outputs}), $\rout{C}$ for the $q$-image of $n$ (\emph{right outputs}) and $\out{C}$ for their union, the set of \emph{outputs}.
%For such $D$, we write $\inp[j]{D}$ for the $p$-image of $j$ and $\inp[m]{D}$ for the $q$-image of $m$. The set $\inp{D}$ of \emph{input} nodes is the union of $\inp[i]{D}$ and $\inp{D}$. Similarly, we write $\out[i]{D}$ for the $p$-image of $i$, $\out[n]{D}$ for the $q$-image of $n$ and $\out{D}$ for their union, the set of \emph{output} nodes. %For such $D$, we define the set $\inp{D}$ of \emph{input} nodes as the union of the $p$-image of $j$ and the $q$-image of $m$. Similarly, we write $\out{D}$ for the set of \emph{output} nodes --- the union of the $p$-image of $i$ and the $q$-image of $n$.

\begin{defn}[Sound context]
A context $i+j \tr{p} C \tl{q} n+m$ is \emph{sound} if the following three conditions hold:
\begin{itemize}
\item $C$ is acyclic.
\item $C$ is \emph{monogamous}, that means, for all nodes $v$ of $C$,
\begin{eqnarray*}
\text{the number of hyperedges with source $v$ is }& \begin{cases} 0 &\mbox{if } v \in \out{D} \\
1 & \mbox{otherwise} \end{cases}  \\
\text{the number of hyperedges with target $v$ is }& \begin{cases} 0 &\mbox{if } v \in \inp{D} \\
1 & \mbox{otherwise.} \end{cases}
\end{eqnarray*}
\item $C$ is \emph{left-feedback free}, that means, given $v \in \linp{D}$ and $v' \in \lout{C}$, there is no path from $v$ to $v'$.
\end{itemize}
\end{defn}

\begin{lem} If $i+j \tr{p} C \tl{q} n+m$ is a sound context, then there exist a number $k$ and diagrams $c_1 \: i+k \to n$ and $c_2 \: k+j \to m$ in $\syntax{\Sigma}$ such that
$$ i+j \tr{p} C \tl{q} n+m \qquad \mapsto \qquad
\lower12pt\hbox{$\includegraphics[height=1.2cm]{graffles/SplittedContext.pdf}$}$$
under the isomorphism $\FTerm{\Sigma} \cong \syntax{\Sigma} + \frob$.
\end{lem}
\begin{proof}
Monogamicity and aciclycity allows us to assign a ranking to $C$ such that XXXXX ... furthermore, left-feedback freedom implies that
\end{proof}
\end{comment}
Before the formal developments, let us sketch the intuition. Given a rewriting system $\mathcal{R}$, we are interested in the shape of contexts for $\rewiring{\mathcal{R}}$-rewriting in $\syntax{\Sigma}+\frob \cong \FTerm{\Sigma}$ that ``look like'' legal contexts for $\mathcal{R}$-rewriting in $\syntax{\Sigma}$. By Lemma~\ref{lem:frobeniusground}, a generic context in $\syntax{\Sigma}+\frob$ for a rule $\rrule{\rewiring{l}}{\rewiring{r}}$ has shape
\[ \cgr{LcontextC.pdf} \]
Now, this context corresponds to a legal one in $\syntax{\Sigma}$ only when we can find $c_1$, $c_2$ in $\syntax{\Sigma}$ such that
\begin{equation}\label{eq:goodcontext} \cgr{contextC.pdf} = \cgr{SplittedContext.pdf}.\end{equation}%\cgr{SplittedContext.pdf}
Indeed, in that case, we are in presence of the bent version of a legal context in $\syntax{\Sigma}$ for rule $\rrule{l}{r}$ (cf. \eqref{eq:rewd}):
\[ \cgr{rewd4.pdf} \ =\  \cgr{rewd2.pdf}\]
% \begin{eqnarray*}
%  \cgr{rewd4.pdf} & =& \cgr{rewd3.pdf} \\
%   & =& \cgr{rewd2.pdf}
%   \end{eqnarray*}

%\medskip

Our task is to characterise legal contexts like~\eqref{eq:goodcontext}. We proceed in two steps. First, we introduce the notion of \emph{boundary complement} (Definition~\ref{def:boundarycomplement}), which rests on monogamicity (Definition~\ref{def:monogamous}). It clarifies the role that interfaces $i,j,m,n$ play in the legal context~\eqref{eq:goodcontext}: $j$, $n$ serve as inputs and $i$, $m$ serve as outputs of its un-bent version. Contrary to arbitrary contexts in $\FTerm{\Sigma}$ (\emph{cf.} Example~\ref{ex:unsoundcontext}), boundary complements are uniquely defined up-to iso when they exist (Proposition~\ref{thm:uniquenessBoundaryCompl}).
%
The second notion is \emph{convex} matching (Definition~\ref{def:convexmatching}),
%It completes the characterisation of legal contexts~\eqref{eq:goodcontext} by
which enforces that the only communication between $c_1$ and $c_2$ happens along the interface $k$, \emph{cf}~\eqref{eq:goodcontext}.

A convex matching always allows to pick a (unique) boundary complement as context: we call this situation a \emph{convex} a DPO rewriting step (Definition~\ref{def:rigidDpoRewriting}). The main result of the section is the adequacy of convex DPO rewriting for rewriting in an SMT (Theorem~\ref{th:adequacyRigidSMT}).

\begin{defn}[Boundary complement] \label{def:boundarycomplement}
    For monogamous cospans $i \xrightarrow{a_1} L \xleftarrow{a_2} j$ and $n \xrightarrow{b_1} G \xleftarrow{b_2} m$,
    and a mono $f : L \to G$, a pushout complement as $(\dagger)$ below
    \[ \xymatrix@C=50pt@R=20pt{
        L \ar[d]_f \ar@{}[dr]|{(\dagger)} & {i + j} \ar[l]_{a := [a_1,a_2]}
              \ar[d]^{c := [c_1,c_2]}
        \ar@{}[dl]|(.8){\text{\large $\urcorner$}}
         \\
       G & L^\perp \ar[l]^{g} \\
       & n+m \ar[ul]^{[b_1,b_2]} \ar@{-->}[u]_{[d_1,d_2]}
       } \]
    is called a \textit{boundary complement} if $c$ is mono and there exists $d_1\: n\to L^\perp$ and $d_2\: m \to L^\perp$, making the above triangle commute, such that
    \begin{equation}\label{eq:boundary} j+n \xrightarrow{[c_2,d_1]} L^\perp \xleftarrow{[c_1,d_2]} m+i \end{equation}
    is a monogamous cospan.
\end{defn}

%
%\begin{defn}[Boundary complement] \label{def:boundarycomplement}
%    For a monogamous cospans:
%    \[ i \xrightarrow{a_1} L \xleftarrow{a_2} j \qquad
%       m \xrightarrow{} G \xleftarrow{} n \]
%    and a mono $f : L \to G$, a pushout complement of the form:
%    \[ \xymatrix@C=50pt{
%        i + j \ar[r]^{a := [a_1,a_2]}
%              \ar[d]_{b}
%        \ar@{}[dr]|(.8){\text{\large $\ulcorner$}}
%        &
%        L \ar[d]^f \\
%        L^\perp \ar[r]^{g} & G \\
%       } \]
%    is called a \textit{boundary complement} if $b$ is mono, and there exists a monogamous cospan:
%    \[ m' \xrightarrow{c_1} L^\perp \xleftarrow{c_2} n' \]
%    and some $h_1,h_2$ such that:
%    % \[ \xymatrix@C=40pt{
%    %     (n + j) + (m + i) \ar[dr]_{[c_2,c_1]} & i + j \ar[d]_{b} \ar[l>]_{h_1 + h_2} \\
%    %                               & L^\perp \\
%    %    } \]
%    \begin{equation}\label{eq:polarity}
%        \xymatrix@C=40pt{
%            n' + m' \ar[dr]_{[c_2,c_1]} & i + j \ar[d]_{b} \ar[l]_{\ \ \ h_1 + h_2} \\
%                                        & L^\perp \\ }
%    \end{equation}
%\end{defn}


\begin{pro}\label{thm:uniquenessBoundaryCompl}
    Boundary complements in $\Hyp{\Sigma}$ are unique, when they exist.
\end{pro}

As mentioned, the notion of boundary complement does not tell the whole story about which matches in $\FTerm{\Sigma}$ are legal in $\syntax{\Sigma}$. The missing requirement is that $c_1^{\star}$ and $c_2$ in~\eqref{eq:goodcontext} can only communicate through interface $k$, which connects outputs of $c_1$ to inputs of $c_2$. The following counterexample shows that, even in presence of a boundary complement, linking outputs of $c_2$ to inputs of $c_1$ may still yield an illegal rewriting step in $\syntax{\Sigma}$.

\begin{exm}\label{ex:unsound} Fix $\Sigma = \{ e_1 \: 2 \to 1, {e_2 \: 1 \to 2}, {e_3 \: 1 \to 1} , \\ e_4 \: 1 \to 1\}$ and consider the following rewriting rule in $\syntax{\Sigma}$.
\begin{eqnarray}
         \rrule{\lower9pt\hbox{$\includegraphics[height=.6cm]{graffles/unsoundSynL.pdf}$}\ \ }{\lower9pt\hbox{\ \ $\includegraphics[height=.7cm]{graffles/unsoundSynRSwap.pdf}$}} \: (2,2) \label{eq:counterexSoundness1} \end{eqnarray}
         Left and right side are interpreted in $\FTerm{\Sigma}$ as cospans
        \begin{eqnarray*}
         2 \tr{} \cgr[height=.6cm]{unsoundHypLround.pdf} \tl{} 2 & \!\!\!\!\! & 2 \tr{}  \cgr[height=.7cm]{unsoundHypRroundSwap.pdf} \tl{} 2.
         \end{eqnarray*}
We introduce another diagram $c \: 1\to 1$ in $\syntax{\Sigma}$ and its interpretation in $\FTerm{\Sigma}$:
                        \begin{equation*}\label{eq:counterexSoundness3}
                         \xymatrix@=10pt{
                        \lower7pt\hbox{$\includegraphics[height=.6cm]{graffles/unsoundSynM.pdf}$}\quad \ar@{|->}[rr]^-{\SynToCsp{\cdot}} && \ \
                        1 \tr{} \lower7pt\hbox{$\includegraphics[height=.6cm]{graffles/unsoundHypMround.pdf}$} \tl{} 1.
                        }
          \end{equation*}
         Now, the left-hand side of the rule \eqref{eq:counterexSoundness1} cannot match in $c$. However, their interpretation yields a DPO rewriting step in $\FTerm{\Sigma}$ as below, where $f$ maps grey nodes to grey nodes.
         \begin{eqnarray*}%\label{eq:counterexSoundness4}
         \xymatrix@=15pt{
         {\cgr[height=.8cm]{unsoundHypLgreyround.pdf} } \ar[d]_{f} & \ar[l] 2+2 \ar[d] \ar[r] & {\cgr[height=.8cm]{unsoundHypRroundSwap.pdf}} \ar[d]
         %& {\text{\Large $\Rightarrow$}} & \lower9pt\hbox{$\includegraphics[height=.8cm]{graffles/unsoundHypR.pdf}$}
          \\
         {\cgr[height=.95cm]{unsoundHypMLgreyround.pdf}}  & \ar[l] {\cgr[height=.7cm]{context-e3-dots.pdf}} \ar[r] & {\cgr[height=.45cm]{unsoundHypMRround.pdf}}
         }
         \end{eqnarray*}
         Observe that the leftmost pushout above \emph{is} a boundary complement: the input-ouput partition is correct. Still, mimicking this rewriting step in $\syntax{\Sigma}$ fails because the context does not fit the legal shape~\eqref{eq:goodcontext}. This is best evident by showing how matching in $\SynToCsp{c}$ appears under the isomorphism $\FTerm{\Sigma} \cong \syntax{\Sigma} + \frob$:
          \begin{eqnarray*}
          {\cgr[height=1.5cm]{nonconvexcontextL.pdf}} \dfop {\cgr[height=1.2cm]{nonconvexcontextR.pdf}}
          \end{eqnarray*}
          The diagrams $l$, $c_1$ and $c_2$ on the right side are defined in terms of the dotted squares on the right. The difference with the prescription of~\eqref{eq:goodcontext} is apparent: the topmost output interface of $c_2$ connects to the bottommost input interface of $c_1$. For this reason, we cannot un-bend our context to obtain a legal matching in $\syntax{\Sigma}$.
\end{exm}

In order to rule out situations~\eqref{eq:counterexSoundness1} and complete the characterisation of legal contexts like~\eqref{eq:goodcontext}, we recover the notion of convexity (Def.~\ref{def:convexsubhyp}) to introduce \emph{convex} matchings. The intuition is that a convex matching cannot leave ``holes'' as $f$ does in Example~\ref{ex:unsound}.

\begin{defn}[Convex matching] \label{def:convexmatching}
We call $m : L \to G$ in $\Hyp{\Sigma}$ a \textit{convex matching} if it is mono and its image is convex.
\end{defn}

% \begin{defn}
%     A \textit{ranking} of a hypergraph $G$ is a function $R : V_G \to \mathbb N$ such that for all hyperedges $h$, $R(s_i(h)) < R(h) < R(s_j(h))$. %$R(h) \leq R(h')$ implies that there exists no node $v$ such that $s(h) = v$ and $t(h') = v$.
%     Let $G_R[i,j]$ be the full sub-hypergraph of $G$ whose nodes have $i \leq R(v) \leq j$.
% \end{defn}

%Note that $G_R[i,j]$ need not be defined for all $i, j$.

% \begin{lem}\label{lem:interval-partition}
%     Let $m \rightarrow G \leftarrow n$ be a cospan in $\syntaxgr{\Sigma}$. For any ranking $R$ of $G$ with $\max{R} = j$, and $i < j$, the subgraphs $G_R[0,i]$ and $G_R[i+1,j]$ extend to cospans in $\syntaxgr{\Sigma}$:
%     \[ m \rightarrow G_R[0,i] \leftarrow p \qquad
%        p \rightarrow G_R[i+1,j] \leftarrow n \qquad \]
%     in such a way that:
%     \[ G = (G_R[0,i] \tns id_{p'}) \poi (id_{p''} \tns G_R[i+1,j]) \]
%     for some subsets $p',p''$ of $p$.
% \end{lem}


% \begin{lem}
%     Let $m \rightarrow G \leftarrow n$ be a cospan in $\syntaxgr{\Sigma}$ and $H$ a convex sub-hypergraph. Then for any ranking $R$, every sub-hypergraph of the form $G_R[i,j]$ induces a cospan such that:
%     \begin{equation}\label{eq:snd-factor}
%         G = C_1 \poi (id_p \tns G_R[i,j]) \poi C_2
%     \end{equation}
% \end{lem}

% \begin{proof}
%     Let $C_1$ be the full sub-hypergraph of $G$ consisting of the inputs of $G$ and nodes of rank $R(v) \leq i$. Similarly, let $C_2$ be the smallest sub-hypergraph consisting of outputs and nodes where $R(v) \geq j$. The three hypergraphs $C_1, C_2$ and $G_R[i,j]$ thus contain precisely the same hyperedges as $G$. They also contain the same nodes, but with some duplication. Let $p := V_{C_1} \cap V_{C_2}$, let $m' := V_{C_1} \cap G_R[i,j]$, and let $n' := G_R[i,j] \cap V_{C_2}$. By monogamy, it is impossble for a single node to be adjacent to 3 hyperedges, so these three sets are disjoint. The colimit of the following diagram:
%     \[ m \rightarrow C_1 \leftarrow p + m'
%          \rightarrow p + G_R[i,j] \leftarrow p + n'
%          \rightarrow C_2 \leftarrow n \]
%     identifies two nodes if and only if they correspond to the same node in $G$. Hence, the result is $G$ itself. Each of the three cospans is acyclic, because $G$ is. The only way they could not be monogamous is if the target of a hyperedge occurs as an input or a source as an output, but the ranking $R$ forbids this. Hence the cospans can be regarded as morphisms in $\syntaxgr{\Sigma}$, and the colimit of the diagram above amounts to the composition \eqref{eq:snd-factor}.
% \end{proof}


% \begin{lem}\label{lem:convex-interval}
%     For any convex subgraph $H$ of $G$, there exists a ranking of $G$ such that $H \cong G_R[i,j] \otimes S$ for some scalar $S$ and $i,j$.
% \end{lem}

% \begin{proof}
%     Define the ranking $R$ as follows. First, split the nodes of $G$ into three parts. $V_1$ consists of the nodes which have at least one path to a node in $H$ (and not in $H$). Let $V_2$ be the nodes in $H$, and let $V_3$ be the rest. Let $R_1$, $R_2$, and $R_3$ be rankings on the associated full sub-hypergraphs and let:
%     \[
%         R(v) = \begin{cases}
%             R_1(v) & \textrm{ if } v \in V_1 \\
%             R_2(v) + \max{R_1} + 1 & \textrm{ if } v \in V_2 \\
%             R_3(v) + \max{R_1} + \max{R_2} + 1 & \textrm{ if } v \in V_3
%         \end{cases}
%     \]
% \end{proof}

%EXPLAIN THE SIGNIFICANCE OF THE NEXT LEMMA

The importance of the above notion is best revealed by Lemma~\ref{lemma:convexfact} and Theorem~\ref{thm:charactImage}: given a convex matching, it is always possible to recover the appropriate context in $\syntax{\Sigma}$. We now combine the notions of boundary complement and of convex matching to tailor a family of DPO rewriting steps which only yield legal $\syntax{\Sigma}$-rewriting.

\begin{defn}[Convex DPO rewriting step] \label{def:rigidDpoRewriting} Let $\mathcal{R}$ be a DPO rewriting system. A \emph{convex} DPO rewriting step
\begin{eqnarray*}
\vcenter{\xymatrix@R=-2pt@C=22pt{ & D& \\ 0 \ar[ur] && \ar[ul]_{[q_1,q_2]} n+m}} & \rigidDPOstep{\mathcal{R}} & \vcenter{\xymatrix@R=-2pt@C=22pt{ & E & \\ 0 \ar[ur] && \ar[ul]_{[p_1,p_2]} n+m}}
\end{eqnarray*}
%$$\left(0 \tr{} D \tl{[q_1,q_2]} n+m \right) \rigidDPOstep{\mathcal{R}} \left(0 \tr{} E \tl{[q_1,q_2]} n+m \right)$$
happens when there is a rule $L \xleftarrow{[a_1,a_2]} i+j \xrightarrow{[b_1,b_2]} R$ in $\mathcal{R}$ such that the following diagram in $\Hyp{\Sigma}$ commutes, the two squares are pushouts
\begin{equation}\label{eq:dpo3}
\raise25pt\hbox{$
\xymatrix@R=15pt@C=20pt{
L \ar[d]_{f}   &  i+j \ar[d]
 \ar@{}[dl]|(.8){\text{\large $\urcorner$}}
 \ar@{}[dr]|(.8){\text{\large $\ulcorner$}}
 \ar[l]_{[a_1,a_2]} \ar[r]^{[b_1,b_2]}  & R \ar[d] \\
 D &  C \ar[l] \ar[r]  & E \\
&  n+m \ar[u] \ar[ur]_{[p_1,p_2]}  \ar[ul]^{[q_1,q_2]}
}$}
\end{equation}
 and the following two restrictions hold:
 \begin{itemize}
 \item $f \: L \to G$ is a convex matching;
 \item in the leftmost pushout $i+j \to C$ is a boundary complement.
\end{itemize}
\end{defn}
Note that the relation $\rigidDPOstep{\mathcal{R}}$ is contained in $\DPOstep{\mathcal{R}}$ (Definition~\ref{defn:dpo}), the difference being that the leftmost pushout has to rest on a convex matching and a boundary complement.

We have now all the ingredients to prove the adequacy of convex DPO rewriting with respect to rewriting in $\syntax{\Sigma}$.

\begin{thm}\label{th:adequacyRigidSMT}Let $\mathcal{R}$ by any rewriting system  on $\syntax{\Sigma}$. Then, % containing a rule $\rrule{l}{r} \: (i,j)$.%the following are equivalent.
\begin{eqnarray*} d\Rightarrow_{\mathcal{R}}e & \Leftrightarrow & \Phi(\rewiring{d}) \rigidDPOstep{\Phi(\rewiring{\mathcal{R}})} \Phi(\rewiring{e}).\end{eqnarray*}
%\begin{enumerate}[label=(\alph*)]
%\item $d\Rightarrow_{\mathcal{R}}e$ is a rewriting step obtained by application of $\rrule{l}{r}$.
%\item $\Phi(\rewiring{d}) \DPOstep{\Phi(\rewiring{\mathcal{R}})} \Phi(\rewiring{e})$ is a rigid dpo rewriting step obtained by application of $\rrule{\Phi(\rewiring{l})}{\Phi(\rewiring{r})}$.
%\end{enumerate}
\end{thm}
\begin{proof} For the only if direction, by Theorem~\ref{thm:frobeniusrewriting} $d\Rightarrow_{\mathcal{R}}e$ implies $\Phi(\rewiring{d}) \DPOstep{\Phi(\rewiring{\mathcal{R}})} \Phi(\rewiring{e})$. It is not hard to verify that the argument actually constructs a \emph{convex} DPO rewriting, thus yielding the desired statement. The reader may consult Appendix~\ref{app:proofs} for details.


We now turn to the converse direction. Let %Let $\Phi(\rewiring{d})$ be a cospan $0 \tr{} D \tl{[q_1,q_2]} n+m$ and $\Phi(\rewiring{e})$ a cospan $0 \tr{} E \tl{[p_1,p_2]} n+m$
\begin{eqnarray*}
\Phi(\rewiring{d}) \dfop \vcenter{\xymatrix@R=5pt@C=3pt{ & D& \\ 0 \ar[ur] && \ar[ul]_{[q_1,q_2]} n+m}} & & \Phi(\rewiring{e}) \dfop \vcenter{\xymatrix@R=5pt@C=3pt{ & E & \\ 0 \ar[ur] && \ar[ul]_{[p_1,p_2]} n+m}}.
\end{eqnarray*}
Our assumption gives us a diagram as in~\eqref{eq:dpo3}, with application of a rule $\rrule{\Phi(\rewiring{l})}{\Phi(\rewiring{r})}$ in $\Phi(\rewiring{\mathcal{R}})$. We now want to show that $d\Rightarrow_{\mathcal{R}}e $ with rule $\rrule{l}{r}$, say of type $(i,j)$. Now, because $n \tr{q_1} D \tl{q_2} m = \SynToCsp{d}$, it is monogamous directed acyclic by Theorem~\ref{thm:charactImage}. Since the matching $f \: L \to D$  in~\eqref{eq:dpo3} is convex, Lemma~\ref{lemma:convexfact} yields a decomposition of $n \tr{q_1} D \tl{q_2} m$ in terms of monogamous directed acyclic cospans:
\begin{equation*}%\label{eq:pathFact}
\left( n \tr{} C_1 \tl{} i\!+\!k \right) \poi\!\!\!
\begin{array}{cc}
\left( k \tr{id} k \tl{id} k \right)\\
\tns \\
\left( i \tr{} L \tl{} j \right)
\end{array}
\!\!\!\poi
\left( j\!+\!k\tr{} C_2 \tl{} m \right).
\end{equation*}
Applying again Theorem~\ref{thm:charactImage} we obtain $c_1$, $c_2$ in $\syntax{\Sigma}$ such that
\begin{align*}
\SynToCsp{c_1} = n\tr{} C_1 \tl{} i+k \qquad \SynToCsp{c_2} = j+k\tr{} C_2 \tl{} m.
\end{align*}
By functoriality of $\SynToCsp{\cdot}$, $\SynToCsp{d} = \SynToCsp{c_1 \poi (id \tns l) \poi c_2} $ and, since $\SynToCsp{\cdot}$ is a faithful prop morphism, $d = c_1 \poi (id \tns l) \poi c_2$. Thus we can apply the rule $\rrule{l}{r}$ on $e$, which yields $e = c_1 \poi (id \tns r) \poi c_2$ such that $d \Ra_{\mathcal{R}} e$. We can conclude that $\SynToCsp{e} = n\tr{p_1} E \tl{p_2} m$ because boundary complements are unique (Proposition~\ref{thm:uniquenessBoundaryCompl}).
\end{proof}

\begin{comment}
\begin{thm}[Completeness]\label{thm:compl} Let $\Sigma$ be a signature and $\mathcal{R}$ be a rewriting system on $\syntax{\Sigma}$ containing a rule $\rrule{l}{r}$. Fix $\SynToCsp{c} = n\tr{q_1} G \tl{q_2} m$, $\SynToCsp{l} = i \tr{a_1} L \tl{a_2} j$, $\SynToCsp{r} = i \tr{b_1} R \tl{b_2} j$ and $\SynToCsp{d} = n\tr{p_1} D \tl{p_2} m$.
 Suppose that $c\Rightarrow_{\mathcal{R}}d$ via $\rrule{l}{r}$. Then there exists a convex DPO rewriting step $G \DPOstep{\mathcal{R}} D$ applying the DPO rule $L \tl{} i+j \tr{} R$.
\end{thm}
\begin{proof}

\end{proof}

\begin{thm}[Soundness]\label{thm:sound}
Let $\Sigma$ be a signature and $\mathcal{R}$ be a rewriting system on $\syntax{\Sigma}$ containing a rule $\rrule{l}{r}$. Fix $\SynToCsp{c} = n\tr{q_1} G \tl{q_2} m$, $\SynToCsp{l} = i \tr{a_1} L \tl{a_2} j$, $\SynToCsp{r} = i \tr{b_1} R \tl{b_2} j$ and suppose that $G \DPOstep{\mathcal{R}} D$ is convex DPO rewriting step applying the DPO rule $L \tl{} i+j \tr{} R$.%Suppose that $L \tr{f} G$ is a convex matching with boundary complement $i+j \tr{h}L^\perp$ given by Lemma~\ref{??}.
\begin{equation}\label{eq:soundness_dposystem}
\raise25pt\hbox{$
\xymatrix@R=30pt@C=20pt{
L \ar@{_(->}[d]_f   &  i+j \ar@{_(->}[d]^g
\ar@{}[dl]|(.5){(\text{PO})}
\ar@{}[dr]|(.5){(\text{PO})}
\ar[l]_{[a_1, a_2]} \ar[r]^{[b_1, b_2]}  & R \ar@{_(->}[d]^h \\
 G &  L^\perp \ar[l] \ar[r]  & D \\
&  n+m \ar[u] \ar[ur]_{[p_1, p_2]}  \ar[ul]^{[q_1, q_2]}
}$}.
\end{equation}
Then there exists $d \: n \to m$  in $\syntax{\Sigma}$ such that $\SynToCsp{d} = n\tr{p_1} D \tl{p_2} m$ and $c\Rightarrow_{\mathcal{R}}d$ via $\rrule{l}{r}$.
\end{thm}
\begin{proof}
As $G \DPOstep{\mathcal{R}} D$ is convex, the matching $f \: L \to D$ is convex; then Lemma~\ref{lemma:convexfact} gives us
\begin{align*}
\SynToCsp{c_1} = n\tr{} C_1 \tl{} i+k \qquad \SynToCsp{c_2} = j+k\tr{} C_2 \tl{} m
\end{align*}
such that the following decomposition holds.
\begin{equation}\label{eq:pathFact}
\left( n \tr{} C_1 \tl{} i\!+\!k \right) \poi\!\!\!
\begin{array}{cc}
\left( k \tr{id} k \tl{id} k \right)\\
\tns \\
\left( i \tr{} L \tl{} j \right)
\end{array}
\!\!\!\poi
\left( j\!+\!k\tr{} C_2 \tl{} m \right)
\end{equation}
 \fznote{Completeness should be reinforced by said that the DPO step is convex}
By functoriality of $\SynToCsp{\cdot}$, $\SynToCsp{c} = \SynToCsp{c_1 \poi (id \tns l) \poi c_2} $ and, since $\SynToCsp{\cdot}$ is a faithful prop morphism, $c = c_1 \poi (id \tns l) \poi c_2$. Thus we can apply the rule $\rrule{l}{r}$ on $c$, which yields $d = c_1 \poi (id \tns r) \poi c_2$ such that $c \Ra_{\mathcal{R}} d$. By Corollary~\ref{cor:comp} we then have a convex rewriting step $\SynToCsp{c} \Ra_{\mathcal{D'}} \SynToCsp{d}$ for a DPO system $\mathcal{D'}$ (\emph{cf.} Definition~\ref{defn:dpo}). Now, $\mathcal{D'}$ must be the same DPO-system as the one in \eqref{eq:soundness_dposystem}, because boundary complements are unique (Theorem~\ref{thm:uniquenessBoundaryCompl}).
 Therefore, $\SynToCsp{d} = n\tr{q_1} D \tl{q_2} m$.
\end{proof}
\end{comment} 
terminationHopf-old.tex



\bR XXXXXXXXXX \e

Let $\mathcal C = \{ C_k \}$ be the set of maximal connected sub-hypergraphs consisting just of $\nu$-hyperedges, and for any path $p$, let $\mathcal C[p] \subseteq \mathcal C$ be the subset consisting just of those $C_k$ which contain a hyperedge from $p$. Then, let:
\[ l_{\mathcal C}(p) := \sum_{C \in \mathcal C[p]} |C| \]
and let the $\mathcal C$-distance from a hyperedge $h$ to a sub-hypergraph $H$ be:
\[ d_{\mathcal C}(h,H) := \max_{p\in\textrm{paths}(h,H)} l_{\mathcal C}(p) \]

For $\textrm{sink}(G)$ be the smallest sub-hypergraph of $G$ containing all outputs and hyperedges of type $\eta$, fix the following sets of hyperedges:
\begin{align*}
  \overline{\mu_k} & := \{ h \ :\  \tau(h) = \mu, d_{\mathcal C}(h, \sink{G}) = k\} \\
  \overline{\nu} & := \{ h \ :\  \tau(h) = \nu \} \\
  \overline{\eta} & := \{ h \ :\  \tau(h) = \eta \} \\
  \overline{\epsilon} & := \{ h \ :\  \tau(h) = \epsilon \} \\
\end{align*}

Let $\leq_{\mathcal C}$ be lexicographic ordering given by:
\[ [\,|\overline{\mu_k}|, |\overline{\mu_{k-1}}|, \ldots, |\overline{\mu_1}|, |\overline{\nu}|, |\overline{\eta}|, |\overline{\epsilon}|\,] \]

\begin{lem}
  The rules {\rm $\HC{j}$} and their converse rules are non-increasing in $\leq_{\mathcal C}$.
\end{lem}

\begin{proof}
  Clearly these rules leave the number of hyperedges of each type fixed, so we only need to show that the numbers $|\overline{\mu_k}|$ remain unchanged.

  We now show that for all $\mu$-hyperedges $h$, that its $\mathcal C$-distance can only decrease. First, consider any $\mu$-hyperedge $h$ not in the image of the LHS of \HC{j}. Then, if the path $p$ with minimal $l_{\mathcal C}(p) = k$ does not pass through the LHS of \HC{j}, $l_{\mathcal C}(p)$ is unchanged. Otherwise, it must enter an input of the LHS and exit an output. Consider the contribution to $l_{\mathcal C}(p)$ of the LHS and RHS of each rule for every input/output pair. For \HC{1} and \HC{3}, it is always zero, for \HC{4} it is always 1, and for \HC{2} it is always 2. Hence, if $h$ is not in the image of the LHS, for every $p$ to $\sink{G}$, there must be a corresponding $p'$ to $\sink{G}$ such that $l_{\mathcal C}(p) = l_{\mathcal C}(p')$.

  Now, consider $\mu$-hyperedges in the image of the LHS. The image of the LHS of \HC{1} contains two $\mu$-hyperedges, each with the same $\mathcal C$-distance $k$. Since any path to $\sink{G'}$ must travel through the unique output, the two $\mu$-hyperedges on the RHS also both have $\mathcal C$-distance $k$. Similarly, the $\mathcal C$-distance of the unique $\mu$-hyperedge in \HC{3} remains unchanged, and the remaining rules don't contain $\mathcal C$-hyperedges.

  Hence the rules \HC{j} are non-increasing in $\leq_{\mathcal C}$, and by symmetry, so too are their converses.
\end{proof}

\begin{lem}
  The rules {\rm $\HR{j}$} are strictly decreasing in $\leq_{\mathcal C}$.
\end{lem}


\bR XXXXXX \e





\bR XXXXXX \e

We now turn out attention to a particular rewrite system, namely the system of commutative and cocommutative Hopf algebras (with trivial antipode) given in Fig.~\ref{fig:hopf}.

\begin{defn}
  A maximal path $p$ in $G$ is a path such that if any path $p'$ contains all of the hyperedges in $p$, then $p = p'$. Let $\mathcal P(G)$ denote the set of all maximal paths.
\end{defn}

For any maximal path $p$ in $G$, let $d(G,p)$ be the number of maximal paths in $G$ that share at least one vertex with $p$ (including $p$ itself). Let:
\[ d(G) := \sum_{p \in \mathcal P(G)} d(G,p) \]
Note paths are being counted multiple times. For example, the LHS of the bialgebra rule has 4 maximal paths, and each of these four paths shares a vertex with all 4 paths, so $d(G) = 16$.

% We extend this to a pre-ordering on hypergraphs in the obvious way:
% \[
% G \geq_d H \Leftrightarrow d(G) \geq d(H)
% \]

\begin{defn} \rm
  A pair of cospans:
  \[ n \rightarrow L \leftarrow m \qquad n \rightarrow R \leftarrow m \]
  has a \textit{path-splitting} if there exists an injection $\phi : \mathcal P(G') \to \mathcal P(G)$ with the following properties:
  \begin{enumerate}
    \item $p$ starts at an input $v$ iff $\phi(p)$ starts at an input $v \in n$
    \item $p$ terminates at an output $v$ iff $\phi(p)$ terminates at an output $v \in m$
    \item if $p$ and $p'$ share a hyperedge, then so too do $\phi(p)$ and $\phi(p')$
  \end{enumerate}
\end{defn}

\begin{lem}
  If there exists a 
\end{lem}


% \begin{lem}
%   If there exists a path-splitting $\phi : H \to G$ then $G \geq_d H$.
% \end{lem}


\begin{lem}
  $\geq_p$ is reflexive, transitive, and well-founded.
\end{lem}

\begin{proof}
  Reflexivity and transitivity are immediate, so suppose $G \geq_p G'$ and $G' \not\geq_p G$. Then, either $G'$ has fewer maximal paths than $G$ or their must be at least one pair of paths in $G$ such that $p, p'$ do not share a hyperedge, but $\phi(p), \phi(p')$ do. Hence any infinite descending chain:
  \[ G >_p G_1 >_p G_2 >_p \ldots \]
  would require infinitely many maximal paths in $G$ to share at least one hyperedge, which is not possible.
\end{proof}


\begin{thm}
  $\geq_p$ is a reduction order. That is, if $G \DPOstep{\mathcal{R}} H$ by applying a rule:
  \[ L \leftarrow n + m \rightarrow R \]
  then:
  \[ L \geq_p R \iff G \geq_p H \]
\end{thm}

\begin{proof}
  Clearly any path-splitting from $H$ to $G$ restricts .
  First, we show this path-splitting lifts to a path-splitting $\widetilde\phi : \mathcal P(H) \rightarrow \mathcal P(G)$ in the following way. Either a path $p$ contains no hyperedges from $R$, in which case let $\widetilde\phi(p) = p$, otherwise it factors into three parts:
  \[ p = [h_1, \ldots h_i, h'_1, \ldots, h'_j, h''_1, \ldots, h''_k]  \]
  where $h'_l \in E_R$ and $h_l, h''_l \in E_H \backslash E_R$. Then, $h_i$ is connected to $h'_1$ via an input of $R$ and $h_j'$ to $h_1''$ via an output. Hence, let:
  \[ \widetilde\phi(p) := [h_1, \ldots h_i] + \phi([h'_1, \ldots, h'_j]) + [h''_1, \ldots, h''_k] \]
  which indeed gives a path in $G$. Furthermore, $\widetilde\phi$ is an injection.
\end{proof}

% Maximal paths start at a unit or an input and terminate at a counit or an output. Let $d(G)$ be the number of duplicate maximal paths and $p(G)$ be the number of all maximal paths. Let $\leq_{d,p}$ be the lexicographic order from $(d,p)$.

\begin{pro}
  The Hopf algebra congruences (assoc, coassoc, commute, cocommute) are non-increasing in $\leq_{d}$.
\end{pro}

\begin{proof}
  All of these rules have exactly one path connecting each input/ouput pair on their LHS and their RHS. Hence applying the rewrite induces a bijection between the old paths $p$ in $G$ and new paths $p'$ in $G[L\Rightarrow R]$. For a pair of paths $p,q$, suppose $p$ and $q$ are not duplicating. Then neither of the paths can be in the image of $L$, and hence $p'$ and $q'$ are not duplicating. Thus $d(G,p) \leq d(G[L\Rightarrow R],p')$. Since the total number of paths is preserved, $d(G) \leq d(G[L\Rightarrow R])$.
\end{proof}

\begin{pro}
  The Hopf algebra reductions (copy, cocopy, unit, counit, bone, bialg, hopf) are strictly decreasing in $\leq_{d}$.
\end{pro}

\begin{proof}
  (sketch/incomplete) All of these rules locally decrease the metric. The only slightly tricky one is bialgebra, where $d(L) = 16$ and $d(R) = 12$. What remains to be shown is locally decreasing the metric implies globally decreasing the metric.
\end{proof}


%$$\cgr{associativityR.pdf}$$

$$\xymatrix{ 
{\cgr{associativityLdpo.pdf} } & 4\ar[l] \ar[r] & { \cgr{associativityR.pdf} }  
}$$


$$\xymatrix{ 
2 & 4\ar[l] \ar[r] & 2}$$

% \begin{figure*}\caption{(Co)commutative Hopf algebra with trivial antipode \label{fig:hopf}}
%   \begin{center}
%   $$  \begin{array}{rccrcc}
%       \HC{1} & := & {\xymatrix{ {\cgr{associativityLdpo.pdf} } & 4\ar[l] \ar[r] & { \cgr{associativityR.pdf} }}}  
%       &
%       \HC{2} & := & {\xymatrix{ {\cgr{coassociativityL.pdf} } & 4\ar[l] \ar[r] & { \cgr{coassociativityR.pdf} }}}  
%       \\
%       \HC{3} & := & {\xymatrix{ {\cgr{commutativityL.pdf} } & 3\ar[l] \ar[r] & { \cgr{commutativityR.pdf} }}}  
%       &
%       \HC{4} & := & {\xymatrix{ {\cgr{cocommutativityL.pdf} } & 3\ar[l] \ar[r] & { \cgr{cocommutativityL.pdf} }}}  
%       \\
%       \HR{1} & := & {\xymatrix{ {\cgr{bialgL.pdf} } & 4\ar[l] \ar[r] & { \cgr{bialgR.pdf} }}}  
%             &
%       \HR{2} & := & {\xymatrix{ {\cgr{boneL.pdf} } & 0\ar[l] \ar[r] & {  }}}  
%       \\
%       \HR{3} & := & {\xymatrix{ {\cgr{duplicationunitL.pdf} } & 2\ar[l] \ar[r] & { \cgr{duplicationunitR.pdf} }}}  
%       &
%       \HR{4} & := & {\xymatrix{ {\cgr{duplicationcounitL.pdf} } & 2\ar[l] \ar[r] & { \cgr{duplicationcounitR.pdf} }}}  
%       \\
%       \HR{5} & := & {\xymatrix{ {\cgr{unitL.pdf} } & 2\ar[l] \ar[r] & { \cgr{unitR.pdf} }}}  
%             &
%       \HR{6} & := & {\xymatrix{ {\cgr{counitL.pdf} } & 2\ar[l] \ar[r] & { \cgr{counitR.pdf} }}}  
%       \\
%       \HR{6} & := & {\xymatrix{ {\cgr{hopfL.pdf} } & 2\ar[l] \ar[r] & { \cgr{hopfR.pdf} }}}  
%     \end{array}$$
%   \end{center}
% \end{figure*}


\begin{figure*}\caption{(Co)commutative Hopf algebra with trivial antipode \label{fig:hopf}}
  \begin{center}
  $$  \begin{array}{rccrcc}
      \HC{1} & := & {\xymatrix{ {\cgr{associativityLdpo.pdf} } & 4\ar[l] \ar[r] & { \cgr{associativityR.pdf} }}}  
      &
      \HC{2} & := & {\xymatrix{ {\cgr{coassociativityL.pdf} } & 4\ar[l] \ar[r] & { \cgr{coassociativityR.pdf} }}}  
      \\
      \HC{3} & := & {\xymatrix{ {\cgr{commutativityL.pdf} } & 3\ar[l] \ar[r] & { \cgr{commutativityR.pdf} }}}  
      &
      \HC{4} & := & {\xymatrix{ {\cgr{cocommutativityL.pdf} } & 3\ar[l] \ar[r] & { \cgr{cocommutativityL.pdf} }}}  
      \\
      \HR{1} & := & {\xymatrix{ {\cgr{bialgL.pdf} } & 4\ar[l] \ar[r] & { \cgr{bialgR.pdf} }}}  
            &
      \HR{2} & := & {\xymatrix{ {\cgr{boneL.pdf} } & 0\ar[l] \ar[r] & {  }}}  
      \\
      \HR{3} & := & {\xymatrix{ {\cgr{duplicationunitL.pdf} } & 2\ar[l] \ar[r] & { \cgr{duplicationunitR.pdf} }}}  
      &
      \HR{4} & := & {\xymatrix{ {\cgr{duplicationcounitL.pdf} } & 2\ar[l] \ar[r] & { \cgr{duplicationcounitR.pdf} }}}  
      \\
      \HR{5} & := & {\xymatrix{ {\cgr{unitL.pdf} } & 2\ar[l] \ar[r] & { \cgr{unitR.pdf} }}}  
            &
      \HR{6} & := & {\xymatrix{ {\cgr{counitL.pdf} } & 2\ar[l] \ar[r] & { \cgr{counitR.pdf} }}}  
      \\
      \HR{6} & := & {\xymatrix{ {\cgr{hopfL.pdf} } & 2\ar[l] \ar[r] & { \cgr{hopfR.pdf} }}}  
    \end{array}$$
  \end{center}
\end{figure*}



%\bR
%
%THIS DOESN'T WORK, SINCE ASSOC. ISN'T MONOTONE....
%
%For a hyperedge $h$, define the maximal path length to an input/output as follows:
%\begin{align*}
%  \textrm{in}(h) & := 1 + \max\{ \textrm{in}(p) \ |\  p \textrm{ is a predecessor hyperedge of } h \} \\
%  \textrm{out}(h) & := 1 + \max\{ \textrm{out}(s) \ |\  s \textrm{ is a successor hyperedge of } h \}
%\end{align*}
%where $\max\{\} = 0$. These are well-defined, since we consider hypergraphs that are directed acyclic.
%
%A rule is called path-monotone if, for every pair consisting of an input and an output, the length of the longest path connecting them is non-increasing from the LHS to the RHS. If there is no path, we call this length $0$.
%
%\begin{pro}\label{prop:image}
%  Let $h$ be a hyperedge not occurring in the image of a path-monotone rewrite $L \Rightarrow R$. Then, for $h'$ the corresponding hyperedge in $G[L\mapsto R]$:
%  \[ \textrm{in}(h) \geq \textrm{in}(h') \qquad\qquad
%     \textrm{out}(h) \geq \textrm{out}(h') \]
%\end{pro}
%
%Let $\mu$ be the type of multiply hyperedges and $\delta$ be the type of comultiply. Then let:
%\[ |G| := \sum_{\{ c \ | \ t(c) = \delta \}} 3^{\textrm{in}(c)} + \sum_{\{m \ | \ t(m) = \mu \}}  3^{\textrm{out}(m)} \]
%The Hopf algebra rewrite system is path-monotone, so by Proposition~\ref{prop:image}, we only need to reduce this metric for hyperedges in the image of a given rewrite rule.
%
%We treat associativity and commutativity as congruences, so we just need to show the remaining laws strictly reduce this metric. The only law that doesn't reduce the number of (co)multiplies is the 2-to-4 bialgebra law. Let $r$ and $s$ be the path lengths of the (co)multiply occurring on the LHS of the rule. Then:
%\[
%3^r + 3^s \ \ \leadsto\ \  2 \cdot 3^{r-1} + 2 \cdot 3^{s-1} < 3^r + 3^s
%\]
%...which is why we take 3 and not 2.
%
%\e

terminationHopf.tex
% -*- root: ../rewriting.tex -*-
\begin{figure*}\caption{DPO Rewriting system $\Phi(\rewiring{\mathcal{R}_{\scriptscriptstyle \NCB}})$ --- \emph{cf.} Example~\ref{ex:ncbialgebrasrewriting}.} \label{fig:hopf}
  \[
  \begin{array}{rrcl} %{rrclrrcl}
      \BA{1} := & \!\!\!\!\cgr{associativityLdpo.pdf}\!\!\!\! & \leftarrow 4 \rightarrow & \!\!\!\!\cgr{associativityR.pdf}
      \\%&
      \BA{2} := & \!\!\!\!\cgr{coassociativityL.pdf}\!\!\!\! & \leftarrow 4 \rightarrow & \!\!\!\!\cgr{coassociativityR.pdf}\!\!\!\!
      \\
      \BA{3} := & \!\!\!\!\cgr{unitL.pdf}\!\!\!\! & \leftarrow 2 \rightarrow & \!\!\!\!\cgr{unitR.pdf}\!\!\!\!
      \\%&
      \BA{4} := & \!\!\!\!\cgr{counitL.pdf}\!\!\!\! & \leftarrow 2 \rightarrow & \!\!\!\!\cgr{counitR.pdf}\!\!\!\!
      \\
      \BA{5} := & \!\!\!\!\cgr{RunitL.pdf}\!\!\!\! & \leftarrow 2 \rightarrow & \!\!\!\!\cgr{unitR.pdf}\!\!\!\!
      \\%&
      \BA{6} := &  \!\!\!\!\cgr{RcounitL.pdf}\!\!\!\! & \leftarrow 2 \rightarrow & \!\!\!\!\cgr{counitR.pdf}\!\!\!\!
      \\
      \BA{7} := & \!\!\!\!\cgr{duplicationunitL.pdf}\!\!\!\! & \leftarrow 2 \rightarrow & \!\!\!\!\cgr{duplicationunitR.pdf}\!\!\!\!
      \\%&
      \BA{8} := & \!\!\!\!\cgr{duplicationcounitL.pdf}\!\!\!\! & \leftarrow 2 \rightarrow & \!\!\!\!\cgr{duplicationcounitR.pdf}\!\!\!\!
      \\
      \BA{9} := & \!\!\!\!\cgr{bialgL.pdf}\!\!\!\! & \leftarrow 4 \rightarrow & \!\!\!\!\cgr{bialgR.pdf}\!\!\!\!
      \\%&
      \BA{10} := & \!\!\!\!\cgr{boneL.pdf}\!\!\!\! & \leftarrow 0 \rightarrow &  {  }
    \end{array}
  \]
\end{figure*}

Thanks to Theorem~\ref{th:adequacyRigidSMT}, we are now in position to recover Example~\ref{ex:ncbialgebrasrewriting} and study the DPO rewriting theory of non-commutative bialgebras (Example~\ref{exm:props}.\ref{ex:ncbialgebras}), shown in Figure~\ref{fig:hopf}. As a proof of concept, we focus on proving \emph{termination} for this system. First, we construct a metric based on two kinds of paths and a weight.
%The equations of non-commutative bialgebras, presented in Example~\ref{ex:ncbialgebras}, can be oriented and converted into the DPO system in Fig.~\ref{fig:hopf}. To show that this system terminates, we construct a metric based on two kinds of paths and a weight.
\begin{itemize}
  \item A \textit{U-path} is a path $p$ from an input or an $\eta$-hyperedge to an output or an $\epsilon$-hyperedge.
  \item An \textit{M-path} is a path from a $\mu$-hyperedge to a $\nu$-hyperedge.
\end{itemize}

A $\mu$-tree with root $x$ is a maximal tree of $\mu$-hyperedges with output $x$. Similarly, a $\nu$-tree with root $x$ is a maximal tree of $\nu$-hyperedges with input $x$.

For a $\mu$-hyperedge $h$, let the L-weight $\ell(h)$ be the size of the $\mu$-tree whose root is the first input of $\mu$. Similarly, for a $\nu$-hyperedge, let $\ell(h)$ be the size of the $\nu$-tree whose root is the first output of $h$. Let $\ell(h) = 0$ otherwise and:
\[
G \precL H \iff \sum_{h \in E_G} \ell(h) \leq \sum_{h \in E_H} \ell(h).
\]
Next, define orders \precU, \precM, \precmu, \precnu based on counting the number of U-paths, M-paths, $\mu$-hyperedges, and $\nu$-hyperedges, respectively. Armed with the five orders, we define the following lexicographic ordering that combines them as its components:
\begin{equation}\label{eq:lex-metric}
  \preceq \ :=\  \textrm{lex}(\precU, \precM, \precmu, \precnu, \precL)
\end{equation}
Clearly, $\preceq$ is well-founded, thus we can conclude as follows.

\begin{thm}
  %The rewrite system 
  $\BA{}$ is strictly decreasing in $\preceq$, thus it terminates.
\end{thm}

\begin{proof}
  We argue rule-by-rule, showing that each is strictly decreasing in one of the orders from \eqref{eq:lex-metric}, and non-increasing in every order that is prior in the lexicographic ordering.

  Since every rule \BA{j} has a unique path from every input to every output on the LHS and RHS, applications of these rules have no effect on paths which start and finish outside of their image. Hence, for each rule, we only need to consider paths which start or terminate in the image of the LHS.

  \BA{1} has no effect on $\eta$ or $\epsilon$ hypereges, hence no effect on \precU. No M-path can terminate in \BA{1} and any M-path originating on \BA{1} must exit through the unique output. Since there are precisely two $\mu$-hyperedges in the LHS and RHS, there is a 1-to-1 correspondence between M-paths before and after applying the rule. \BA{1} also leaves the number of $\mu$ and $\nu$ hyperedges fixed, so we only need to show it strictly decreases \precL. Applying the rule has no effect on the L-weight of any $\mu$-hyperedges outside of the image of the LHS. Suppose there are $\mu$-trees of size $a, b, c$ connected to inputs $0, 1, 2$ of the LHS, respectively. Then, the L-weight of the two $\mu$-hyperedges on the LHS are $a$ and $a + b + 1$, whereas on the LHS they are $a$ and $b$. Hence \precL is strictly decreased. \BA{2} follows via a symmetric argument.

  Since \BA{3}--\BA{6} and \BA{10} remove $\eta$- and $\epsilon$-hyperedges from the hypergraph, they will strictly decrease the number of U-paths.

  For \BA{7}, no U-path can terminate in the LHS, and any U-path starting in LHS must exit through one of the two outputs. Hence it corresponds to a unique U-path exiting the RHS. M-paths are unaffected, as is the number of $\mu$-hyperedges. However, the number of $\nu$-hyperedges is strictly decreased, so \BA{7} strictly decreases \precnu. The argument for \BA{8} is again symmetric.

  \BA{9} has no $\eta$ or $\epsilon$-hyperedges in its LHS or RHS, so it leaves the number of U-paths fixed. Consider an M-path which enters the LHS from the left. It must enter either from input $0$ or input $1$, hence it corresponds to a unique M-path entering the RHS. We can argue similarly for M-paths exiting on the right. Hence, the only M-path left to consider is the one from the $\mu$-hyperedge to the $\nu$-hyperedge in the LHS, which is eliminated. Thus \BA{9} strictly reduces \precM.
\end{proof}

Hence, the combinatorial presentation gives a short and simple proof of termination. We conjecture that one can construct a similarly simple proof of confluence, via analysis of critical pairs. There is an existing notion of critical pair in the DPO literature, of which \BA{} rewrite system has 24 (all of which are `joinable'). There are, however, subtleties arising in critical pair analysis for DPO rewrite systems~\cite{Plump1993} and general rewriting for SMCs~\cite{Lafont2003}. We leave development of a comprehensive theoretical framework for critical pair analysis on convex DPO rewrite systems as future work.

test.tex
\documentclass{article}

\begin{document}

poo

\end{document}

rewriting.bbl
\begin{thebibliography}{10}

\bibitem{Globular}
{Globular}.
\newblock \url{http://globular.science/}.
\newblock Accessed: 2016-01-18.

\bibitem{BaezErbele-CategoriesInControl}
J.~Baez and J.~Erbele.
\newblock Categories in control.
\newblock {\em CoRR/1405.6881}, 2014.

\bibitem{Bonchi2014b}
F.~Bonchi, P.~Sobocinski, and F.~Zanasi.
\newblock A categorical semantics of signal flow graphs.
\newblock In {\em {CONCUR} 2014}, pages 435--450, 2014.

\bibitem{Bonchi2015}
F.~Bonchi, P.~Sobocinski, and F.~Zanasi.
\newblock Full abstraction for signal flow graphs.
\newblock In {\em {POPL} 2015}, pages 515--526, 2015.

\bibitem{Bruni2006}
R.~Bruni, I.~Lanese, and U.~Montanari.
\newblock A basic algebra of stateless connectors.
\newblock {\em Theor Comput Sci}, 366:98--120, 2006.

\bibitem{Bruni2011}
R.~Bruni, H.~C. Melgratti, and U.~Montanari.
\newblock A connector algebra for {P/T} nets interactions.
\newblock In {\em {CONCUR `11}}, pages 312--326, 2011.

\bibitem{Burroni1993}
A.~Burroni.
\newblock Higher dimensional word problems with applications to equational
  logic.
\newblock {\em Theor Comput Sci}, 115:43--62, 1993.

\bibitem{Coecke2008}
B.~Coecke and R.~Duncan.
\newblock Interacting quantum observables.
\newblock In {\em ICALP`08}, pages 298--310, 2008.

\bibitem{Coecke2012}
B.~Coecke, R.~Duncan, A.~Kissinger, and Q.~Wang.
\newblock Strong complementarity and non-locality in categorical quantum
  mechanics.
\newblock In {\em LiCS`12}, pages 245--254, 2012.

\bibitem{GadducciCorradini-termgraph}
A.~Corradini and F.~Gadducci.
\newblock An algebraic presentation of term graphs, via {GS}-monoidal
  categories.
\newblock {\em Appl Cat S}, 7(4):299--331, 1999.

\bibitem{open_graphs1}
L.~Dixon and A.~Kissinger.
\newblock Open-graphs and monoidal theories.
\newblock {\em Math Str Comput Sci}, 23:308--359, 4 2013.

\bibitem{Ehrig2004}
H.~Ehrig and B.~K\"{o}nig.
\newblock Deriving bisimulation congruences in the {DPO} approach to graph
  rewriting.
\newblock In {\em {FoSSaCS `04}}, LNCS, 2004.

\bibitem{Ehrig1976}
H.~Ehrig and H.-J. Kreowski.
\newblock Parallelism of manipulations in multidimensional information
  structures.
\newblock In {\em MFCS `76}, LNCS, 1976.

\bibitem{Fong2015}
B.~Fong, P.~Rapisarda, and P.~Soboci\'{n}ski.
\newblock A categorical approach to open \& interconnected dynamical systems.
\newblock {\em CoRR/1510.05076}, 2015.

\bibitem{Gadducci1998}
F.~Gadducci and R.~Heckel.
\newblock An inductive view of graph transformation.
\newblock LNCS. Springer, 1998.

\bibitem{DBLP:journals/corr/abs-math-0612083}
Y.~Guiraud.
\newblock Termination orders for 3-dimensional rewriting.
\newblock {\em CoRR}, abs/math/0612083, 2006.

\bibitem{hyland2007category}
M.~Hyland and J.~Power.
\newblock Lawvere theories and monads.
\newblock {\em ENTCS}, 172:437--458, 2007.

\bibitem{Joyal1991}
A.~Joyal and R.~Street.
\newblock The geometry of tensor calculus, \textsc{i}.
\newblock {\em Adv Math}, 88:55--112, 1991.

\bibitem{Joyal_tracedcategories}
A.~Joyal, R.~Street, and D.~Verity.
\newblock Traced monoidal categories.
\newblock {\em Math Proc Cambridge Phil Soc}, 119:447--468, 4 1996.

\bibitem{Kassel-quantumgroups2012}
C.~Kassel.
\newblock {\em Quantum Groups}.
\newblock Springer, 2012.

\bibitem{Kelly1980}
G.~M. Kelly and M.~L. Laplaza.
\newblock Coherence for compact closed categories.
\newblock {\em J Pure Appl Algebra}, 19:193--213, 1980.

\bibitem{Kissinger_quantomatic}
A.~Kissinger and V.~Zamdzhiev.
\newblock Quantomatic: {A} proof assistant for diagrammatic reasoning.
\newblock {\em CoRR}, abs/1503.01034, 2015.

\bibitem{Lack2004a}
S.~Lack.
\newblock Composing {PROPs}.
\newblock {\em Theor App Cats}, 13(9):147--163, 2004.

\bibitem{Lack2005}
S.~Lack and P.~Soboci\'{n}ski.
\newblock Adhesive and quasiadhesive categories.
\newblock {\em RAIRO-Theor.\ Inf.\ Appl.}, 39(3):511--546, 2005.

\bibitem{Lafont2003}
Y.~Lafont.
\newblock Towards an algebraic theory of boolean circuits.
\newblock {\em J Pure Appl Alg}, 184:257--310, 2003.

\bibitem{MacLane1965}
S.~{Mac Lane}.
\newblock Categorical algebra.
\newblock {\em B Am Math Soc}, 71:40--106, 1965.

\bibitem{MacDonald2009}
J.~MacDonald and L.~Scull.
\newblock Amalgamations of categories.
\newblock {\em Can Math B}, 52:273--284, 2009.

\bibitem{Meseguer1990}
J.~Meseguer and U.~Montanari.
\newblock {P}etri nets are monoids.
\newblock {\em Inform Comput}, 88:105--155, 1990.

\bibitem{Mimram14}
S.~Mimram.
\newblock Towards 3-dimensional rewriting theory.
\newblock {\em Log Meth Comput Sci}, 10(2), 2014.

\bibitem{Plump1993}
D.~Plump.
\newblock In {\em Term Graph Rewriting}, chapter Hypergraph Rewriting: Critical
  Pairs and Undecidability of Confluence, pages 201--213. Wiley, 1993.

\bibitem{Rathke2014a}
J.~Rathke, P.~Soboci\'{n}ski, and O.~Stephens.
\newblock Compositional reachability in {P}etri nets.
\newblock In {\em Reachability Problems `14}, 2014.

\bibitem{Rosebrugh2005}
R.~Rosebrugh, N.~Sabadini, and R.~Walters.
\newblock Generic commutative separable algebras and cospans of graphs.
\newblock {\em Th Appl Categories}, 17(6):164--177, 2005.

\bibitem{Sassone2005a}
V.~Sassone and P.~Soboci\'{n}ski.
\newblock Reactive systems over cospans.
\newblock In {\em {LiCS `05}}, pages 311--320. IEEE Press, 2005.

\bibitem{Selinger07DaggerCC}
P.~Selinger.
\newblock Dagger compact closed categories and completely positive maps.
\newblock {\em ENTCS}, 170:139--163, 2007.

\bibitem{Selinger2009}
P.~Selinger.
\newblock A survey of graphical languages for monoidal categories.
\newblock {\em Springer Lecture Notes in Physics}, 13(813):289--355, 2011.

\bibitem{TermGraphSurvey}
M.~R. Sleep, M.~J. Plasmeijer, and M.~C. J.~D. van Eekelen, editors.
\newblock {\em Term Graph Rewriting: Theory and Practice}.
\newblock Wiley, 1993.

\bibitem{Sobocinski2014}
P.~Soboci\'{n}ski and O.~Stephens.
\newblock A programming language for spatial distribution of net systems.
\newblock In {\em Petri Nets `14}, 2014.

\bibitem{Street-computads}
R.~Street.
\newblock Limits indexed by category-valued 2-functors.
\newblock {\em J Pure Appl Algebra}, 8(2):149 -- 181, 1976.

\bibitem{Walters-lecture-WSCC}
R.~Walters.
\newblock The tensor product of matrices.
\newblock Lecture, International Conference on Category Theory,
  Louvain-la-Neuve, 1987.

\bibitem{ZanasiThesis}
F.~Zanasi.
\newblock {\em Interacting Hopf Algebras: the theory of linear systems}.
\newblock PhD thesis, {E}cole Normale Sup\'{e}rieure de Lyon, 2015.

\end{thebibliography}
