Diagrammatic Semantics for Digital Circuits
Dan R. Ghica1 , Achim Jung1 , and Aliaume Lopez2
1

2

University of Birmingham
ENS Cachan, Université Paris-Saclay

arXiv:1703.10247v1 [] 29 Mar 2017

March 31, 2017
Abstract
We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large
class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our
symbolic approach is the enabling of automated reasoning about parametrised circuits, with a
potentially interesting new application to partial evaluation of digital circuits. Relative to the
recent interest and activity in categorical and diagrammatic methods, our work makes several
new contributions. The most important is establishing that categories of digital circuits are
Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is
producing a general yet simple graph-rewrite framework for reasoning about such categories
in which the rewrite rules are computationally efficient, opening the way for practical applications.

1

Introduction

Of the many differences between the worlds of software and hardware design, a particularly intriguing one is their prevailing modelling methodologies. The workhorse of software reasoning
— operational semantics [28] — is syntactic and reduction-based. It is essentially an abstract,
entirely machine-independent presentation of a programming language which is not required to be
faithful to the execution model other than insofar as the final result is concerned. On the other
hand, reasoning about hardware relies on having an accurate execution model, akin to what we
would call an abstract machine in programming languages, usually some kind of automaton [21].
To reason about a circuit, it is translated so that its execution is simulated by the automaton. The
abstract machine approach is of course established and useful in programming language theory
as well [23], especially in compiler design. But the operational semantics has several advantages
over the abstract machine approach, of which perhaps the most important is the ability to evaluate programs which are specified only in part. This is useful because many front-end compiler
optimisations are, in one way or another, partial evaluations [8].
Broadly speaking, the main contribution of our paper is to provide an operational semantics
for digital circuits, based on diagram rewriting. Our methodology is influenced by the interplay
between graph rewriting and monoidal categories, which led in the last decade to diagrammatic
models for quantum computing [2], signal flow [5] and asynchronous circuits [12]. Algebraic specifications in the style of monoidal categories have been pioneered by Sheeran in the 1980s [30]
and a certain amount of algebraic reasoning about circuits using such specifications has been attempted [25]. However, a full and systematic categorical presentation of digital circuits has only
been given recently by the first two authors of the present paper [13]. Starting only from an
equational specification of digital components (“gates”) it shows that the free traced monoidal category, subject to certain quotients, is Cartesian. Such categories, known as dataflow categories [29,
Sec. 6.4] (or traced cartesian categories [15]), have very useful equations for iterative unfolding of
the trace [7, 15, 31], offering a convenient way to model feedback.
1

The main theoretical contribution of this paper is providing a rewriting semantics for dataflow
categories with a discrete delay operator. It is well known that an algebraic semantics does not
automatically translate into an operational semantics, because distributive laws (in particular the
functoriality of the tensor product) are directionless. This is where the diagrammatic approach
can help when used as a graphical syntax, by avoiding the need for such problematic laws [4] and
leading to computationally efficient rewriting. The iteration axioms also raise difficulties, this time
of identifying diagrammatic redexes. This problem is compounded by the fact that choosing the
wrong iterators to unfold can lead to unproductive rewrites. Finally, the presence of delays raises
yet a different set of technical challenges because they cannot be rewritten out of a circuit but only
moved around using a retiming axiom [24]. We solve these problems by writing circuit diagrams
in a particular canonical form, which we call global trace delay, for which we can provide effective
and efficient unfolding, with certain guarantees of productivity.
The main motivation of this work is to open the door to new optimisation techniques for digital
circuits, similar to partial evaluation. We will test our theory against a particularly challenging
class of circuits, so called circuits with combinational feedback [26]. These are circuits which, despite
the presence of feedback loops, behave just like combinational circuits, i.e. they exhibit none of the
effects associated with genuine feedback, such as state or oscillation. As is the case with operational
semantics, we will see how handling such circuits is mathematically elementary and fully automated.
This is indeed remarkable, because the conventional automata-based reasoning method does not
accept combinational feedback. Denotational semantics can model such circuits [27] but using
rather complex mathematical machinery. Moreover, we will show how circuits with combinational
feedback which are parametrised by unspecified “black box” components can be just as easily
handled by our approach. As far as we know, there is no existing method for modelling such
circuits (called “abstract circuits”) in the design literature.

2

Categorical semantics

The material in most of this section is presented more extensively in [13].

2.1

Combinational circuits

We introduce a categorical language of circuits. Let object variables, labelling (collections of) wires,
be natural numbers and let morphism variables be labels for boxes (e.g., gates and circuits). This
is a category of PROducts and Permutations (PROP) [22].
Definition 1. Let Circ be a categorical signature with objects the natural numbers N and a finite
set of morphisms which may be grouped into the following three classes:
• levels (or values) v : 0 → 1 forming a lattice (V, v);
• gates k : m → 1; and
• the special morphisms join g : 2 → 1, fork f : 1 → 2, and stub w : 1 → 0.
All circuit signatures include combinators for joining two outputs (join) and duplicating an
input (fork ), as well as the ability to discard an output (stub). What varies from signature to
signature is the number of signal levels and the set of gates. Since levels form a lattice, they must
include a smallest element (⊥), corresponding to a disconnected input, and a top element (>)
corresponding to an illegal output (“short circuit”). In the simplest and most common instance,
the set of level has two other elements, high and low, but it can go beyond that. For example, in
the case of metal-oxide-semiconductor field-effect transistors (MOSFET) it makes sense, in certain
designs, to model the diode properties of the transistor by taking into account four levels (strong
and weak high and low voltage, cf. the relevant IEEE standard for logical simulations [1]).
Circuits, in the sense of this paper, are the morphisms of a free categorical construction over
their signature. Beginning with combinational circuits, the free construction is as follows:
Definition 2. Let CCirc be the free symmetric monoidal category over Circ and monoidal
signature (N, +, 0), and equations:
Fork: f ◦ v = v ⊗ v.
Join: g ◦ (v ⊗ v 0 ) = v t v 0 .
2

