|
58 | 58 | \end{definition}
|
59 | 59 |
|
60 | 60 | \noindent
|
61 |
| - 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. |
| 61 | + 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: the latter can be thought of as `true and false simultaneously'. |
62 | 62 | Using a signature, digital circuits are constructed as morphisms in a freely generated symmetric traced monoidal category (STMC).
|
63 | 63 | To aid in the presentation, we shall use the graphical calculus of \emph{string diagrams}~\cite{joyal1991geometry,joyal1996traced,selinger2011survey}.
|
64 | 64 |
|
|
81 | 81 |
|
82 | 82 | \noindent
|
83 | 83 | The small boxes are \emph{values}: these represent the signals that can flow through our circuits.
|
84 |
| - Next come the generators for each gate symbol in our signature, and three \emph{structural} generators for forking, joining and stubbing wires. |
85 |
| - The final generator is a \emph{delay} generator: one can think of this as delaying its inputs for one tick of the clock. |
86 |
| - We write arbitrary sequential circuits obtained by composing generators together as green squares \iltikzfig{circuits/components/circuits/f-seq}. |
| 84 | + Next come the generators for each gate symbol in our signature, and \emph{structural} generators for forking, joining and stubbing wires. |
| 85 | + The final generator is a \emph{delay} generator: one can think of this as delaying its inputs for one tick. |
| 86 | + We write sequential circuits obtained by composing generators as green squares \iltikzfig{circuits/components/circuits/f-seq}. |
87 | 87 | 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}.
|
| 88 | + To avoid clutter, we occasionally omit the backgrounds of generators. |
88 | 89 | When restricted to the combinational circuits, this work is similar to~\cite{lafont2003algebraic}.
|
89 | 90 | Where the approaches diverge is the inclusion of delay and feedback.
|
90 | 91 |
|
|
95 | 96 |
|
96 | 97 | \begin{definition}[Interpretation]\label{def:interpretation}
|
97 | 98 | Let \(\circuitsignature = (\circuitsignaturevalues,\circuitsignaturegates)\) be a signature.
|
98 |
| - 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}\). |
| 99 | + A interpretation of \(\circuitsignature\) is a tuple \(\interpretation = (\mathbf{V}, \valueinterpretation,\gateinterpretation)\) where \(\values\) is a finite lattice, \(\valueinterpretation\) is a bijective function \(\circuitsignaturevalues \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}\). |
99 | 100 | \end{definition}
|
100 | 101 |
|
101 | 102 | \begin{figure}[p]
|
|
0 commit comments