Timing, Span(Graph) and Cospan(Graph)
Posted by Emily Riehl
Guest post by Siddharth Bhat and Pim de Haan. Many thanks to Mario Román for proofreading this blogpost.
This paper explores modelling automata using the Span/Cospan framework by Sabadini and Walters. The aim of this blogpost is to introduce the key constructions that are used in this paper, and to explain how these categorical constructions allow us to talking about modelling automata and timing in these automata.
The category
The category is built from the category by considering diagrams of the form , where is the apex of the span, and are the base of the span. The ordering of left and right is important when we describe the composition of spans. Formally, the objects of are the objects of . The arrows of are from to are spans ().
Now, a natural question is to ask how one composes spans. We compose spans by taking their pullback. Consequently, the category only exists if has all pullbacks. The composition of a span () with another () is given by the pullback with the associated diagram:
Some examples of spans follows:
First, as mathematicians, we are honor-bound to give the trivial example () is the identity span on the object .
Next, any arrow can be considered as a span on the left (), or as a span to the right (). Note that these define a pair of functors from to .
A prototypical example of spans is the span of two finite sets. Suppose we have two sets , and we wish to describe the set of ways to go from to (where we think of and as abstract locations). In such a case, we need a set , which describes the set of ways to get from to , and morphisms , that gives us the start and end position of a path from some element of to some element of .
Remark The pullback, and thus the composition of spans, is only unique up to isomorphism. Hence, is only a proper category if the morphisms are taken to be the isomorphism classes of spans.
The category of directed multigraphs
There are many slightly different notions of a graph in the literature. For our exposition, we will focus on the category of directed multigraphs. Intuitively, this means that we have vertices (states of an automata) and edges (transitions). There can be multiple edges between a pair of vertices (there are multiple ways to transition from one state into another).
Formally, a multigraph is given by a vertex set , a set of edges and a pair functions which denote the source and target of the edge. We will denote a graph as as a pair of its vertex and edge set. We denote for the vertex set of , and for the edge set of .
The objects of the category are these directed multigraphs. The arrows of this category are multigraph morphisms.
A morphism in this category is given by two set valued functions which maps vertices, and which maps edges, under the condition that the images of the edges are consistent with the images of the vertices. That is, for all , and . Said differently, the above condition means that edges must preserve adjacency.
Remark A more concise way to define the above construction is as the presheaf category , over the diagram , whose objects are functors and morphisms are natural transformations.
The (co)limits of
The category of graphs has products , which is computed pointwise: and . Similarly, it has coproducts , also computed pointwise. can thus be made into a cartesian monoidal category or a cocartesian category .
The pullback of a diagram of graphs , written , intuitively performs a pullback along the vertices and the edges. Formally, it is a graph whose vertex set is the pullback of the vertices: , and whose edge set is the pullback of the edges: .
The pushout dualizes the above construction. Intuitively, it glues two graphs along a third one. Formally, the pushout of a diagram of graphs , written , is a quotient by the equivalence generated by .
Remark Seeing as the functor category , automatically derives the above limits and colimits from . The (co)limits are then computed pointwise.
Parallel composition of automata with
At this stage, we have the machinery necessary to add labels onto our graph edges, by means of exploiting , which is a category as has pullbacks. is a symmetric monoidal category with the monoidal product deriving from the cartesian monoidal structure on .
In our case, for automata, we focus on the situation where the graphs at the base are graphs with a single vertex and many edges. These edges are thought of as transition labels. Formally, for a given set of labels , we create the graph .
An automaton is then a span . The states of the automaton are the vertices and the transitions the edges . By definition, each transition maps to some edge and some edge . We denote this diagramatically as a label on the transition.
When composing spans , we get . This composition can be interpreted as synchronized parallel computation. The pullback contains all vertices , meaning that the state of the composed automaton is a product of both a state of automaton and a state of automaton . For the transitions, however, only the edges that have the same label survive. This can be interpreted as a requirement that automata and communicate and can only transition when their signal agrees.
Sequential composition of automata with
In the exact same way that provides us with parallel composition, dualising the construction to gives us sequential composition. This is a category whose objects are graphs, morphisms are cospans of graphs and composition is given by pushout, which exist for . is a symmetric monoidal category due to the cocartesian monoidal structure on .
For a set , define the graph to contain no edges. Then a cospan can be interpreted as an automaton with states and edges having input states, with each corresponding to a state , and similarly output states.
A composition of cospans of automata yields a new automaton . This composition can be thought of as sequential computation, as the state of the composed automaton is either a state of or a state of , where we glue toghether output and inputs states, because we make the equivalence that if corresponds to an output that corresponds as an input to .
Wiring in Span(Graph)
Composition in Span(Graph) allows one to compose spans into a span between and , while the tensor product of spans yield a span between and . However, to allow for more flexible compositions, such as the composition of spans into a span between and , one needs morphisms to connect multiple copies of . In a string diagram of this looks like:
As automata, this corresponds to a synchronization between the parallel processes and , so that they can transition when their left transition is equal. Generally, such connectors between parallel interfaces of automata are given by a Frobenius monoid on , which consists of the following spans: - , giving - , giving - , giving - , giving
where we use the following morphisms in : - , where the monoidal unit is the terminal graph with a single vertex and single loop. - that is the identity on the components. Concretely on graphs, it maps vertex to and edge to .
These are written as string diagrams in [figs from Fong & Spivak 2019]
It can be shown that these obey the commutative monoid axioms
the cocommutative comonoid axioms
and the Frobenius and special axioms
Definition. A tuple of such maps satisfying these axioms is called a special commutative Frobenius monoid.
Theorem. [Fong & Spivak 2018] Given a special commutative Frobenius monoid , for two non-negative integers , any map composed of and the swap , whose string diagram is connected, equals the spider morphism given by
which is also written as
If a special commutative Frobenius monoid exist for all objects in a category and the Frobenius monoid for tensor products are composed of the Frobenius monoid of the objects and , then the category is called hypergraph category [Fong & Spivak 2019]. String diagrams of such categories can be interpreted as a hypergraph. A hypergraph is a graph in which the edges connect an arbitrary number of nodes. In this case, the spans are the nodes of the hypergraph and the spider morphisms form the hyperedges.
Remark The fact that is a hypergraph category relies on the fact that is a Cartesian category, a symmetric monoidal category whose tensor product is a categorical product and whose unit is terminal. Hence, for any Cartesian category , is a hypergraph category. The spans in the Frobenius monoids are constructed similarly from the diagonal morphisms and terminal maps .
Wiring in Cospan(Graph)
Similar to , also forms a hypergraph category in which each object is equiped with a spider morphism. Recall that is a symmetric monoidal category with as tensor product the disjoint union of graphs, which is a coproduct, and its unit is , the initial graph , which contains no edges and vertices. As such, it is equiped with a codiagonal map , which is the identity on each part, and an initial map . For any graph , one can construct the following cospans, constituting a special Frobenius monoid: - , giving - , giving - , giving - , giving
Remark In more generality, for any cocartesian category - a symmetric monoidal category whose tensor product is a coproduct and unit is initial - is a hypergraph category.
Feedback via traces
Some automata may also want to synchronize their parallel left and right interfaces (in the case of ) or their sequential top and bottom interfaces (in the case of ). In either case, the hypergraph structure provides for this in the following way:
Hence, every hypergraph category is traced monoidal category, which are categories which provide a notion of feedback by providing for all objects , a tracing map: satisfying some coherence axioms.
Timing
A path in a directed graph is a sequence of edges such that the tail node of edge equals the start node of edge . In the context of an automaton, a path is called a behaviour. The automaton can be interpreted as a discrete time system, in the simplest case by saying that each edge has time duration 1, so that the duration of a behaviour equals the length of the path. Note that this notion of time is imposed as an interpretation, while the underlying model remains unchanged.
As an example, we will construct a clock by parallel composing automata that cycle with frequency 1, 60, 60 and 24. We define one parallel interface , corresponding to taking a step or remaining idle. We define an automaton with left interface and right interface with one node and one edge: . This automaton sends a tick to the right at each step. Also, for any natural number , we define automaton with left and right interface :
Whenever receives a tick from the left, it ticks itself. After ticks, it sends a tick to the right.
If we compose these automata as:
We get a unit interface on the left and interface on the right. Its only behaviour is a single cycle of duration . The right labels are on the first position on each step, on the second position every 60 steps, on the third position every steps and on the fourth position every steps. We have built a clock.
References
- Baez, John C. “Spans in quantum theory.” Keynote talk at Deep Beauty: Mathematical Innovation and the Search for an Underlying Intelligibility of the Quantum World, Princeton University
- Alessandra Cherubini, Nicoletta Sabadini, Robert F. C. Walters: Timing in the Cospan-Span Model. Electron. Notes Theor. Comput. Sci. 104: 81-97 (2004)
- Brendan Fong and David I. Spivak. 2019. “Hypergraph Categories.” Journal of Pure and Applied Algebra 223 (11): 4746-77.
- Brendan Fong and David I. Spivak. 2018. “Seven Sketches in Compositionality: An Invitation to Applied Category Theory.”