Stub: w ◦ N
v = id 0 ,
N
N
Gate: k ◦ i=1,m vi = v, such that whenever vi w vi0 then k ◦ i=1,m vi w k ◦ i=1,m vi0 .
We will call morphisms in this category combinational circuits.
The first three model the fact that a fork duplicates a value, a join coalesces two values, and a
stub discards anything it receives. The gate equations must cover all possible inputs to a gate k
and their particular format entails that the output from a gate is always one of the original levels
in V. Since V is a lattice, the monotonicity requirement is also expressible equationally.
It is known that, in a formal sense, the equality of morphisms in a free SMC corresponds to graph
isomorphisms in the diagrammatic language [18], where diagrams are created by the operations
of sequential composition (◦), parallel composition (⊗) and symmetry (xm,n , the swapping of
two buses with m and n wires, respectively), governed by coherence equations. We will usually
write composition in diagrammatical order f · g = g ◦ f . We
Nwrite the identity
N(bus of width m)
m
id
:
m
→
m
as
simply
m.
For
simplicity
we
also
write
f
=
f
,
i=1,m
i=1,m fi = f and
Nm
v
=
v.
For
lack
of
space
we
will
not
enumerate
the
coherence
equations
here, since they
i=1,m i
are standard.
The Gate axioms state that the behaviour of basic components is fully defined by their inputs,
i.e. they are extensionally complete. By simple inductive arguments on the structure of morphisms
we can establish that all circuits are in fact extensionally complete, i.e. for any circuit (not just
gates)
n, for any values vi , 1 ≤ i ≤ m, there exist unique values vj0 , 1 ≤ j ≤ n such that
N f :m→N
f ◦ i=1,m vi = i=1,n vi0 . Intuitively this means that we only model local interactions, abstracting
away from global effects such as electromagnetic interference or quantum tunelling etc.
We can further say that two circuits with the same input-output behaviour are extensionally
equivalent, and a simple inductive argument shows that this is a congruence, i.e. it is an equivalence
preserved by sequential and parallel composition. Therefore it makes sense to quotient our category
CCirc and create a new category ECCirc in which equivalent circuits are made equal.
ECCirc has interesting additional categorical properties which aid reasoning. Two are of
particular importance. The first one is that ECCirc is Cartesian. The diagonals are defined by
∆0 = 0 and ∆n+1 = (∆n ⊗ f) · (n ⊗ x(1,n) ⊗ 1), forks of width n. The diagonal has two important
coherences represented by the following diagram equalities valid for any diagram f : n → m.
f
=

=

f

f

f

f · wm = wm .

hf, f i = ∆n · (f ⊗ f ) = f · ∆m

Another useful property is that (f, g, w, ⊥) forms what is known as a bialgebra, i.e. an algebraic
structure in which (g, ⊥) is a commutative monoid, (f, w) is a co-commutative co-monoid, such
that g · f = f2 · (1 ⊗ x1,1 ⊗ 1) · g2 :

=

Fork is a section and join a retraction, f · g = 1:

=
They are not generally isomorphisms, except for a special context:
Proposition 1. For any f : m → n + 1, ∆m · f 2 · (n ⊗ (g · f) ⊗ n) = ∆m · f 2 · (n ⊗ 1)2 :
f

f

=
f

f

3

Another useful connector is the join of width n, defined as ∇0 = 0 and ∇n+1 = (n ⊗ x1,n ⊗ 1) ·
(∇n ⊗ g).

2.2

Circuits with discrete delays

Definition 3. Let CCircδ be the category obtained by freely extending ECCirc with a new
morphism δ : 1 → 1 subject to the following equations:
Timelessness: For any gate or structural morphism k : m → n, δ m · k = k · δ n .
Streaming: For any gate k : m → 1 and levels v, (δ m ⊗ v) · ∇m · k = ((δ m · k) ⊗ (v · k)) · ∇1 .
Disconnect: ⊥ · δ = ⊥.
Unobservable delay: δ · w = w.
Timelessness means that compared to δ, all other basic gates and structural morphisms compute
instantaneously. An immediate consequence is that delays can be propagated through combinational circuits, akin to retiming [24]. Disconnect means that the initial conditions of circuits is ⊥,
so that a wire that also promises to dangle later might as well be considered dangling already. The
last rule expresses the same for dangling output wires. Diagrammatically, this is:
k

k

=

The Streaming axiom is more interesting, and it was one of the essential new axioms proposed
in [13]. It is key to capturing the intuition of δ as a delay operator. Mathematically, first observe
that there are infinitely many morphisms of type 0 → 1 in CCircδ , not just the finitely many
values. This is because expressions such as v · δ do not reduce to a value. However, it can be shown
that any expression built from values, δ, and the structural morphisms can be transformed into a
canonical form which may be viewed as a sequence of values presented over time, something that
is called a waveform in hardware design lingo. We write a waveform consisting of n + 1 values as a
list sn = vn :: vn−1 :: · · · :: v0 where vn is the value that is currently visible, vn−1 becomes visible
in the next step, and so on. Formally, s0 = v0 and sn+1 = (sn · δ ⊗ vn+1 ) · g. For example, the
expression v · δ corresponds to the waveform ⊥ :: v; a value v is equal to (any of) the waveforms
v :: ⊥ :: · · · :: ⊥ which
N means thatmit is only
N available now but no longer in the next time-step.
As before, we write
s
=
s
and
i=i,m
i=i,m si = s. In the case of m = 2, the equation is
represented by the diagram:

v
v'

k

k

=
v
v'

k

The Streaming axiom now tells us how a gate processes a waveform: we create two separate
instances of the gate, one to process the immediate inputs and another to process the subsequent
inputs. Applying it repeatedly to a given circuit allows us to determine the waveform that is
produced at the output wires. We obtain:
Theorem 2 (Extensionality). Given any morphism f in CCircδ , for any input waveform s there
exists a unique output waveform s0 such that s · f = s0 .
The proof is given elsewhere [13], noting that Prop. 1 plays a key role.
As in the case of circuits without delays, we can show that extensionality is a congruence and
we can quotient by it, creating an extensional category of circuits with delays, ECCircδ . It is then
a routine exercise to show ECCircδ is Cartesian, with the diagonal and terminal object defined
the same way as in ECCirc.
To conclude the section we will prove a generalisation of the Streaming axiom which will aid the
formulation of the operational semantics. First note is a general diagrammatic reasoning principle
which holds in all free symmetric monoidal categories.
Lemma 3 (Staging). Given a free SMC over a signature Γ, any morphism f can be written as a
sequence of compositions f = f0 · f1 · · · fn where fi is a tensor including exactly one non-identity
morphism, fi = m ⊗ k ⊗ n.
4

Proof. By diagrammatic reasoning, repeatedly rearranging the diagram as:
f
h

f
h'

=

h

g

h'
g

Let us call passive a circuit which has no occurrences of a value.
Lemma 4 (Generalised Streaming). For any passive combinational circuit f : m → n, (δ m ⊗ m) ·
∇m · f = (f · δ n ⊗ f ) · ∇n .
Proof. We make an extensional argument and use the Staging Lemma (3) and induction on the
number of stages. Each stage is combinational. For each stage, the property is immediate from
Streaming and Timelessness.

2.3

Circuits with feedback

Definition 4. Let CCirc∗δ be the category obtained from ECCircδ by freely adding a trace
operator.
Diagrammatically, the trace operator applied to a diagram f : m + k → n + k corresponds to a
feedback loop of width k, written Trk (f ) : m → n. Symmetric traced monoidal categories (STMC)
satisfy a number of equations (coherences) which we will not enumerate for lack of space [19].
As before, their interpretation coincides with equality of diagrams (with feedbacks) up to graph
isomorphism.
As before, we are committed to an extensional view of circuits where the only observable is the
input-output behaviour. In combinational circuits, with or without delays, the only way we can
create a circuit with 0 outputs is by explicitly composing a circuit f : m → n with wn . However,
0-output circuits can arise in more complicated ways in the presence of feedback, whenever all the
outputs are fed back. For example, the diagram on the left can be reduced to just three unobserved
inputs:
k'
k

