main.tex

\documentclass[10pt]{article}

\usepackage[utf8]{inputenc}
\usepackage[margin=0.5in]{geometry}
\usepackage{kpfonts}

\PassOptionsToPackage{usenames, dvipsnames}{xcolor}
\usepackage{figures/tikzit}

\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{stmaryrd}
\usepackage{microtype}
\usepackage{enumitem}

\usepackage[style=alphabetic]{biblatex}
\usepackage[colorlinks=true, citecolor=Green, linkcolor=NavyBlue, urlcolor=BrickRed, pdftitle={Fully abstract categorical semantics for digital circuits}]{hyperref}
\usepackage[capitalise]{cleveref}

\input{macros/sets}
\input{macros/category}
\input{macros/streams}
\input{macros/circuits}
\input{macros/theorems}

\input{figures/circuits.tikzstyles}
\input{figures/circuits.tikzdefs}

\setcounter{biburlnumpenalty}{100}
\setcounter{biburlucpenalty}{100}
\setcounter{biburllcpenalty}{100}

\addbibresource{refs/refs.biblatex.bib}
\pagenumbering{gobble} 

\title{\vspace{-3em}Fully abstract categorical semantics for digital circuits\\\textbf{Extended abstract}}
\author{\textbf{George Kaye}, David Sprunger and Dan R. Ghica}
\date{July 20, 2022}

