Make some small changes

Author: georgejkaye

figures

@@ -34,31 +34,30 @@
 \addbibresource{refs/refs.biblatex.bib}
 \pagenumbering{gobble} 
 
-\title{\vspace{-3em}Full abstraction for digital circuits: \textbf{Extended abstract}}
+\title{\vspace{-3em}Fully abstract categorical semantics for digital circuits: \textbf{Extended abstract}}
 \author{\textbf{George Kaye}, David Sprunger and Dan R. Ghica}
 
 \begin{document}
     \maketitle
 
-    \paragraph*{Motivation.}
-    Digital circuits are ubiquitous in today's society, so it is essential that we have easy ways to verify their correctness and reason with them.
-    Conventionally, this is done by translation into an executable model such as an automaton, which can be simulated to observe its behaviour.
-    An alternative approach, used commonly in software, is to reason \emph{syntactically}: programs are formulated equationally and can be reduced step by step by identifying \emph{redexes} in terms.
-    When provided with inputs, the goal of such a system is to apply redexes and eventually return an output value.
+    \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 feedback are modelled as morphisms in a freely generated traced cartesian category, or \emph{dataflow category}~\cite{cazanescu1990new,cazanescu1994feedback}.
-    However, there were some informalities in the presentation, and, crucially, the framework was not guaranteed to reduce circuits with \emph{non-delay-guarded feedback} to a 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, and could not reduce all circuits 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.}
-    Before we can start constructing circuits, we must specify the components we can use.
 
     \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} (a \emph{glut} of information) respectively.
+    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.
     Using a signature, 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}.
 
@@ -85,16 +84,17 @@
     The final generator is a \emph{delay} generator: one can think of this as delaying its inputs for one tick of the clock.
     We write arbitrary sequential circuits obtained by composing generators together as green squares \iltikzfig{circuits/components/circuits/f-seq}.
     If a circuit is \emph{combinational}, i.e. it contains no delay or trace, it is drawn in a lighter blue square \iltikzfig{circuits/components/circuits/f-comb}.
-    When restricted to the combinational circuits, this work is similar to~\cite{lafont2003algebraic}: where the approaches diverge is the inclusion of delay and feedback.
+    When restricted to the combinational circuits, this work is similar to~\cite{lafont2003algebraic}.
+    Where the approaches diverge is the inclusion of delay and feedback.
 
     \paragraph*{Semantics.}
 
-    Circuits specified syntactically have no computational content associated with them.
+    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}
-        Let \(\circuitsignature = (\circuitsignaturevalues,\circuitsignaturegates)\) be a circuit signature.
-        A interpretation of \(\circuitsignature\) is a tuple \(\interpretation = (\mathbf{V}, \valueinterpretation,\gateinterpretation)\) where \(\values\) is a finite lattice, \(\valueinterpretation\) is a bijective function \(\valueinterpretation \setminus \{\disconnected,\shortcircuit\} \to \values \setminus \{\top,\bot\}\), and \(\gateinterpretation\) is a map from each gate \((g,m) \in \circuitsignaturegates\) to a monotone function \(\morph{\overline{g}}{\valuetuple{m}}{\values}\).
+        Let \(\circuitsignature = (\circuitsignaturevalues,\circuitsignaturegates)\) be a signature.
+        A interpretation of \(\circuitsignature\) is a tuple \(\interpretation = (\mathbf{V}, \valueinterpretation,\gateinterpretation)\) where \(\values\) is a finite lattice, \(\valueinterpretation\) is a bijective function \(\valueinterpretation \setminus \{\disconnected,\shortcircuit\} \to \values \setminus \{\top,\bot\}\), and \(\gateinterpretation\) is a map from each \((g,m) \in \circuitsignaturegates\) to a monotone function \(\morph{\overline{g}}{\valuetuple{m}}{\values}\).
     \end{definition}
 
     \begin{figure}[p]
@@ -170,12 +170,12 @@
 
     \begin{theorem}[\cite{ghica2022full}]
         Let \(\scircsigmai\) be the category obtained by quotienting \(\scircsigma\) by \(\eqaxioms{\mathcal{B}}\).
-        Then, \(\scircsigmai \cong \streami\).
+        Then, there is an isomorphism of categories \(\scircsigmai \cong \streami\).
     \end{theorem}
 
     \paragraph*{Equational reasoning.}
 