=

k"

Such equalities cannot be proved out of local interactions, so we will simply impose the equivalence
of all 0-output circuits, an equivalence which is trivially a congruence. The new quotient category
is called OCirc∗δ . In this category all diagrams of shape f : m → 0 are therefore equal which,
categorically speaking, makes 0 a “terminal object”.
In general, in programs feedback corresponds to recursion and iteration, and syntactic models
(operational semantics) of such programs involve creating two copies of the code recursed over. For
example, the operational semantics of the Y-combinator as applied to some G is Y G = G(Y G).
A similar rule does not exist in general for SMTCs unless the category is also Cartesian. Such
categories, also called data-flow categories [7], admit an iterator defined for any f : m + n → n:

f
n

n

iter (f ) = Tr (f · (∆n ⊗ n)) : m → n
which satisfies the following equations:
f

Naturality: iter((g⊗n)·f ) = g·iter(f ) for any g : k → m.

g
f

Iteration: iter(f ) = hm, iter(f )i · f

5

=
=

g

f

f

f

f

=

f

Diagonal : itern (itern (f )) = itern ((hn, ni ⊗ m) · f ).
Naturality justifies treating diagrams containing the iterator graphically, just as we are used to
from SMTCs. Let us also state formally that the precondition for the iterator is fulfilled by the
SMTC of circuits with feedback:
Theorem 5 ([13]). The category OCirc∗δ is Cartesian with diagonal ∆n .

2.4

A model for OCirc∗δ

To conclude the section, we sketch the construction of a model for OCirc∗δ which will confirm the
intuition we have alluded to above. It needs to be Cartesian and support the delay operator and
iteration. The usual example of a traced SMC, sets and relations, is not Cartesian so a slightly
more complex construction is required. We start with a basic model for combinational circuits
based on the lattice V of values (Def. 1).
Definition 5. Let V be the category whose objects are finite powers of V and whose morphisms
are monotone maps.
Proposition 6. V is cartesian, i.e., it has finite products.
For each basic gate k, V contains the concrete monotone function describing its input-output
behaviour. The special morphisms join, fork, and stub are represented by t, the diagonal into
the product, and the unique map into the one-element lattice V0 , respectively; all of these are
monotone. Since CCirc is freely generated by the basic gates, we have:
Proposition 7. There is a unique monoidal functor J·KV from CCirc to V mapping the object 1
of the former to V of the latter.
It is a trivial exercise to check that the equations given in subsection 2.1 are satisfied in V, so
J·KV factors through the extensional category ECCirc.
To model the delay operators, we replace V by S = VN , the N-indexed product of V with
itself. Its elements are streams of elements of V. This is an infinite lattice, the order being defined componentwise, and it makes sense therefore to stipulate that morphisms preserve not just
the order but also suprema of directed sets. Thus we have the category S of finite powers of S
with Scott-continuous maps between them. As before, we immediately obtain that S is cartesian. The interpretation of gates and special morphisms is component-wise: JkKS (s1 , . . . , sm )[n] =
JkKV (s1 [n], . . . , sm [n]), where we are reusing the semantics of gates inside V. Values (= levels)
are interpreted as those streams that have the corresponding semantic value in first position and
bottoms after that, which we write as v. The following is obvious because the gate operations are
defined componentwise:
Proposition 8. The semantic gate functions JkKS are Scott-continuous.
Delay. In the stream model we interpret delay by shift:

⊥
if n = 0
JδKS (s)[n] =
s[n − 1] otherwise

Again, it is easily seen that this is a Scott-continuous operation from S to S.
The soundness of the timelessness rule (Def. 3) is now easily checked; it holds because gates
act componentwise on streams and whether we shift the input streams or the output streams is
immaterial. Streaming is more interesting. In the case of m = 1, we want to show
Jδ⊗v · g · kKS = J(δ · k)⊗(v · k) · gKS

so let v ∈ V be a value and s ∈ S a stream. Consider first the head position of the output stream.
The left hand side evaluates as
Jδ⊗v · g · kKS (s)[0]

=
=
=
=
6

Jg · kKS (JδKS (s), v)[0]
JkKS (JδKS (s) t v)[0]
JkKV (⊥ t v)
JkKV (v)

and the right hand side as
J(δ · k)⊗(v · k) · gKS (s)[0]

= t(JkKV (⊥), JkKV (v))
= JkKV (v)

where the last equality holds because by monotonicity we know that JkKV (⊥) v JkKV (v) and hence
the supremum is the larger of the two. The same argument is used for all other positions n > 0:
Jδ⊗v · g · kKS (s)[n]

=
=
=
=

JkKV (s[n − 1] t ⊥)
JkKV (s[n − 1])
JkKV (s[n − 1]) t JkKV (⊥)
J(δ · k)⊗(v · k) · gKS (s)[n]

It is clear from the semantics of the delay operator that a circuit with n delay operators takes
account of (at most) the inputs s[m − n], . . . , s[m − 1], s[m] when computing the m-th output value.
Thus we have the following full characterisation of extensional equality:
Proposition 9. Two circuits f and g, which both contain no more than n delay operators, are
observationally equivalent if and only if they produce the same outputs for all waveforms of length
up to n + 1.
Feedback. Iteration can be added toFV already. Let f : Vm+n → Vn be a monotone map.
¯ and Φ(k + 1, f, ā) =
Define fix(f ) : Vm → Vn by fix(f )(ā) = k∈N Φ(k, f, ā), where Φ(0, f, ā) = ⊥
f (ā, Φ(k, f, ā)) (and ā is short for a1 , . . . , am ). The definition of fix(f ) in S is very similar, the
only difference being that we start the iteration with the constant bottom stream ⊥ on each of the
n inputs.
In interpreting circuits with feedback, we let fix be the semantics of iter.
Proposition 10. fix satisfies the three equations for the iterator.
Remark. This fact is mentioned (without proof) in Example 7.1.2 of [15] but for the convenience
of the reader we include the argument.
Proof. The first equation, Naturality, is a straightforward calculation:
G
fix((g ⊗ n) · f )(ā) =
Φ(k, (g ⊗ n) · f, ā)
k∈N

(g · fix(f ))(ā) = fix(f )(g(ā)) =

G

Φ(k, f, g(ā))

k∈N

The two chains on the right are term-wise identical as one sees by induction over k: For k = 0 we
¯ in both cases and for k + 1 we have
get ⊥
Φ(k + 1, (g ⊗ n) · f, ā) = ((g ⊗ n) · f )(ā, Φ(k, (g ⊗ n) · f, ā)) = f (g(ā), Φ(k, (g ⊗ n) · f, ā))

and

Φ(k + 1, f, g(ā)) = f (g(ā), Φ(k, f, g(ā)))
which are equal by induction hypothesis.
equation, Iteration, holds because all maps in S are Scott-continuous and therefore
F Thek second
¯ is a fixpoint of g:
g
(
⊥)
k∈N
f (ā, fix(f )(ā)) = g(

G

¯ =
g k (⊥))

