You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We describe an algebraic theory of graphs, $\mathsf{G}[X,V]$. The theory is dependent on a theory of variables, $X$, and a theory of vertices, $V$. Each theory is required to provide an effective procedure for deciding membership. More specifically, given any $u$ we can decide $u \in X$ (and $u \in V$, respectively). Likewise, both dependencies must come with an effective notion of equality. That is, for variables $x_1$ and $x_2$ there is an effective procedure for deciding whether $x_1 = x_2$, and likewise for vertices. We refer to the graphs captured by the theory as the domain of graphs of $\mathsf{G}[X,V]$. The theory is unique in that it explicitly includes a notion of a reference to a vertex and only admits edges between references. Indeed, variables supply the references. We write
$$\mathsf{G}[X,V];\Gamma \vdash g$$
to mean that -- given the references $\Gamma$ -- $g$ is well formed in $\mathsf{G}[X,V]$ and we use Plotkin-style SOS rules of the form
to indicate that given dependencies $K_{\Gamma}(\Gamma_1,\ldots,\Gamma_n)$ the graph, $K_g(g_1,\ldots,g_n)$, constructed from well-formed graphs $g_1,\ldots,g_n$, using the constructor $K_g$ is well-formed. The effective procedure (aka algorithm) for determining when a graph is well formed is given by a collection of such rules.
There are two principal reasons for the development of this theory. One is complexity management. Whether they are the objects of investigations themselves, as in graph theory, or are being used a tools to support some other investigation such as in biology or physics or cryptocurrency, graphs are used primarily in computations. As such they should be algorithmically specified. The standard presentation of graphs as collections of vertices and edges does not treat them as algorithmically specified. To understand this lacunae consider the standard presentation of a linked list.
$$\mathsf{List}[A] = 1 + A \times \mathsf{List}[A]$$
This recursive specification matches the standard interpretation of lists containing elements of type $A$ as either empty (the $1$ in the domain equation) or formed by consing an element of type $A$ onto a list containing elements of type $A$ (the product $A \times \mathsf{List}[A]$). The recursive specification recognizes that lists are recursively built up from lists and a small set of operations.
Such an algebraic characterization of linked lists is typically used in algorithmic specifications of calculations involving lists. By contrast graphs are typically presented as a pair of collections of vertices and edges, rather than as a recursive data type involving operations that build graphs from graphs. This conception permeates many tools and software libraries that provide computational support for calculating with graphs and result in nearly overwhelming complexity.
An excellent example is the popular tool GraphViz and its dotty language. Using dotty to specify the complete graph of 100 nodes is an enormous task. The recursive data type resulting from the theory of graphs presented here results in a single line specification of the complete graph. More generally, in the examples we present we see an exponential jump in complexity in the types of graphs being characterized and yet the algorithmic characterizations remain typical 1-line recursive specifications.
The other motivation is foundational. We seek a minimal characterization of subtypes of of the type of graphs. As will become clear, $\mathsf{G}[X,V]$ represents the type of graphs. We can pick out subtypes of this type by two well established methodologies. One is to probe the type with structure preserving functions from a domain, such as the naturals $\mathsf{Nat}$ or $\mathcal{P}A$, the power set of a set $A$, into $\mathsf{G}[X,V]$. The other is to lift the graph constructors point-wise through a collection type. Here we find the minimal domain in which these two notions of subtype coincide.
Related work
This work is inspired by two different threads. One is the seminal work of Cardelli, Gardner, and Ghelli. There is a natural way to encode graphs in process calculi, such as the $\pi$-calculus. This turns the spatial logics of Caires and Cardelli into a graph query language. A formula queries for the graphs that satisfy it. The other thread is the seminal work of Bill Lawvere and many others relating monads to algebraic theories.
Well-formedness
This is an algebraic theory, and thus it is syntactic in nature. It provides a language of graphs that are built out of logical sentences. In more detail, the theory admits three kinds of sentences:
recognizing an admissible vertex: $\mathsf{G}[X,V]; \Gamma \vdash v$;
recognizing an admissible variable: $\mathsf{G}[X,V]; \Gamma \vdash x$;
and, recognizing a well formed graph: $\mathsf{G}[X,V]; \Gamma \vdash g$
Variables are used to capture references to vertices which are in turn used to form edges between vertices. As such, judging the wellformedness of a graph depends on the use of references. Hence, a judgement makes use of a dependency list, $\Gamma$ which is just a sequence of variables. That is,
$$\Gamma ::= () ;|; x, \Gamma$$
Notationally, we overload the comma to indicate concatenation of sequences. Thus, given $\Gamma_1 = x_{11},\ldots,x_{1m}$ and $\Gamma_2 = x_{21},\ldots,x_{2n}$, then $\Gamma_1,\Gamma_2 = x_{11},\ldots,x_{1m},x_{21},\ldots,x_{2n}$
A graph expression is given by the grammar
$$g,h ::= 0 ;|; v|g ;|; g \otimes h ; |;\mathsf{let}; x = v ; \mathsf{in}; g ;|; \langle \mathsf{let}; x_1 = v_1 ; \mathsf{in}; g, \mathsf{let}; x_2 = v_2 ; \mathsf{in}; h\rangle$$
Pronunciation
The graph constructors are pronounced as follows.
$0$ -- "the empty graph", or just "empty";
$v | g$ -- "$g$ with the vertex $v$ adjoined", or "adjoin $v$ to $g$";
$g_1 \otimes g_2$ -- "the graph formed by juxtaposing $g_1$ and $g_2$", or "juxtapose $g_1$ and $g_2$", or just "$g_1$ and $g_2$";
$\mathsf{let}; x = v ; \mathsf{in}; g$ -- "let $x$ stand for $v$ in $g$"; or "let $x$ be $v$ in $g$";
$\langle \mathsf{let}; x_1 = v_1 ; \mathsf{in}; g_1,\mathsf{let}; x_2 = v_2 ; \mathsf{in}; g_2\rangle$ -- "the graph formed by connecting $g_1$ to $g_2$ with and edge from $x_1$ to $x_2$"; or, "connect $g_1$ to $g_2$ with and edge from $x_1$ to $x_2$".
The judgment $\mathsf{G}[X,V]; \Gamma \vdash g$ is pronounced "$\mathsf{G}[X,V]$ thinks that $g$ is well-formed, given dependencies, $\Gamma$ ." Similarly, $\mathsf{G}[X,V]; \Gamma \vdash v$ is pronounced "$\mathsf{G}[X,V]$ thinks that $v$ is an admissible vertex, given dependencies, $\Gamma$;" and $\mathsf{G}[X,V]; \Gamma \vdash x$ is pronounced "$\mathsf{G}[X,V]$ thinks that $x$ is an admissible variable, given dependencies, $\Gamma$."
A rule of the form
$$\frac{ H_1, \ldots , H_n }{ C }R$$
is pronounced "$R$ concludes that $C$ given $H_1$, $\ldots$, $H_n$".
The rules for judging when a vertex or a variable are admissible or graph is well formed are as follows
The $Foundation$ rule says that regardless of the theory of vertices or variables, the empty graph is always well formed.
The rules $Verticity$ and $Variation$ say that admissibility derives from the effective notion of membership required of the theory of vertices and the theory variables.
The rule for $Participation$ says that if $\mathsf{G}[X,V]$ thinks that $g$ is well formed, given $\Gamma$, and $\mathsf{G}[X,V]$ thinks that $v$ is admissible as a vertex, then $\mathsf{G}[X,V]$ thinks that adjoining $v$ to $g$, i.e. $v|g$, is well formed.
The rule for $Dependence$ is similar to $Participation$. It says that $\mathsf{G}[X,V]$ thinks that it can adjoin $x$ to $g$, i.e. $x|g$ to get a well formed graph given $\Gamma$ if $\mathsf{G}[X,V]$ thinks that $g$ is well formed, given $\Gamma,x$.
The rule for $Juxtaposition$ says that simply juxtaposing two well formed graphs results in a well formed graph. A careful accounting will observe that the dependencies of the two graphs must be disjoint.
Logicians and computer scientists will recognize the rule for $Nomination$ as a kind of cut rule. It's like $\beta$-reduction with an explicit substitution. Specifically, supposing that $\mathsf{G}[X,V]$ thinks that $g$ is well formed, given $\Gamma,x$ and that $\mathsf{G}[X,V]$ thinks that $v$ is an admissible vertex then $\mathsf{G}[X,V]$ thinks that letting $x$ stand for $v$ in $g$ is well formed, given $\Gamma$. A graph given by an expression of this form is said to be in nominated form.
Finally, the rule for $Connection$ says that an edge is only admissible between two well formed graphs in nominated form and then only when the dependencies are disjoint.
Notice that the intuitive interpretation for $Nomination$ matches the pronunciation.
$$\frac{ \mathsf{G}[X,V];\Gamma,x \vdash g ; ;\mathsf{G}[X,V]; () \vdash v}{ \mathsf{G}[X,V]; \Gamma \vdash \mathsf{let}; x = v ; \mathsf{in}; g}Nomination$$
"Nomination concludes that $\mathsf{G}[X,V]$ thinks that the graph that lets $x$ stand for $v$ in $g$ is well formed given $\Gamma$ if $\mathsf{G}[X,V]$ thinks that $g$ is well formed given $\Gamma,x$, and $\mathsf{G}[X,V]$ thinks that $v$ is an admissible vertex."
For clarity we will often write $v|0$ as $[v]$.
Membership
We can extend the effective membership relation provided by $V$ to one on $\mathsf{G}[X,V]$. Written $\mathsf{G}[X,V] \vdash v \in g$, the algorithm is given by the following set of rules
$$\frac{ }{ \mathsf{G}[X,V] \vdash v \in v | g}Ground$$
$$\frac{ \mathsf{G}[X,V] \vdash v \in g }{ \mathsf{G}[X,V] \vdash v \in g \otimes g'}Union$$
$$\frac{ \mathsf{G}[X,V] \vdash v \in g }{ \mathsf{G}[X,V] \vdash v \in \mathsf{let}; x = v ; \mathsf{in}; g}Transparency$$
As a matter of convenience we write $\mathsf{G}[X,V] \vdash v \not\in g$ to mean that it is not the case that $\mathsf{G}[X,V] \vdash v \in g$. The inquisitive reader is invited to write a similar set of rules for edge membership. Of course, given a graph, $g$, it is very useful to refer to its collection of vertices and its collection of edges, which we denote $\mathsf{v}(g)$ and $\mathsf{e}(g)$ respectively.
Equations
The syntactic theory is too fine grained. It makes syntactic distinctions that do not correspond to distinct graphs. Juxtaposition is a great example. It corresponds to the disjoint sum of two graphs and as such the order of juxtaposition should not matter. We erase these syntactic distinctions with a set of equations on the graph expressions.
$$\frac{ }{ \mathsf{G}[X,V] \vdash 0 \otimes g \equiv g}Identity$$
$$\frac{ }{ \mathsf{G}[X,V] \vdash \mathsf{let}; x = v ; \mathsf{in}; \mathsf{let}; x' = v ; \mathsf{in}; g \equiv \mathsf{let}; x = v ; \mathsf{in}; g}Conservation$$
$$\frac{ \mathsf{G}[X,V] \vdash x \notin g_2}{ \mathsf{G}[X,V] \vdash (\mathsf{let}; x = v ; \mathsf{in}; g_1) \otimes g_2 \equiv \mathsf{let}; x = v ; \mathsf{in}; ( g_1 \otimes g_2)}Extrusion$$
Note the mutual dependency amongst $Extrusion$ and $Permutation$ and the extended $\in$ relation.
Examples
Graphs as morphism
Let $X$ be some set of variables, $D$ be some domain, such as $Nat$, the natural numbers, or $Bool$, the booleans. We can describe many graphs as morphisms, $g(X,D): D \to \mathsf{G}[X,D]$.
The discrete graph
The discrete graph of $n$ elements, written $\mathsf{discrete}(n)$, is simply $n$ unconnected vertices. Noting that the graph consisting of a single vertex, $n$, has the form $n \to 0$, which adjoins $n$ to the empty graph, $0$, we can define the domain of discrete graphs recursively.
Sometimes it is convenient to use domain elements as variables as well as vertices; that is, it is often useful to form graphs from $\mathsf{G}[D,D]$. In this case, we distinguish the mention of a domain element, say $d$, in the role of a variable from the mention in the role of a vertex by quotation marks. Specifically, we write $\ulcorner d\urcorner$ when using $d$ as a variable versus merely $d$ when using $d$ as a vertex. An example in context this might look like $\mathsf{let}; \ulcorner d\urcorner = d ; \mathsf{in}; g$.
The chain
Using these two ideas we can give a recursive definition of the domain of chains. As with the discrete graph, the chain of $0$ elements is the empty graph. The chain of a single element is not simply adjoining that element as a vertex to the empty graph. It also selects that element. Then the recursive specification creates an edge between the graph containing a single element, $n \to 0$, and the chain of $n-1$ elements by selecting the element, $n$ and calling it $\ulcorner 2n-1\urcorner$, and then linking the two resulting graphs. To ensure that the result is linkable it selects the element again, this time calling it $\ulcorner 2n \urcorner$.
This next example is made even more compact if we admit some syntactic sugar. First, let us stipulate that $D$ supports a means of checking elements, such as $d$, for properties, say $p$, and write $p(d)$ for the predicate that determines when $d$ inhabits the property $p$. We can lift the edge expression to an expression between collections of elements from $D$. Specifically, we can form
which adds to the graph $g_1 \otimes g_2$ an edge from each vertex in ${ v \in \mathsf{v}(g_1) | p_1(v) }$ to each vertex in ${ v \in \mathsf{v}(g_2) | p_2(v) }$
When $|{ v \in \mathsf{v}(g_i) | p_i(v) }| = 1$ then this form is the same as
where $c_i[0]$ denotes the singleton element inhabiting ${ v \in \mathsf{v}(g_i) | p_i(v) }|$.
With this syntactic sugar we have a 1-line specification for the complete graph.
$\mathsf{complete}(0) = 0$$\mathsf{complete}(n) = \langle \mathsf{for} ( x \leftarrow \mathsf{v}(\mathsf{discrete(1)})){ \mathsf{discrete(1)} }, \mathsf{for} ( y \leftarrow \mathsf{v}(\mathsf{complete}(n-1))){ \mathsf{complete}(n-1) } \rangle$
These examples illustrate our main motivation for introducing the theory of graphs. As we move from discrete to chain to cycle to complete graphs the complexity of the graph structure grows dramatically; and yet the complexity of the recursive specifications of the graphs remains almost constant.
It is also important to recognize that each of these examples are also subdomains of their respective graph domains. For example,
$${ \mathsf{chain(i)} | i \in \mathsf{Nat}} \subset \mathsf{G}[\mathsf{Nat},\mathsf{Nat}]$$
In this sense we can think of $\mathsf{G}[\mathsf{Nat},\mathsf{Nat}]$ as a container domain for ${ \mathsf{chain(i)} | i \in \mathsf{Nat}}$. More standard language would dub the latter a subtype of the former. In each of these examples we arrive at the subdomain or subtype of the container domain by imposing additional constraints on edge formation. In fact, each of these examples and infinitely many more can be computed either directly as we have done or as filters on their container domains, or super types, that selects graphs that adhere to the edge criteria or they can be computed by adjoining to the theory the additional constraints on edges. We will formalize this idea in a subsequent section.
The cycle and complete graph examples raise an important point about graph equality and references to whole graphs. In the section below we develop a notion of graph references to allow for more sophisticated compositional and recursive specification of graphs.
Graph references
In many instances it it useful to refer not only to vertices but whole graphs. For this we assume that the collection of variables is actually divided into two distinct sub-collections; that is, we require $X = X_v + X_g$. Notationally, we will use lowercase letters such as $x$, $y$, $z$ to range over $X_v$ and uppercase letters such as $A$, $B$, $C$, etc to range over $X_g$. When we are building graphs using references to graphs we need to expand the theory to include more common cyclic definitions as is typically found in functional languages involving $\mathsf{letrec}$.
Just as we separate the collection of variables into variables for vertices and variables for graphs, we separate the functional dependencies. This requires expanding the basic judgment to include graph variable dependencies on the left hand side of the turnstile: $\mathsf{G}[X,V]; \Gamma; \mathcal{G} \vdash g$. This expanded form allows mentions of $A$, $B$, etc to occur in $g$, which can be discharged later and gives rise to our first new rule. Just as with $\Gamma$, we use $\mathcal{G}$ to range over comma separated sequences of graph variables. This allows us to form wires.
$$\frac{ }{ \mathsf{G}[X,V]; \Gamma; A \vdash A}Wire$$
Equipped with this rule we can form graphs that have "holes" in them. Note that we could have achieved the same effect by calculating a graph context type from our graph type. However, with this next rule we allow bundling of wires and establish that our contexts have multiple holes.
This in turn makes it possible to describe a wide range of graphs with recursive structure. In particular, prior to the addition of graph references the theory describes only finite graphs built from $X$ and $V$. With the addition of graph references the graphs can be infinitary. In the sequel we will refer to graphs that make no mention of graph variables as ground. Likewise, if graph $g$ enjoys wellformedness without any dependencies, i.e. $\mathsf{G}[X,V]; (); () \vdash g$, we say $g$ is closed.
Rewrite systems
The $\lambda$-calculus
Let $M$ denote the set of terms in the $\lambda$-calculus, and $t$, $u$, $\ldots$ range over terms in $M$. We form graphs of the reductions of terms, $\mathsf{G}[M,M]$ by filtering edges for $\beta$-reduction. To avoid confusion in the sequel we will write $\ulcorner t\urcorner$ when using $t$ as a variable, and unadorned when considering it as a term. More concretely, given
$$\uparrow t = \mathsf{let}; \ulcorner t \urcorner = t ; \mathsf{in}; [\ulcorner t \urcorner] $$
we lift terms to graphs using
$$\frac{ }{ \mathsf{G}[M,M]; (); () \vdash \uparrow t }embedding$$
and then filter edges by the condition
$$\frac{ \mathsf{G}[M,M]; (); () \vdash \uparrow t ; ;\mathsf{G}[M,M]; (); () \vdash \uparrow u ;; t \to u}{ \mathsf{G}[X,V]; (); () \vdash \langle \uparrow t,\uparrow u \rangle}Reduction$$
This gives rise to the graph of reductions of a term, $\mathsf{red}(t)$ which is defined by
The ambitious reader is invited to provide a similar domain of graphs for the $\mathsf{rho}$-calculus.
Categories
We can provide a theory of categories, $\mathcal{C}[X,V]$, that are subdomains of $\mathsf{G}[X,V]$.
Reflection and the syntax of a graph
In some sense the entire point of the previous sections is to provide proof that the domain $\mathsf{G}[X,V]$ serves equally well as theory of variables or as a theory of vertices, provided that $X$ and $V$ serve those roles respectively. That is, $\mathsf{G}[X,V]$ comes with an effective procedure for deciding when a graph, say $g$ is in the domain, $\mathsf{G}[X,V]$. Specifically, we define $g \in \mathsf{G}[X,V]$ to be the determination that $\mathsf{G}[X,V];();() \vdash g$, i.e. that $g$ is closed in $\mathsf{G}[X,V]$. Likewise, $\mathsf{G}[X,V]$ comes with an effective procedure for determining if two graphs are equal. This observation yields additional expressive power. We can consider graph domains that are recursively defined.
Domains like $\mathcal{D}[X,V]$ allow us to create graphs in which we freely mix vertices from $V$ with vertices made out of entire graphs. As an example, with the recursive domain we given a graph $g \in \mathsf{G}[X,V]$ we can compute the graph of its syntax, $\mathsf{s}(g) \in \mathcal{D}[X,V]$.
$\mathsf{s}( 0 ) = \ulcorner 0 \urcorner | 0$
$\mathsf{s}( v | g ) = (\mathsf{let}; \ulcorner g \urcorner = g ; \mathsf{in}; \ulcorner g \urcorner | \mathsf{s}(g),\mathsf{let}; \ulcorner v \urcorner = v ; \mathsf{in}; \ulcorner v \urcorner | 0)$
$\mathsf{s}( \mathsf{let}; x = v ;\mathsf{in}; g )$
$ = $
$ (\mathsf{let}; \ulcorner g \urcorner = g ; \mathsf{in}; \ulcorner g \urcorner | \mathsf{s}(g),\mathsf{let}; \ulcorner x \urcorner = x ; \mathsf{in}; \mathsf{let} ; \ulcorner v \urcorner = v ; \mathsf{in}; \ulcorner x \urcorner | \ulcorner v \urcorner | 0)$
This sets up our foundational investigation. Recall that our examples $\mathsf{discrete}$, $\mathsf{chain}$, $\mathsf{cycle}$, and $\mathsf{complete}$ gave rise to subtypes of $\mathsf{G}[\mathsf{Nat},\mathsf{Nat}]$ by exploiting structure of $\mathsf{Nat}$. Similarly, the $\mathsf{LADL}$ types give rise to subtypes of $\mathsf{G}[X,V]$. Our focus of investigation is the question of the conditions under which the structure of $X$ and $V$ supply subtypes of $\mathsf{G}[X,V]$ that coincide with the $\mathsf{LADL}$ types?
Not surprisingly, we find that when we can faithfully map $X$ (resp., $V$) into $\mathsf{G}[X',V']$ for some $X'$ and $V'$, then we can establish an isomorphism between the subtypes available from the structure of $X$ and $V$ and the $\mathsf{LADL}$ types. This observation sets up a process by which domains of $X$ and $V$ are replaced by graph-based representations of them. The limit of this process, the smallest structure for which these coincide, is given by
Note that the crossover style operations like "$\cdot$" together with reflection allow us to define evolutionary processes (in the sense of Holland) for graphs and graph domains. The principal missing ingredient is a fitness function for evaluating graphs and graph domains for selection and "reproduction."
[This is a reference test][Holland]
Bibliography
[Holland]: Adaptation in Natural and Artificial Systems
J. Holland. University of Michigan Press, Ann Arbor, MI, (1975)second edition, 1992.
Algebraic Graph Theory
C. Godsil, and G. Royle. Graduate Texts in Mathematics. volume 207 of Graduate Texts in Mathematics. Springer, (2001)
Graph-based Logic and Sketches
Atish Bagchi, Charles Wells
Expressiveness and complexity of graph logic
Anuj Dawar, Philippa Gardner, Giorgio Ghelli
A Spatial Logic for Querying Graphs
Luca Cardelli, Philippa Gardner, Giorgio Ghelli