-    Circuits of different structure can have the same semantics as stream functions.
+    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~\cite{ghica2017diagrammatica}: it is more efficient to reason \emph{equationally}.
     Equations are identities that hold in the quotient category \(\scircsigmai\).
     Given a set of equations \(\mathcal{E}\), we write \(\iltikzfig{circuits/components/circuits/f-seq} \eqaxioms{\mathcal{E}} \iltikzfig{circuits/components/circuits/g-seq}\) if \iltikzfig{circuits/components/circuits/f-seq} can be rewritten to \iltikzfig{circuits/components/circuits/g-seq} by applying equations in \(\mathcal{E}\).
@@ -224,8 +224,20 @@
         \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 using equations in \(\mathcal{C}\).}
+        \label{fig:unfolding}
+    \end{figure}
+
     \paragraph*{Productivity.}
-    A common use of equational reasoning is to take a circuit and reduce it to its output values.
+    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/fcirc-closed-traced} is called \emph{productive under} \(\mathcal{E}\) if there exist values \iltikzfig{circuits/components/values/vs} and sequential circuit \iltikzfig{circuits/components/gcirc-closed-traced} such that
@@ -240,7 +252,7 @@
     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 take inspiration from \emph{Kleene's 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.
+    To tackle this, we use \emph{Kleene's 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}
 
@@ -269,6 +281,7 @@
 
     \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}\).
@@ -291,14 +304,14 @@
     All that remains is to add equations for equivalences between gates
 
     \begin{definition}
-        We say that a set of equations \(\mathcal{E}\), where each \(e \in \mathcal{E}\) contains at least one gate, is \emph{combinationally complete} for an interpretation \(\interpretation\) if for all combinational circuits \(\iltikzfig{circuits/components/circuits/f-comb}\) and \(\iltikzfig{circuits/components/circuits/g-comb}\), if \(\circuittostream[\iltikzfig{circuits/components/circuits/f-comb}]{\interpretation} = \circuittostream[\iltikzfig{circuits/components/circuits/g-comb}]{\interpretation}\) then there exists a sequence of axioms in \(\mathcal{E}\) such that \(\circuittostream[\iltikzfig{circuits/components/circuits/f-comb}]{\interpretation} \eqaxioms{\mathcal{E}}\circuittostream[\iltikzfig{circuits/components/circuits/g-comb}]{\interpretation}\).
+        We say that a set of equations \(\mathcal{E}\), where each \(e \in \mathcal{E}\) contains at least one gate, is \emph{combinationally complete} for an interpretation \(\interpretation\) if for all combinational circuits \(\iltikzfig{circuits/components/circuits/f-comb}\) and \(\iltikzfig{circuits/components/circuits/g-comb}\), if \(\circuittostream[\iltikzfig{circuits/components/circuits/f-comb}]{\interpretation} = \circuittostream[\iltikzfig{circuits/components/circuits/g-comb}]{\interpretation}\) then there exists a sequence of equations in \(\mathcal{E}\) such that \(\circuittostream[\iltikzfig{circuits/components/circuits/f-comb}]{\interpretation} \eqaxioms{\mathcal{E}}\circuittostream[\iltikzfig{circuits/components/circuits/g-comb}]{\interpretation}\).
     \end{definition}
 
     \begin{example}
         A set of equations combinationally complete for \(\interpretation_\star\) are listed in \cref{fig:combinational-axioms}.
     \end{example}
 
-    \begin{figure}
+    \begin{figure}[p]
         \centering
         \begin{align*}
             \iltikzfig{strings/structure/comonoid/unitality-l-lhs} &\eqaxioms{\mathcal{B}}
@@ -409,7 +422,7 @@
             &\eqaxioms{\mathcal{P}}
             \iltikzfig{circuits/axioms/belnap/de-morgan-2-rhs}
         \end{align*}
-        \caption{A set of equations \(\mathcal{P}\) which is combinationally complete for \(\interpretation_\star\).}
+        \caption{A (not necessarily minimal) set of equations \(\mathcal{P}\) which is combinationally complete for \(\interpretation_\star\), adapted from~\cite{rodrigues1998translation}.}
         \label{fig:combinational-axioms}
     \end{figure}
 
@@ -420,8 +433,8 @@
 
     \noindent
     This allows us to reason \emph{purely equationally} with digital circuits, rather than having to appeal 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}~\cite{ghica2017diagrammatic}; a current thread of work involves reworking this using recent work on rewriting with \emph{hypergraphs}~\cite{bonchi2016rewriting}.
+    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 involves reworking this using recent work on rewriting with \emph{hypergraphs}~\cite{bonchi2016rewriting,kaye2021rewriting}.
 
     \printbibliography[heading=bibintoc,title={References}]