k∈N

G
k∈N

¯ =
g k+1 (⊥)

G

¯
g k (⊥)

k∈N

The left-hand side of the third equation, Diagonal, can be re-written into a system of simultaneous
equations by Bekič’s rule, and these precisely describe the right-hand side.

7

Note that in the case of V the computation of the supremum takes place in the finite lattice
Vn . This means that the terms Φ(k, f, ā) can only take finitely many different values, or in other
words, that the supremum is obtained after finitely many iterations. This agrees with intuition:
As the circuit is powered up, the potential in all wires stabilises after a (very short) finite delay;
there is no possibility of infinite oscillation. In the case of S the same holds for every component
of the output, although the (mathematical) iteration will typically take infinitely many steps to
produce all components of the output stream.
A Cartesian category admits an iterator (satisfying the three equations listed above) if and only
if it is traced. This result appears in [15, Section 7.1] where it is credited to Martin Hyland. The
following is now an immediate consequence of this and the fact that CCirc∗δ is the free symmetric
traced monoidal category over Circδ :
Proposition 11. There is a unique traced monoidal functor J·KS from CCirc∗δ to S mapping the
object 1 of the former to S of the latter.
In the presence of delay and feedback, even an input waveform of finite length can produce
an infinite output stream. However, such an output stream must be eventually periodic. This
is because the output at any point in time is completely determined by the contents of the delay
components and the inputs at that time. A circuit can only contain finitely many delay components
n
(say n many) and so the “internal memory” can only assume k = |V| -many different states. Any
input stream that is longer than k must lead to at least one internal state re-occurring. In other
k
words, if we provide such a circuit with all possible input streams of length k (there are |V| -many)
then we are guaranteed that the circuit has assumed all possible internal states it can ever assume.
This means that if we test for the output from one more input after all these initial waveforms
then we have tested the circuit under all possible internal configurations. We have shown:
Proposition 12. Two circuits with feedback f and g, which both contain no more than n delay operators, are observationally equivalent if and only if they produce the same outputs for all
n
waveforms of length up to |V| + 1.
Propositions 9 and 12 give an exponential and a superexponential upper bound, respectively, for
the number of tests required for checking the equivalence of circuits. They provide the background
against which we present the much more efficient diagrammatic operational semantics below.
The semantics also suggests other equations, not considered in this paper, for example, the
following always holds
G
G
G
¯ =
¯ =
¯ .
g k (⊥)
g k+1 (⊥)
g k (g(⊥))
k∈N

k∈N

k∈N

On diagrams, this equations does not seem to lead to productive re-writes, but it does point to
additional reasoning principles.

3

Diagrammatic operational semantics

The results of the previous section establish a powerful framework for algebraic reasoning about circuits. However, this framework is not equally useful for automatic reasoning and cannot implement
a reasonable operational semantics.
The first obstacle is the functoriality property of the tensor, which lacks directionality. Consider
the circuit corresponding to the boolean expression t ∧ f ∧ t, where the constants involved satisfy
the obvious equations. This diagram can be specified in several ways. Some of the specifications,
e.g. (((t ⊗ f ) · ∧) ⊗ t) · ∧ have the immediately identifiable redex (t ⊗ f ) · ∧ = f which reduces the
overall expression to (f ⊗ f ) · ∧, which reduces to f . However, the same circuit can be equivalently
written as (t ⊗ f ⊗ t) · (∧ ⊗ id) · ∧ which has no obvious redex.

8

t

t

^

f

^ =

^

f
^

t

t

Finding redexes in such structural diagram specifications is computationally prohibitive and an
unsuitable operational semantics. The alternative is to exploit the connection between monoidal
categories in general, and traced monoidal categories in particular, and certain graphs. This idea
has been analysed in depth recently [4].
We will give a concrete presentation of the graphs following Kissinger’s framed point graphs,
which are a free (strict) symmetric traced monoidal category [20, Thm. 5.5.10]. To make the
presentation more accessible we will elide some of the categorical technicalities in loc. cit. and give
a more direct presentation.
Let a labelled directed acyclic graph (LDAG) be a DAG (V, E) equipped with a partial labelling
function f : V * L. Let a labelled interfaced DAG (LIDAG) be a labelled DAG with two
distinguished lists of unlabelled nodes representing the “input” and “output” interfaces. LIDAGs
can be visualised as
O

I

Unlabelled nodes are called wire nodes and edges connecting them are called wires. A wire homeomorphism [20, Sec. 5.2.1] is any insertion or removal of wire nodes along wires, which does not
change the shape of the graph. Two LIDAGs are considered to be equivalent if they are graph
isomorphic up to renaming vertices and wire homeomorphisms. The quotienting of LIDAGs by
this equivalence gives us framed point graphs (FPG) [20, Def. 5.3.1]. The algebraic specifications of
the diagrams associated with the expression t ∧ f ∧ t mentioned above all correspond to the (same)
framed point graph with empty input interface and 1-point output interface.
t
⋀

f
⋀
t

This representation solves the problem raised by the functoriality of the tensor. Moreover, the
graph representation can be made canonical by eliminating all redundant wire nodes efficiently (in
linear time in terms of the size of the graph). In the PROP with FPGs as morphisms, composition,
tensor and trace can be represented visually as below.
Sequential composition of two FPGs where the size of the output of the first matches the size
of the input of the second is defined by identifying the output list and the input list of the two
graphs. Since FPGs are equal up to renaming of vertices, the names of the wires can be chosen so
that the composition is well defined. The unlabelled input and output nodes become wire nodes
in the composition.
I₁

O₁=I₂

O₂

The tensor is the disjoint union of the two graphs. It is always well defined since graphs are
identified up to vertex renaming.
I₁

O₁

I₂

O₂

9

The trace operator picks the head nodes of the input and output lists of points, makes them wire
nodes, and connects them.

tl(O₁)

tl(I₁)

The graph representation provides a solution for dealing with the functoriality of the tensor, but
the presence of feedback raises a new, additional problem. Suppose that we deal with a graph
which includes several iterations, e.g. iter(f ) · iter(g).
f

g

This graph raises two computationally difficult questions. The first one is how we identify feedback
patterns efficiently so that we can apply the iteration axiom. The second one is, if there are several
instances of the iteration unfolding axiom that can be applied, what is the schedule of applying
them? Without a good (linear time) solution to the first problem we cannot claim that we have
a genuine operational semantics. Without a good solution to the second problem we run into
technical problems of confluence. Diagrammatic representation alone is no longer the solution.
The main contribution of this section is showing how to solve these two problems.
Lemma 13 (Global trace form). For any morphism f in a free STMC there exists a trace-free
morphism fˆ such that Trn (fˆ) = f for some n ∈ N.
Proof. The proof is by diagrammatic reasoning1 . The same diagram can be created either by
applying a trace locally or globally for any g : m + m0 → p1 + p2 + p3 , f 0 : n + p2 → n + p02 ,
h : p1 + p02 + p3 → m + n0 :
Trm (g; (p1 ⊗Trn (f 0 )⊗p3 ); h) = Trm+n ((n⊗g); (xn,p1 ⊗p2 ⊗p3 ); (p1 ⊗f 0 ⊗p3 ); (xp1 ,n ⊗p02 ⊗p3 ); (n⊗h)).