\begin{document}
    \maketitle

    \paragraph*{Contribution.}
    It is essential that we have ways to verify the correctness of digital circuits and reason with them.
    Conventionally, this is done by translation into an executable model which can be simulated to observe its behaviour.
    An alternative approach, used in software, is to reason \emph{syntactically}: programs are formulated equationally and can be reduced step by step.
    When provided with inputs, the goal of such a system is to apply reductions and derive an output value.

    Such an equational system was first presented in~\cite{ghica2016categorical,ghica2017diagrammatic}, in which digital circuits with delay and (instant) feedback are modelled as morphisms in a freely generated traced cartesian category, or \emph{dataflow category}~\cite{cazanescu1994feedback,hasegawa1997recursion}.
    However, the presentation was informal and, crucially, not complete: not all circuits could be reduced to a stream of values.
    Our work brings this project to its conclusion, formalising the categorical semantics and completing the set of equations.

    \paragraph*{Syntax.}
    Circuits are defined over a \emph{signature}.

    \begin{definition}[Circuit signature]
        Let \(\Sigma\) be a tuple \((\mathcal{V},\disconnected,\shortcircuit,\mathcal{G})\) where \(\mathcal{V}\) is a finite set of \emph{values} with distinguished elements \(\disconnected,\shortcircuit \in \mathcal{V}\), and \(\mathcal{G}\) is a finite set of tuples \((g,m)\) where \(g\) is a \emph{gate symbol} and \(m \in \nat\) is its \emph{arity}.
    \end{definition}

    \noindent
    The distinct elements \(\bullet\) and \(\circ\) represent a \emph{disconnected wire} (a \emph{lack} of information) and a \emph{short circuit} (\emph{inconsistent} information) respectively.
    Digital circuits are constructed as morphisms in a freely generated symmetric traced monoidal category (STMC).
    To aid in the presentation, we shall use the graphical calculus of \emph{string diagrams}~\cite{joyal1991geometry,joyal1996traced,selinger2011survey}.

    \begin{definition}[Sequential circuits]
        For a signature \(\Sigma\), let \(\scircsigma\) be the symmetric traced monoidal category freely generated over:
        \begin{align*}
            \iltikzfig{circuits/components/values/v}\ \text{for each}\ v \in \circuitsignaturevalues
            &&
            \iltikzfig{circuits/components/gates/gate-labelled}\ \text{for each}\ (g,m) \in \circuitsignaturegates
            &&
            \iltikzfig{strings/structure/comonoid/copy}
            &&
            \iltikzfig{strings/structure/monoid/merge}
            &&
            \iltikzfig{strings/structure/comonoid/discard}
            &&
            \iltikzfig{circuits/components/delay}
        \end{align*}
    \end{definition}    

    \noindent
    In turn each generator represents: \emph{values} that flow through wires; \emph{gates}; constructs for forking, joining and stubbing wires; and finally a generator for \emph{delay}.
    Circuits obtained by composing generators are drawn as dark green squares \iltikzfig{circuits/components/circuits/f-seq}; circuits containing only gates and structural generators are drawn in a lighter blue square \iltikzfig{circuits/components/circuits/f-comb}.
    To avoid clutter, we occasionally omit the backgrounds of concrete generators in large diagrams.

    \paragraph*{Semantics.}

    Circuits specified syntactically have no computational content.
    To add \emph{semantics} to circuits, first the signature must be interpreted in some domain.

    \begin{definition}[Interpretation]\label{def:interpretation}
        An interpretation of \(\circuitsignature = (\circuitsignaturevalues,\bullet,\circ,\circuitsignaturegates)\) is a tuple \(\interpretation = (\mathbf{V}, \valueinterpretation,\gateinterpretation)\) where \((\values,\sqsubseteq, \bot,\top)\) is a finite lattice, \(\valueinterpretation\) is a function \(\circuitsignaturevalues \setminus \{\disconnected,\shortcircuit\} \to \values \setminus \{\bot,\top\}\), and \(\gateinterpretation\) is a map from each \((g,m) \in \circuitsignaturegates\) to a monotone function \(\morph{\overline{g}}{\valuetuple{m}}{\values}\) such that \(\overline{g}(\bot^m) = \bot\) and \(\overline{g}(\mathbf{v})\) is in the image of \(\valueinterpretation\) for all \(\mathbf{v} \in \valuetuple{m}\).
    \end{definition}

    \begin{figure}[p]
        \centering
        \tikzfig{circuits/a4}
        \quad
        \scalebox{1}{
            \begin{tabular}{|c|cccc|}
                \hline
                \(\land\) & \(\bot\) & \(0\) & \(1\) & \(\top\) \\
                \hline
                \(\bot\)  & \(\bot\) & \(0\) & \(\bot\) & \(0\) \\
                \(0\) & \(0\) & \(0\) & \(0\) & \(0\) \\
                \(1\) & \(\bot\) & \(0\) & \(1\) & \(\top\) \\
                \(\top\) & \(0\) & \(0\) & \(\top\) & \(\top\) \\
                \hline
            \end{tabular}
            \quad
            \begin{tabular}{|c|cccc|}
                \hline
                \(\lor\) & \(\bot\) & \(0\) & \(1\) & \(\top\) \\
                \hline
                \(\bot\)  & \(\bot\) & \(\bot\) & \(1\) & \(1\) \\
                \(0\) & \(\bot\) & \(0\) & \(1\) & \(\top\) \\
                \(1\) & \(1\) & \(1\) & \(1\) & \(1\) \\
                \(\top\) & \(1\) & \(\top\) & \(1\) & \(\top\) \\
                \hline
            \end{tabular}
            \quad
            \begin{tabular}{|c|c|}
                \hline    
                \(\neg\) & \\
                \hline
                \(\bot\) & \(\bot\) \\
                \(1\) & \(0\) \\
                \(0\) & \(1\) \\
                \(\top\) & \(\top\) \\
                \hline
            \end{tabular}
        }
        \caption{The lattice structure on \(\values_\star\), and truth tables for the gates in \(\Sigma_\star\) under \(\interpretation_\star\).}
        \label{tab:truths}
    \end{figure}

    \begin{example}\label{ex:interp}
        Let \(\Sigma_\star = (\{\disconnected,\valuetrue,\valuefalse,\shortcircuit\}, \disconnected, \shortcircuit, \{(\text{AND},2),(\text{OR},2),(\text{NOT},1)\}\)) be a signature.
        In \(\scirc{\Sigma_\star}\), the values are \(\iltikzfig{strings/structure/monoid/init}, \iltikzfig{circuits/components/values/true}, \iltikzfig{circuits/components/values/false}\) and \(\iltikzfig{strings/structure/monoid/init-white}\); the gates are \(\iltikzfig{circuits/components/gates/and}, \iltikzfig{circuits/components/gates/or}\) and \(\iltikzfig{circuits/components/gates/not}\).
        Let \(\values_\star\) be the lattice \((\{\bot, 0, 1, \top\},\sqsubseteq)\), with the join defined as \(0 \ljoin 1 = \top\) and the meet defined as \(0 \lmeet 1 = \bot\).
        Let \(\{\wedge,\vee,\neg\}\) be the \emph{Belnap logic} operators~\cite{belnap1977useful}: the truth tables are listed in \cref{tab:truths}.
        Let \(\interpretation_\star = (\mathbf{V}_\star, \{\mathsf{f} \mapsto 0, \mathsf{t} \mapsto 1\}, \{\text{AND} \mapsto \land, \text{OR} \mapsto \lor, \text{NOT} \mapsto \neg\})\).
    \end{example}

    \noindent
    The semantics of circuits is that of \emph{stream functions}, which take as input a stream and output a stream.
    In particular, we are interested in stream functions of the form \(\valuetuplestream{m} \to \valuetuplestream{n}\).

    \begin{example}
        For a value \(v \in \circuitsignaturevalues\), the stream function \(\morph{\valstream{v}}{\stream{(\valuetuple{0})}}{\stream{\values}}\) is defined as \(\valstream{v}(\bullet)(0) := \valueinterpretation(v), \valstream{v}(\bullet)(i+1) := \bot\). 
        For a gate \((g,m) \in \circuitsignaturegates\), the stream function \(\morph{\gatestream{g}}{\stream{(\valuetuple{m})}}{\stream{\values}}\) is defined as \(\gatestream{g}(\sigma)(i) := \gateinterpretation(g)(\sigma(i))\).
        Finally, the \emph{shift} stream function \(\morph{\delta}{\stream{\values}}{\stream{\values}}\) is defined as \(\delta(\sigma)(0) := \bot, \delta(\sigma)(i+1) := \sigma(i)\).
    \end{example}
    
    \begin{definition}
        For a signature \(\circuitsignature = (\circuitsignaturevalues,\bullet,\circ,\circuitsignaturegates)\) and its interpretation \(\interpretation = (\values, \valueinterpretation, \gateinterpretation)\), let \(\streami\) be the prop freely generated over \(\valstream{v}\) for each \(v \in \circuitsignaturevalues\), \(\gatestream{g}\) for each \((g,m) \in \circuitsignaturegates\), and the shift stream \(\delta\).
        Composition and tensor are by function composition and cartesian product; the symmetry swaps input streams.
    \end{definition}

    \begin{theorem}
        \(\streami\) is traced.
    \end{theorem}

    \begin{definition}\label{def:circuittostreams}
        Let \(\morph{\circuittostream{\interpretation}}{\scircsigma}{\streami}\) be a traced prop morphism, mapping circuits to appropriate stream functions.
        The details are omitted, see~\cite{ghica2022full}.
    \end{definition}

    \noindent
    If two circuits map to the same semantics in \(\streami\), we say they are \emph{extensionally equivalent}, written \(\iltikzfig{circuits/components/circuits/f-seq} \extequivi \iltikzfig{circuits/components/circuits/g-seq}\).

    \begin{theorem}[\cite{ghica2022full}]
        Let \(\scircsigmai\) be the category obtained by quotienting \(\scircsigma\) by \(\extequivi\).
        Then there is an isomorphism of categories \(\scircsigmai \cong \streami\).
    \end{theorem}

    \paragraph*{Equational reasoning.}

    Circuits of non-equal syntax can have the same semantics as stream functions.
    However, in general it is prohibitive to check that the corresponding streams for two circuits are equal: it is more efficient to reason \emph{equationally}.
    Equations are identities that hold in the quotient category \(\scircsigmai\): we write \(\iltikzfig{circuits/components/circuits/f-seq} \eqaxioms{} \iltikzfig{circuits/components/circuits/g-seq}\) if \(\iltikzfig{circuits/components/circuits/f-seq}\) is equal to \(\iltikzfig{circuits/components/circuits/g-seq}\) under the equational theory.
    Note that since we are using string diagrams, the axioms of STMCs are `absorbed' into the notation and always hold by moving wires and boxes around.

    \begin{figure}[p]
        \centering
        \begin{align*}
            \iltikzfig{circuits/axioms/join-lhs}
            &\eqaxioms{}
            \iltikzfig{circuits/axioms/join-rhs}
            &
            \iltikzfig{circuits/axioms/gate-lhs}
            &\eqaxioms{}
            \iltikzfig{circuits/axioms/gate-rhs}
            &
            \iltikzfig{strings/structure/comonoid/unitality-l-lhs}
            &\eqaxioms{}
            \iltikzfig{strings/structure/comonoid/unitality-l-rhs}
            \eqaxioms{}
            \iltikzfig{strings/structure/comonoid/unitality-r-lhs}
            &
            \iltikzfig{strings/structure/monoid/unitality-l-lhs}
            &\eqaxioms{}
            \iltikzfig{strings/structure/monoid/unitality-l-rhs}
            \eqaxioms{}
            \iltikzfig{strings/structure/monoid/unitality-r-lhs}
            &
            \iltikzfig{circuits/axioms/disconnect-lhs}
            &\eqaxioms{}
            \iltikzfig{circuits/axioms/disconnect-rhs} 
        \end{align*}
        \begin{align*}
            \iltikzfig{strings/cartesian/naturality-discard-lhs}
            &\eqaxioms{}
            \iltikzfig{strings/cartesian/naturality-discard-rhs}
            &
            \iltikzfig{strings/cartesian/naturality-copy-lhs}
            &\eqaxioms{}
            \iltikzfig{strings/cartesian/naturality-copy-rhs}
            &
            \iltikzfig{circuits/axioms/streaming-lhs}
            &\eqaxioms{}
            \iltikzfig{circuits/axioms/streaming-rhs} 
            &
            \iltikzfig{circuits/instant-feedback/axiom-lhs}
            &\eqaxioms{}
            \iltikzfig{circuits/instant-feedback/axiom-rhs}
        \end{align*}
        \caption{Equations for reducing closed circuits.}
        \label{fig:closed-circuit-axioms}
    \end{figure}

    \begin{figure}[p]
        \centering
        \begin{align*}
            \iltikzfig{strings/traced/trace-rhs.seq} 
            = \iltikzfig{circuits/examples/reasoning/unfolding/unfolding-1}
            = \iltikzfig{circuits/examples/reasoning/unfolding/unfolding-2}
            = \iltikzfig{circuits/examples/reasoning/unfolding/unfolding-3}
        \end{align*}
        \caption{Deriving the \emph{unfolding} rule.}
        \label{fig:unfolding}
    \end{figure}

    \paragraph*{Productivity.}
    A common use of equational reasoning is to take a circuit and reduce it to its stream of output values.

    \begin{definition}[Productivity]
        For a set of equations \(\mathcal{E}\), a closed sequential circuit \iltikzfig{circuits/components/circuits/f-seq-closed} is called \emph{productive under} \(\mathcal{E}\) if there exist values \iltikzfig{circuits/components/values/vs-n} and sequential circuit \iltikzfig{circuits/components/circuits/g-seq-closed} such that
        \(
            \iltikzfig{circuits/components/circuits/f-seq-closed} 
            \eqaxioms{\mathcal{E}}
            \iltikzfig{circuits/productivity/productive}
        \).
    \end{definition}

    \noindent
    A set of equations was presented in~\cite{ghica2016categorical}.
    However, they were not \emph{complete}: these axioms could not necessarily handle circuits with \emph{non-delay-guarded feedback}, in which every feedback loop does not pass through a delay generator.
    While in some circuits `instant feedback' is useful~\cite{riedel2004cyclic,mendler2012constructive}, in other cases it can result in an unproductive circuit.
    To tackle this, we use the \emph{Kleene fixpoint theorem}: since all the gates in an interpretation are monotone, they have a least fixpoint; since our lattice is finite, we are able to compute it after a finite number of iterations.

    \begin{definition}
        For a combinational circuit
        \(\iltikzfig{circuits/instant-feedback/fixpoint-lhs}\)
        , let its \emph{\(n\)th iteration} 
        \(\iltikzfig{circuits/instant-feedback/fn-box}\) 
        be defined inductively as
        \(
            \iltikzfig{circuits/instant-feedback/f0-box} 
            := 
            \iltikzfig{circuits/instant-feedback/f0-definition}
        \) 
        and 
        \(
            \iltikzfig{circuits/instant-feedback/fkp1-box} 
            := 
            \iltikzfig{circuits/instant-feedback/fkp1-definition}
        \).
        Let \(\interpretation = (\values,\valueinterpretation,\gateinterpretation)\) be an interpretation and let \(c\) be the length of the longest chain in \(\values\): the \emph{fixpoint} of 
        \(\iltikzfig{circuits/instant-feedback/fixpoint-lhs}\)
        in \(\interpretation\), denoted as 
        \(\iltikzfig{circuits/instant-feedback/fixpoint}\)
        , is defined as \(\iltikzfig{circuits/instant-feedback/fc-box}\).
    \end{definition}
    
    \noindent
    The complete set of equations \(\mathcal{C}\) for closed circuits under \emph{any} interpretation is shown in \cref{fig:closed-circuit-axioms}.
    An important consequence of these is that the \emph{unfolding} rule for circuits with feedback can be derived, illustrated in \cref{fig:unfolding}.

    \begin{theorem}
        Any closed sequential circuit \iltikzfig{circuits/components/circuits/f-seq-closed} is productive under \(\mathcal{C}\).
    \end{theorem}

    \noindent
    By applying productivity, a sequence of values can be obtained for \emph{any} sequential circuit \(\iltikzfig{circuits/components/circuits/f-seq}\) given some inputs \(\iltikzfig{circuits/components/values/vs}\).
    This sequence is precisely the corresponding stream obtained using \(\circuittostream{\interpretation}\).

    \paragraph*{Full abstraction.}

    In the closed case these equations suffice, but when faced with an \emph{open circuit} we must devise another equation.
    To do this, we view circuits as \emph{state transition machines}: recall that a circuit \(\iltikzfig{circuits/components/circuits/f-seq}\) is in \emph{global delay form} if it is in the form \(\iltikzfig{circuits/full-abstraction/global-delay-f}\).
    We call the circuit \(\iltikzfig{circuits/components/circuits/f-pre-trace}\) a \emph{combinational core} of \(\iltikzfig{circuits/components/circuits/f-seq}\): this circuit produces its \emph{state transition} and its \emph{output}.
    To equate circuits with the same behaviour we essentially construct a bisimulation between these state machines.

    \begin{proposition}
        Let \(\iltikzfig{circuits/components/circuits/f-seq}\) and \(\iltikzfig{circuits/components/circuits/f-seq}\) be sequential circuits. Then, if their combinational cores produce the same outputs for all accessible states, then \(\iltikzfig{circuits/components/circuits/f-seq} \eqaxioms{} \iltikzfig{circuits/components/circuits/f-seq}\)
    \end{proposition}

    \begin{figure}[p]
        \centering
        \begin{align*}
            \iltikzfig{strings/structure/comonoid/unitality-l-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/comonoid/unitality-l-rhs} &
            \iltikzfig{strings/structure/comonoid/unitality-r-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/comonoid/unitality-r-rhs} &
            \iltikzfig{strings/structure/comonoid/associativity-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/comonoid/associativity-rhs} &
            \iltikzfig{strings/structure/comonoid/commutativity-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/comonoid/commutativity-rhs}
        \end{align*}
        \begin{align*}
            \iltikzfig{strings/structure/monoid/unitality-l-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/monoid/unitality-l-rhs} &
            \iltikzfig{strings/structure/monoid/unitality-r-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/monoid/unitality-r-rhs} &
            \iltikzfig{strings/structure/monoid/associativity-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/monoid/associativity-rhs} &
            \iltikzfig{strings/structure/monoid/commutativity-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/monoid/commutativity-rhs}
        \end{align*}
        \begin{align*}
            \iltikzfig{strings/structure/bialgebra/copy-merge-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/bialgebra/copy-merge-rhs} &
            \iltikzfig{strings/structure/bialgebra/merge-copy-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/bialgebra/merge-copy-rhs} &
            \iltikzfig{strings/structure/bialgebra/init-copy-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/bialgebra/init-copy-rhs} &
            \iltikzfig{strings/structure/bialgebra/merge-discard-lhs} &\eqaxioms{}
            \iltikzfig{strings/structure/bialgebra/merge-discard-rhs}
       \end{align*}
        \caption{The equations of a \emph{bialgebra}, derivable using the `Mealy equation'}
        \label{fig:bialgebra-axioms}
    \end{figure}

    \begin{figure}[p]
        \centering
        \begin{align*}
            \iltikzfig{circuits/axioms/belnap/or-associativity-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/or-associativity-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/and-associativity-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/and-associativity-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/or-commutativity-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/or-commutativity-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/and-commutativity-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/and-commutativity-rhs}
        \end{align*}
        \begin{align*}
            \iltikzfig{circuits/axioms/belnap/or-identity-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/or-identity-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/and-identity-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/and-identity-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/or-annihilator-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/or-annihilator-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/and-annihilator-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/and-annihilator-rhs}
        \end{align*}
        \begin{align*}
            \iltikzfig{circuits/axioms/belnap/or-idempotent-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/or-idempotent-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/and-idempotent-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/and-idempotent-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/absorption-1-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/absorption-1-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/absorption-2-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/absorption-2-rhs}
        \end{align*}
        \begin{align*}
            \iltikzfig{circuits/axioms/belnap/or-and-distributivity-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/or-and-distributivity-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/and-or-distributivity-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/and-or-distributivity-rhs}
        \end{align*}
        \begin{align*}
            \iltikzfig{circuits/axioms/belnap/double-negation-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/double-negation-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/de-morgan-1-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/de-morgan-1-rhs}
            &
            \iltikzfig{circuits/axioms/belnap/de-morgan-2-lhs}
            &\eqaxioms[(\mealyequation)]{}
            \iltikzfig{circuits/axioms/belnap/de-morgan-2-rhs}
        \end{align*}
        \caption{A set of equations derivable using the `Mealy equation', .}
        \label{fig:combinational-axioms}
    \end{figure}

    \noindent
    This equivalence may look obtuse at first glance, but many familiar equations can be derived using it: a selection is shown in \cref{fig:bialgebra-axioms,fig:combinational-axioms}.
    With this equation, the final result can be shown.

    \begin{theorem}[Full abstraction]
        \(\iltikzfig{circuits/components/circuits/f-seq} \eqaxioms{\closedcombequations + \mealyequation}\iltikzfig{circuits/components/circuits/g-seq}\) if and only if \(\circuittostream[\iltikzfig{circuits/components/circuits/f-seq}]{\interpretation} = \circuittostream[\iltikzfig{circuits/components/circuits/g-seq}]{\interpretation}\).
    \end{theorem}

    \noindent
    This allows us to reason \emph{purely equationally} with digital circuits, instead of appealing to the potentially inefficient stream semantics.
    Even so, this does not immediately yield an \emph{automatic} rewriting framework, as computationally it is difficult to handle the trace.
    A suitable strategy for tackling this problem was presented in~\cite{ghica2017diagrammatic} using graph rewriting on \emph{framed point graphs}; a current thread of work is reworking this using recent work on rewriting with \emph{hypergraphs}~\cite{bonchi2016rewriting,kaye2021rewriting}.

    \printbibliography[heading=bibintoc,title={References}]

\end{document}