f'

g

h

f'

g

=

h

Since diagrams are finite, this rewrite can be repeated to write the diagram as a global trace applied
to a trace-free morphism fˆ.
So a diagram with feedback loops can always be rewritten as single, global, feedback loop.
In the graph we can maintain a distinguished subset of known feedback wire nodes so that the
feedback loops can be immediately identified. This can be done compositionally just by keeping
track of the feedback wire nodes in sequential composition, tensor and trace.
The most interesting case is of the trace:
T

T

I

1 This

O

tl(I)

can be done algebraically, of course, but it is much less clear.

10

tl(O)

The wire homeomorphism rules allow us to place exactly one wire node in the set of feedback wire
nodes. By maintaining the feedback wire nodes explicitly we can ensure two useful invariants.
First, the rest of the graph is a DAG. Second, for each feedback wire node there is precisely
one incoming and one outgoing edge. We call these graphs trace-framed point graphs (TFPGs).
Note that feedback wire nodes must not be entirely removed as wire homeomorphisms are applied.
Feedback edges that bypass the set of feedback wire nodes are legal, but break the TFPG form.
Maintaining these restrictions is computationally trivial (constant overhead).
We are now in a position to define the diagrammatic operational semantics as a graph-rewriting
system in which each rule can be applied efficiently, in linear time as a function of the size of the
graph.
Given a categorical signature Circ we use the levels and the gates as labels, along with labels
denoting discrete delays and stubs as well as a set of labels ik , k ∈ N denoting distinguished input
ports for gates. For readability we usually omit the labels and for join, fork, and its input ports.
i₀
k
i₁

k:2→1

f:1→2

j:2→1

A circuit specified as a morphism is a TFPG. We add the following rewrite rules corresponding to
the categorical axioms. Note that each rule can be applied in linear time, including the identification
of the redex.

3.1

Combinational rules

The diagrammatic semantics will be given as a collection of graph-rewriting rules. We give the
rules in an informal diagrammatic style, but a formalisation in an established formalism such as
DPO [9] is a standard exercise.
Constant. The basic rule is the reduction of a gate with known input levels. If v · k = v 0 then
i₀

v₀

k

v'

i₁

v₁

Enhanced Constant Rules. Besides the basic equations for constants, more equations can be
proved by extensionality in which reductions can be carried out without all input values being
present. For example, true ∨ x = true or true ∧ x = x. These equations are admissible in the
rewrite system.
Fork. In contrast, the forking of a wire means copying the value attached to it. Forking has w
as a co-unit.
v
v
v

v
s

δ

The rules below are for waveforms, where v :: s is the circuit diagram
. Note
that waveforms are simple sub-graphs that can be identified in the overall circuit diagram in linear
time.
Streaming. For any values v, v 0 , waveforms s, s0 and constant k

11

v

v

i₀

v'

i₁

k

i₀

δ

k
i₀

v'
i₁

k

δ

δ

i₁

Stub. We omit the label and the input port of the stub w, for readability. For any constant
k : m → 1,

...

...

k

We call the rewrite rules above the local rewrite rules. A TFPG where no local rewrite rules apply
is in canonical form.
Proposition 14. The local rewrite rules are sound.
If the graph on the left is a representation of a morphism f then the graph on the right is a
representation of a morphism g and f = g in ECCirc. The proof is immediate.
Lemma 15. The local rewrite rules are terminating.
Proof. TFPGs are finite. All rules reduce the sum of path lengths to the input. In the case of
input we assume that the new redex corresponding to the term (v ⊗ v 0 ) · k is reduced as well.
Lemma 16. The local rewrite rules are strongly confluent.
Proof. Given a TFPG so that more than one local rewrite rule is applicable we first note that for
all rules other than Stub the redex subgraphs must be disjoint, so they commute trivially. But
the Stub rule also commutes, obviously, with any other rule. It follows that the system is strongly
confluent.
Lemma 17 (Progress). A circuit f : 0 → n, n 6= 0 without traces or delays is either a value or the
TPFG associated with it has redexes.
Proof. A trace-free circuits of type 0 → n must have form v · g for some g. If the TPFG representation of g consists just of identities then by wire homeomorphisms we have a representation of
a value. If the TPFG contains a constant, or a node structure corresponding to join or fork, the
input nodes must connect directly to constants so there are redexes.
From Lem. 16 and 17 it follows that
Theorem 18. Given a circuit f : 0 → m, m 6= 0 in ECCirc the local rules will always rewrite its
TPFG representation in a finite number of steps into a TPFG representation of a value v such
that f = v.

3.2

Feedback and delay

We now need to add rules to ensure to deal with delays which occur in arbitrary places in the circuit,
not just in waveforms. For example, a circuit such as (t ⊗ f ) · (1 ⊗ δ) · ∧, in TFPG representation,
does not have any redex because of how the delay is placed. Dealing with the delays requires a
complex rule which takes into account the presence of the trace. The trace and the delay must
be dealt with together because of the following result which allows us to write any circuit in what
we will call global-delay form. Note Lem. 4 does not hold for combinational circuits with values.
However, the following holds:
Lemma 19. For any combinational circuit f : m → n there exists a passive circuit f˜ such that
f = (m ⊗ v) · f˜ for some v.
12

Proof. The proof is immediate by diagrammatic reasoning, by applying this transformation for
each occurrence of a value v:

f'

f'

=

f''

v

f''

v

We call the application of the transformation in this lemma the passification of the circuit.
Lemma 20. Any circuit f in OCirc∗δ can be written as f = Trm ((δ n ⊗ p) · f 0 ) for some trace-free,
delay-free circuit f 0 , m, n, p ∈ N.
Proof. The proof is diagrammatic. All diagrams can be rewritten in the following, isomorphic,
shape:

δ
g

δ

h

h

g

=

Trace-Delay. The most complex rule is the unfolding of the global trace, which also handles
the delays. We will explain it before stating it.
The first step is to derive an unfolding axiom for trace from the unfolding axiom for iteration, by
expressing trace in terms of iteration. This is possible using the co-monoid f and its co-unit w [15]:
A

A

A

=

f
X

A

f

Y

X

Y

TrA (f ) = iterA⊗Y ((idA ⊗ wY ⊗ idX ) · f ) · (wA ⊗ idY ).
The right-hand side is an iteration which we unfold, and then simplify:
A

A

A

f
X

A

f
Y

X

Y

=

A

A

A

Y

X

f
X

A

f
Y

If used as an operational semantics, the rewrite rules will apply to representations of circuits which
have known inputs, so their input interface is empty (closed circuits). We will concentrate on this
usage of the rewrite system, for now. In the case of optimisation for partial evaluation the more
general unfolding provided above can be used.
In the case of closed circuits the unfolding of the trace is shown in Fig 1. Step (1) represents the
unfolding of the trace. The delays are all managed separately, so step (2) passifies the combinational
circuit f (Lem. 19). Step (3) uses ⊥ as the unit of the join-monoid along with the Unobservable
Delay axiom, to bring the circuit to a form where Generalised Streaming (Lem. 4) can be applied
(Step (4)). A final simplification removes redundant delays which are not observable (Step (5)). A
final step (not shown) moves the delays on the output of f to restore the global-delay form, using
Lem. 20. The resulting circuit can be represented as a TFPG.
Wire homeomorphisms. We know that wire homeomorphisms can be applied efficiently, bringing
the graph to a normal form [20, Lem. 5.2.10]. However, we have prohibited the elimination of
feedback nodes using these wire homeomorphisms. Instead we use an explicit rule that “unwinds”
feedback loops if and only if they reach a value v. This rule results in the removal of a wire feedback
node. A similar rule propagates stubs across feedback loops.
13

δ

(1)

f

δ

(2)

δ

f

=

δ

δ

f

=

f

~
f

v
⊥

(3)

δ

~
f

δ

f

=

⊥

δ

⊥

v
δ
δ

(4)

δ

⊥
⊥

f

=

⊥
v

(5)

δ

⊥
⊥

f

=

⊥
v

δ

~
f

δ

~
f

~
f

δ

~
f

Figure 1: Unfolding a circuit in global-delay form

v

v

v

v

The wire homeomorphism is a “tidy-up” rule which does not play a key role in the proof of our
main results about the rewrite system, but is practically useful as it reduces the size of the graph,
a form of garbage collection.
We define the overall rewriting system as a cycle of local rewrites until canonical form is reached,
followed by trace-delay unfoldings. This system is obviously not terminating, which is consistent
with the fact that circuits with feedback can generate infinite waveforms. E.g., iter(v :: 1) = v ::
iter(v :: 1) = v :: v :: iter(v :: 1) = · · · . which diagrammatically corresponds to (up to graph
isomorphism and wire homeomorphism, to keep the representation simple):

v

δ

v

δ

δ
v

v

δ

δ
v

δ
v

14

δ

(1)

δ

=

f

f
⊥

=

δ

f

δ

~
f

v

(2)

δ

~
f

⊥

~
f

⊥

δ

v'

Figure 2: Proof of Thm. 21.

3.3

Productivity

In a circuit of the form v :: f = (v⊗(f ·δ))·g value v will be observed before whatever the behaviour
of f is, since v is instantaneous whereas f is guarded by a delay. We call such circuits productive,
and we add a labelled rewrite rule to simplify productive circuit by removing the produced value
v

v :: f =⇒ f.
This rule is sound because the sub-circuit v :: − can never be part of any redex. So the example
above can be written as
v

iter(v :: 1) = v :: iter(v :: 1) =⇒ iter(v :: 1).
However, we note circuits need not be productive in general. There exist circuits where unfoldings never reduce to shape v :: f . Take, for example, the unfolding of t · iter(∧):

t

^

t

^
t

^

This is a well known problem caused by a genuine instant feedback loop between the output and
one of the inputs of the gate. If a circuit has no instant feedback loops, it is guaranteed to be
productive.
Definition 6. We say that a circuit has delay-guarded feedback if its global-delay form is Trm (δ m ·
f ).
If a circuit has delay-guarded feedback loops then it is productive. In fact it implements a
Mealy automaton.
Theorem 21. Delay-guarded circuits with no inputs are productive. Given the TPFG representation of a delay-guarded feedback, the rewrite system will produce a TPFG graph representing a
circuit v :: g in a finite number of steps.
Proof. The proof can be expressed diagrammatically as the sequence of equal diagrams in Fig. 2.
Step 1 is the unfolding of the global-delay form trace, with no instant feedbacks. Step 2 is the
extensionality property of (⊥m ⊗ v) · f in ECirc, which must reduce to a value v0 , combided with
the non-observability of delay axiom. Because the final diagram represents a circuit of the form
v0 :: − it is by definition productive.
The rewrite system will successfully produce the final circuit because in computing the canonical
form, the sub-circuit ⊥m · f is delay free and trace free so Lem. 17 ensures that it will reduce to
value v.
15

With a delay, the unproductive example t · iter(∧) becomes the productive t · iter((δ ⊗ 1) · ∧)
which, after a series of routine calculations can be shown to reduce to a productive circuit of
shape ⊥ :: f .
Note that the delay-guarded feedback condition is sufficient but not necessary. An interesting
example of circuits with non-delay guarded feedback which are productive are the cyclic combinational circuits which we discuss in Sec. 4.1 below.
To wrap up the operational semantics we also give a necessary and sufficient non-productivity
criterion, to prevent needless unfoldings of the circuit.
Theorem 22. If a circuit has the shape in Fig. 1 and is unproductive then all further unfoldings
of the trace will be unproductive.
Proof outline. Let a circuit as in Fig. 1 (Step 5) be unproductive. Suppose that we unfold the
trace again. The resulting circuit will look as in the diagram below. The sub-circuit drawn as a
cloud is irrelevant for productivity because all its outputs are guarded by delays – so we can omit
it.
δ
δ

⊥

f

⊥

~
f

v

~
f

v

If this circuit is to be productive then the circuit framed by the dotted line must reduce to
a value. But this contradicts the hypothesis, because if the first (on the left) occurrence of the
sub-circuit f˜ can reduce to values, then it could have reduced to values before the unfolding of the
circuit. So the unfolded circuit must be also unproductive.

3.4

Example: Cyclic combinational circuits

A challenging class of circuits, which cannot be handled by standard tools, are combinational
circuits with feedback which is not delay guarded [26]. Consider Boolean circuits with and and or
gates. The following is an example of such a circuit:
z

x'

x'

V

x'

x'

V

Closing the circuit by applying a boolean value at the input makes it possible to apply the diagrammatic operational semantics, using the enhanced equational rewrite rules:

V

T

T

V

V

T

T

V

Finally, we unfold the (superfluous) loop:

T

T

T

The circuit above reduces to True, by applying the co-unit of fork and the Stub rule several times.

16

4

Specialising abstract digital circuits

If we are not using the rewrite rules as an operational semantics, and so are not concerned with productivity issues, we can apply the reduction rules to open and to parametrised circuits. This gives
us a basis for powerful partial evaluation-like optimisations of circuits. This is a new contribution
with potentially interesting practical applications.

4.1

Abstract cyclic combinational circuits

Consider the circuit represented by the TFPG below (highlighting feedback nodes in red), where
the gate m is a multiplexer and F, G are abstract circuits. For readability we omit the input labels
of the multiplexer.
x'

m
x'

G

x'

x

z

x'

x'
z

y
x'

x'

m

x'

m

F

This circuit, presented in [26], implements the operation if x then F(G(y)) else G(F(y)). The circuit
has no delays so the feedback loops are combinational, so they cannot be handled by conventional
circuit analysis tools. However, the multiplexers are set up so that no matter what the value
applied at x, the residual circuit is feedback-free. The false feedback loops in the circuit are only
a clever way to reuse the two abstract circuits F and G.
Consider the case when x becomes t:
x'

m

G

x'

t
x'

z

x'
z

y
x'

x'

m

x'

m

F

Fork and enhanced equational rewrite rules for m lead to:
x'

m

G

x'

t
x'

z

x'
z

y
x'

x'

m

x'

m

F

The Stub rule repeatedly applied results in a circuit which can be written as, to emphasise the
residual feedback loop:
x'

x

y

G
z

z'

y

y'

F

To the naked eye the circuit above is obviously feedback-free, being equal to G · F . However, the
rewrite rules have no way to eliminate feedback wire nodes in this TPFG and we need to unfold
the circuit:
17

z

y

z

y

x'

y

F

G

y'

F

G

The Stub rule will remove the first occurrence of F and the second occurrence of G, resulting, as
expected, in G · F .

4.2

Pre-logical circuits

The diagrammatic semantics can also model operationally transistor-level circuits, which is also a
new development.
The circuit framework is general enough to allow operational reasoning about digital circuits
at a level of abstraction below logical gates, for example metal-oxide-semiconductor field-effect
transistor (MOSFET) circuits. In saturation mode such transistors can be considered to take on
a discrete set of values which, depending on the circuit and the analysis, can be four-valued (high
impedance < high, low < unknown.) or six-valued (high impedance < weak high, weak low ; weak
high < strong high; weak low < strong low ; strong high, strong low < unknown.). Unlike Boolean
logic, where the wire-join construct is not used, in a transistor circuit output wires are joined, and
the semantics of the wire-join is that of the value-lattice join operator.
We will work in the six-value lattice ⊥ (high impedance), h (weak high), H (strong high), l (weak
low), L (strong low), > (unknown). We will take the (idealised) nMOS and pMOS transistors as
the basic gates. The nMOS transistor (n : 2 → 1) works like a low-activated switch, but it only
allows low current to flow. High current can flow, but is much diminished. The defining equations
are
(L ⊗ L) · n = L

(L ⊗ l) · n = l

(L ⊗ H) · n = h

(L ⊗ h) · n = ⊥

(H ⊗ v) · n = ⊥

(v ⊗ v 0 ) · n = >, if v 6= H, L.

(v ⊗ >) · n = >
The pMOS transistor (p : 2 → 1) is activated by the h value and allows low L value to pass, so the
equations are the converse of their nMOS counterparts.
When implementing a logical gate in MOSFET we want H to correspond to true and L to false.
The correct behaviour of a gate must keep this representation without, e.g. producing > or weak
output h, l.
A very simple circuit is the inverter (inv), given in conventional schematics and as a TFPG.
The syntactic description is inv = f · (1 ⊗ h ⊗ 1 ⊗ l) · (p ⊗ n) · g.

z'

H

z'

z'

L

p

z'

z'

n

We can see via a sequence of rewrites that this circuit correctly maps H to L and vice-versa. For
example:
H
H

z'

p

H
L

n

z'

z'

H
H

p

z'

z'

⊥

z'

z'

z'

L
n

L

L

Let us now revisit the example of the previous section, but with the multiplexer implemented
down to transistors. Let pass be a pass-through gate and m a multiplexer:
pass = f2 · (inv ⊗ 3) · (1 ⊗ x ⊗ 1) · (p ⊗ n) · g
m = (f ⊗ 2) · (1 ⊗ x ⊗ 1) · (2 ⊗ inv ⊗ 1) · pass2 · g.
18

L

P2

P1

N

P1

P

P1

H

L

P2

P1
P1

H

N
P2

P2

N

P1

P2
P2

H

P

P
P2

H

H

P1

L

P2

Z

P1

P

N

P1

N

P1

B

P

P2

P1
L

L
P2

H

P1

P1

N

P1

P

H

N

P1

P

⇒

P1

P2

P2

P

P

P1
H

P2
P2

P1

N

P1

P

P2

N

P2

P

B

L

P2
L

P1
H

H

N

P2

P2

P

L

P1

P
P1

P1
H

H

N

P2
P1

H

H

P1

P2

P2

H
P2

H
H

L

N

P2

N

P2

L

N

P1

P2

P1

P2

N

P2

P

B
Z

Z

P1
L

P1

B

P2

P1

N

P1

P

P1
P

H
H

P2

P2
P1

H

N

P2
H

P2

Figure 3: MOSFET implementation of the circuit in Sec. 4.1, and the residual circuit after partial
evaluation
The resulting TFPG has too many nodes to reduce by hand but we have implemented a prototype
tool for partial evaluation by rewriting, available for download2 .
The abstract circuit of the previous section is represented as a TFPG in the first graph in Fig. 3.
The residual circuit after partial evaluation is shown as the second graph. It is interesting to note
that the MOSFET version of the circuit leads to a different residual circuit compared to the more
high level circuit of the previous section. The reason is that we do not use any enhanced rewriting
rules, so the residual circuit contains some irreducible pass-through gates.

5

Conclusion, related and further work

Some theoretical ingredients we have used in this work have been around for quite a while and it
is perhaps somewhat surprising that they have not been put together for a coherent operational
and diagrammatic treatment of digital circuits. Our Thm. 5 implies that OCirc∗δ is a Lawvere
theory [10] with trace, also known as an iteration theory [11], a concept which has been studied
extensively [3], leading to recent connections with rewrite systems [14]. The relation between trace
and iteration has also been studied before in a somewhat similar categorical setting [16]. The
connection between Lawvere theories and PROPS has also been recently studied [6].
We have been in particular inspired by the deep connections between monoidal categories
and diagrams [29] which inter alia have been used in the modelling of quantum protocols [2] and
signal-flow graphs [5]. Some contrasts are quite interesting. Unlike in quantum protocols, all digital
circuits with no inputs and no outputs are equal whereas in quantum computing they correspond to
scalars, which allow quantitative aspects to be expressed. Should we have taken a similar direction
we could have included quantitative aspects such as power consumption in our formalism, but we
would have lost the diagonal property. Obviously, two copies of a circuit will at least sometimes
consume more power than one copy.
The signal-flow graphs in [5] are linear and reversible, which is not the case for digital circuits. Without elaborating the mathematics too much, a key difference between their model and
ours can be illustrated by the following equality, involving the interaction between fork, join, and
disconnected wires, as a trace can be created out of a fork and a join:
f

=

f

Of course, by comparison, in our setting the directionality of the wires never changes, so the correct
equality is:
f

=

f

These simple diagrammatic equations above truly capture the essential difference between electric
and electronic circuits!
2 https://github.com/AliaumeL/circuit-syntax

19

It is also quite surprising that despite major early progress in the algebraic treatment of circuits,
[30, 25], this line of work has not come earlier to a systematic conclusion. But the contribution
of our work is not merely assembling off-the-shelf components. The Streaming axiom is new,
and the fact that it generalises to arbitrary passive combinational circuits is a crucial ingredient
for our work. To make the unfolding of iteration computationally tractable, the diagrammatic
representation required a non-obvious canonical form, which must be easy to compute. Without
it our earlier semantics [13] cannot be used as an effective operational semantics.
Beyond the scholarly context and technical innovations, we are most excited about the potential
applications of our work. Cyclic combinational circuits are a litmus test for circuit modelling
theories and we hope the reader can appreciate that in our framework their model is elementary. For
comparison, there are few theories that can handle such circuits, and they demand a significant level
of mathematical sophistication [27]. The true potential of our method is unleashing of symbolic,
operational and syntactic methods, such as partial evaluation, for reasoning about and optimising
circuits, methods which proved so effective in programming languages.
There is work to be done, from exploring theoretical questions to implementing more efficient
circuit-rewriting tools. The most interesting theoretical questions involve the extensionality and
characterisation of circuits with feedback. We do not have yet equivalents of Thm. 2 for circuits with
delays and feedback. These theorems would play an important role in dealing with circuits with
instant feedback which are currently unproductive in the graph rewrite system, such as t · iter(∧)
or infinitely productive such as iter((1 ⊗ v) · δ), by developing meta-theoretic reasoning principles
for such graphs. In the concrete category (Sec. 2.4) we can see that the first circuit is equal to ⊥
while the second can be considered a “normal form” for infinite waveforms. Since all the operations
in this setting are finite-state (V is finite) a general, complete and efficient framework should be
achievable. This is currently in progress.
A more long term development could see these ideas applied to other computational structures
which are dataflow categories, such as reactive programming [32] or arrows [17], giving a diagrammatic operational semantics more abstract than that of the underlying programming language.
Acknowledgements. We thank George Constantinides and Alex Smith for feedback and suggestions.

References
[1] IEEE standard multivalue logic system for VHDL model interoperability (std logic 1164).
IEEE Std 1164-1993, pages 1–24, May 1993.
[2] S. Abramsky and B. Coecke. A categorical semantics of quantum protocols. In LICS, pages
415–425, 2004.
[3] S. L. Bloom and Z. Ésik. Iteration Theories: The Equational Logic of Iterative Processes.
Springer-Verlag New York, Inc., New York, NY, USA, 1993.
[4] F. Bonchi, F. Gadducci, A. Kissinger, P. Sobocinski, and F. Zanasi. Rewriting modulo symmetric monoidal structure. In LICS, pages 710–719, 2016.
[5] F. Bonchi, P. Sobocinski, and F. Zanasi. Full abstraction for signal flow graphs. In POPL,
pages 515–526, 2015.
[6] F. Bonchi, P. Sobocinski, and F. Zanasi. Lawvere categories as composed props. In CMCS,
pages 11–32, 2016.
[7] V. E. Căzănescu and G. Ştefănescu. Towards a new algebraic foundation of flowchart scheme
theory. Fund. Inf., 13(2):171–210, 1990.
[8] C. Consel and O. Danvy. Tutorial notes on partial evaluation. In POPL, pages 493–501, 1993.
[9] A. Corradini, U. Montanari, F. Rossi, H. Ehrig, R. Heckel, and M. Löwe. Algebraic approaches
to graph transformation-part i: Basic concepts and double pushout approach. In Handbook of
Graph Grammars, pages 163–246, 1997.

20

[10] S. Eilenberg and J. B. Wright. Automata in general algebras. Information and Control,
11(4):452–470, 1967.
[11] C. C. Elgot. Monadic computation and iterative algebraic theories. Studies in Logic and the
Foundations of Mathematics, 80:175–230, 1975.
[12] D. R. Ghica. Diagrammatic reasoning for delay-insensitive asynchronous circuits. In Computation, Logic, Games, and Quantum Foundations, pages 52–68, 2013.
[13] D. R. Ghica and A. Jung. Categorical semantics of digital circuits. In Formal Methods in
Computer-Aided Design (FMCAD), 2016.
[14] M. Hamana. Strongly normalising cyclic data computation by iteration categories of secondorder algebraic theories. In FCSD, pages 21:1–21:18, 2016.
[15] M. Hasegawa. Models of Sharing Graphs: A Categorical Semantics of let and letrec. Springer
Verlag, 1999.
[16] M. Hasegawa. The uniformity principle on traced monoidal categories. Electr. Notes Theor.
Comput. Sci., 69:137–155, 2002.
[17] J. Hughes. Generalising monads to arrows. Science of computer programming, 37(1):67–111,
2000.
[18] A. Joyal and R. Street. The geometry of tensor calculus, i. Adv. in Math., 88(1):55–112, 1991.
[19] A. Joyal, R. Street, and D. Verity. Traced monoidal categories. In Math. Proc. of the Cambridge
Phil. Soc., volume 119, pages 447–468. Cambridge Univ. Press, 1996.
[20] A. Kissinger. Pictures of Processes. PhD thesis, University of Oxford, 2011. arXiv:1203.0202v2.
[21] R. P. Kurshan and K. L. McMillan. Analysis of digital circuits through symbolic reduction.
IEEE Trans. on CAD of Integrated Circuits and Systems, 10(11):1356–1371, 1991.
[22] S. Lack. Composing PROPs. Theory and App. of Categories, 13(9):147–163, 2004.
[23] P. J. Landin. An abstract machine for designers of computing languages. In Proc. IFIP
Congress, volume 65, 1965.
[24] C. E. Leiserson and J. B. Saxe. Retiming synchronous circuitry. Algorithmica, 6(1-6):5–35,
1991.
[25] W. Luk. Pipelining and transposing heterogeneous array designs. J. of VLSI Sig. Proc. Sys.,
5(1):7–20, 1993.
[26] S. Malik. Analysis of cyclic combinational circuits. In Proc. IEEE/ACM Int. Conf. on Comp.
Aided Design, pages 618–625, 1993.
[27] M. Mendler, T. R. Shiple, and G. Berry. Constructive boolean circuits and the exactness of
timed ternary simulation. Form. Meth. Syst. Des., 40(3):283–329, 2012.
[28] G. D. Plotkin. A structural approach to operational semantics. J. Log. Algebr. Program.,
60-61:17–139, 2004.
[29] P. Selinger. A survey of graphical languages for monoidal categories. In New structures for
physics, pages 289–355. Springer, 2010.
[30] M. Sheeran. muFP, A language for VLSI design. In LISP and Func. Prog., pages 104–112,
1984.
[31] A. Simpson and G. Plotkin. Complete axioms for categorical fixed-point operators. In Logic in
Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on, pages 30–41. IEEE,
2000.
[32] Z. Wan and P. Hudak. Functional reactive programming from first principles. In Acm Sigplan
notices, volume 35, pages 242–252. ACM, 2000.

21

