Keywords

1 Introduction

Graph operations have been a key ingredient of the generalized sketch framework, developed in the 90s by a group around the second author and motivated by applications in databases and data modeling [1, 3, 5]. What was missing, until now, is a proper formal substantiation of the “Kleisli mapping” construct heavily employed in those papers. When we re-launched, ten years later, generalized sketches under the name Diagrammatic Predicate Framework (DPF) [6, 12,13,14], we dropped operations due to the lack of a proper formalization appropriate for our applications in Model Driven Software Engineering. Finally, during his period in Hartmut’s group in 1991-00, the first author had always been wondering if one should look for a uniform mechanism to create names for new items produced by injective graph transformation rules via pushouts.

In the paper, we present a concept of graph algebra that generalizes the traditional concept of algebra in the sense that (1) we use graphs as carriers, instead of sets, and (2) we generalize algebraic operations to graph operations. We introduce graph terms and present a concrete construction of free graph algebras as graph term algebras. As a side effect, graph terms provide a uniform mechanism for the new names problem mentioned above.

As the main result of the paper we obtain for any graph signature \(\varGamma \) an adjunction between the category \(\mathsf {Graph}\) of graphs and the category \(\mathsf {GAlg}{(\varGamma )}\) of graph \(\varGamma \)-algebras. These adjunctions generalize the traditional adjunctions between the category \(\mathsf {Set}\) and categories \(\mathsf {Alg}{(\varSigma )}\) of \(\varSigma \)-algebras. The Kleisli categories of the new adjunctions provide the necessary substantiation of the idea of “Kleisli morphisms” of the second author, we have been looking for.

As a pleasant surprise, we realized that the new setting of graph algebras establishes an “integrating link” between the two areas Hartmut Ehrig contributed most - algebraic specifications with initial semantics and graph transformations.

To keep technicalities simple, and to meet the space limitations, we only consider unsorted/untyped signatures and algebras, and leave the straightforward generalization for the many-sorted/typed case for future work. As a running example for a graph signature \(\varGamma \), we have chosen \(\varGamma \) consisting of arrow composition, identity, initial object, and pullback, which hopefully most of the readers are familiar with.

The paper is organized as follows. In Sect. 2 we recapitulate the basic algebraic concepts signature, operation, algebra, variable, term and term algebra, and we discuss the characterization of term algebras as free algebras. In Sect. 3 we analyze algebraic operations and “diagrammatic” operations, like composition and pullbacks, in the light of graphs, and develop the new concepts graph signature, graph operation and graph algebra. We define corresponding categories \(\mathsf {GAlg}{(\varGamma )}\) of graph algebras for given graph signatures \(\varGamma \). In Sect. 4, we analyse the construction of terms in the light of graph transformations, and develop the new concepts of a graph term and a graph term algebra. We show that graph term algebras are free graph algebras and discuss applications of this main result. Finally, we discuss related work in Sect. 5 and Sect. 6 outlines different dimensions of further research.

2 Background: Algebras and Term Algebras

An (algebraic) signature \(\varSigma =(F,ar)\) is given by a finite set \(F\) of operation symbols and an arity function \(ar:F\rightarrow \mathbb {N}\). A \(\varSigma \)-algebra \(\mathcal {A}=(A,F^\mathcal {A})\) is provided by a (carrier) set \(A\), also denoted by \(|\mathcal {A}|\), and a family \(F^\mathcal {A}=(\omega ^\mathcal {A}:A^{ar(\omega )}\rightarrow A\mid \omega \in F)\) of operations. For \(n\in \mathbb {N}\) we denote by \(A^n\) the set of all n-tuples \(\bar{a}=(a_1,\ldots ,a_n)\) of elements in \(A\). For \(n=0\) we obtain, in such a way, the singleton set \(A^0=\{()\}\) containing the empty tuple. A symbol \(c\in F\) with \(ar(c)=0\) is also called a constant symbol. The corresponding operation \(c^\mathcal {A}:A^0\rightarrow A\) in a \(\varSigma \)-algebra \(\mathcal {A}\) is a “pointer” with the only element () in \(A^0\) pointing to the element \(c^\mathcal {A}()\) in \(A\).

A \(\varSigma \)-algebra \(\mathcal {A}\) is a subalgebra of a \(\varSigma \)-algebra \(\mathcal {B}\) if, and only if, \(A\subseteq B\) and \(\omega ^\mathcal {A}(\bar{a})=\omega ^\mathcal {B}(\bar{a})\) for all \(\omega \in F\) and all \(\bar{a}\in A^{ar(\omega )}\subseteq B^{ar(\omega )}\). This means that the subset \(A\) of the carrier of \(\mathcal {B}\) has to be closed under the operations in \(\mathcal {B}\). Specifically, \(A\) has to contain all the constants \(c^\mathcal {B}()\) from \(\mathcal {B}\).

A \(\varSigma \)-homomorphism \(f:\mathcal {A}\rightarrow \mathcal {B}\) between two \(\varSigma \)-algebras \(\mathcal {A}\) and \(\mathcal {B}\) is a map \(f:A\rightarrow B\) such that for every \(\omega \in F,\; ar(\omega )=n\) we have \(f\circ \omega ^\mathcal {A}=\omega ^\mathcal {B}\circ f^n\) where the n’th power \(f^n:A^n\rightarrow B^n\) of the map \(f\) is defined by \(f^n(\bar{a})=(f(a_1),\ldots ,f(a_n))\) for all \(\bar{a}=(a_1,\ldots ,a_n)\in A^n\). That is, for each \(\omega \in F,\; ar(\omega )=n\) we require

$$\begin{aligned} f(\omega ^\mathcal {A}(a_1,\ldots ,a_n))=\omega ^\mathcal {B}(f(a_1),\ldots ,f(a_n))\; \text{ for } \text{ all }\; (a_1,\ldots ,a_n)\in A^n. \end{aligned}$$
(1)

\(f^0:A^0\rightarrow B^0\) is the identity on \(\{()\}\). Note that requirement (1) for constants \(c\in F\) means that constants are mapped to constants: \(f(c^\mathcal {A}())=c^\mathcal {B}(f^0())=c^\mathcal {B}()\).

The composition \(g\circ f:\mathcal {A}\rightarrow \mathcal {C}\) of two \(\varSigma \)-homomorphisms \(f:\mathcal {A}\rightarrow \mathcal {B}\) and \(g:\mathcal {B}\rightarrow \mathcal {C}\) is given by the composition \(g\circ f:A\rightarrow C\) of the underlying maps \(f:A\rightarrow B\) and \(g:B\rightarrow C\). In such a way, \(\varSigma \)-algebras and \(\varSigma \)-homomorphisms constitute a category \(\mathsf {Alg}{(\varSigma )}\), and the assignments \(\mathcal {A}\mapsto |\mathcal {A}|\) and \((f:\mathcal {A}\rightarrow \mathcal {B})\mapsto (f:|\mathcal {A}|\rightarrow |\mathcal {B}|)\) define a forgetful functor \(|\_|:\mathsf {Alg}{(\varSigma )}\rightarrow \mathsf {Set}\).

Example 1

(Natural numbers). We consider the signature \(\varSigma =(F,ar)\) with \(F=\{\mathsf {z},\mathsf {s},\mathsf {p}\}\) consisting of a constant symbol \(\mathsf {z}\), \(ar(\mathsf {z})=0\), a unary operation symbol \(\mathsf {s}\), \(ar(\mathsf {s})=1\), and a binary operation symbol \(\mathsf {p}\), \(ar(\mathsf {p})=2\). As sample \(\varSigma \)-algebra \(\mathcal {N}=(\mathbb {N}, F^\mathcal {N})\) we consider the natural numbers with a zero, a successor, and a plus operation: \(\mathsf {z}^\mathcal {N}()=0\), \(\mathsf {s}^\mathcal {N}=\_\,+\,1:\mathbb {N}\rightarrow \mathbb {N}\), \(\mathsf {p}^\mathcal {N}= \_\,+\_ :\mathbb {N}^2\rightarrow \mathbb {N}\).

Let be given an algebraic signature \(\varSigma \) and a set \(X\) of variables. \(\varSigma \)-terms on \(X\) are strings build of three kinds of symbols: operation symbols from \(F\), variables from \(X\) and three auxiliary symbols “,”, “\(\langle \)”, “\(\rangle \)”. The inductive definition of terms goes traditionally as follows (compare [8], p. 18):

Definition 1

(Terms). The set of all \(\varSigma \)-terms on a set \(X\) of variables is the smallest set of strings of symbols such that:

\(\mathrm{(Variables).}\) \(X\subseteq T_\varSigma (X)\),

\(\mathrm{(Constants).}\)   for all \(c\in F\) with \(ar(c)=0\),

\(\mathrm{(Operations).}\)   for all operation symbols \(\omega \in F\) with \(ar(\omega )=n\ge 1\) and all \(\varSigma \)-terms .

A simple, but crucial, observation is, that the generation of terms can be interpreted as operations in special \(\varSigma \)-algebras (compare [8], p. 67):

Definition 2

(Term algebra). For a given set \(X\) of variables we denote by \(\mathcal {T}_\varSigma (X)=(T_\varSigma (X),F^{\mathcal {T}_\varSigma (X)})\) the \(\varSigma \)-algebra of \(\varSigma \)-terms on \(X\) with:

\(\mathrm{(Constants).}\) \(c^{\mathcal {T}_\varSigma (X)}()=c\langle \rangle \in T_\varSigma (X)\) for all \(c\in F\) with \(ar(c)=0\),

\(\mathrm{(Operations).}\) \(\omega ^{\mathcal {T}_\varSigma (X)}(t_1,\ldots , t_n)=\omega \langle t_1,\ldots ,t_n\rangle \in T_\varSigma (X)\) for all operation symbols \(\omega \in F\) with \(ar(\omega )=n\ge 1\) and all n-tuples .

That any term is generated in a unique way, is abstractly reflected by the characterization of term algebras as free algebras (compare [8], p. 68):

Proposition 1

(Free algebras). For each set \(X\) of variables the \(\varSigma \)-algebra \(\mathcal {T}_\varSigma (X)=(T_\varSigma (X),F^{\mathcal {T}_\varSigma (X)})\) has the following universal property: For any \(\varSigma \)-algebra \(\mathcal {A}\) and any variable assignment \(\alpha :X\rightarrow |\mathcal {A}|\) there exists a unique \(\varSigma \)-homomorphism \(\alpha ^*:\mathcal {T}_\varSigma (X)\rightarrow \mathcal {A}\) such that: \(\alpha ^*\circ in_X= \alpha \).

Proposition 1 can be shown by structural induction according to the inductive definition of terms in Definition 1: For the basic case of variables the defining condition forces \(\alpha ^*(x)=\alpha (x)\) for all \(x\in X\). For the basic case of constant symbols the definition of operations in \(\mathcal {T}_\varSigma (X)\) and the homomorphism condition entail \(\alpha ^*(c\langle \rangle )=\alpha ^*(c^{\mathcal {T}_\varSigma (X)}())=c^\mathcal {A}()\) for all \(c\in F\) with \(ar(c)=0\). And, for the induction step the definition of operations in \(\mathcal {T}_\varSigma (X)\) and the homomorphism condition provide the necessary induction/recursion scheme

$$\begin{aligned} \alpha ^*(\omega \langle t_1,\ldots ,t_n\rangle )=\alpha ^*(\omega ^{\mathcal {T}_\varSigma (X)}(t_1,\ldots ,t_n)) =\omega ^\mathcal {A}(\alpha ^*(t_1),\ldots ,\alpha ^*(t_n)) \end{aligned}$$
(2)

for all operation symbols \(\omega \in F\) with \(ar(\omega )=n\ge 1\) and all .

The universal property determines \(\mathcal {T}_\varSigma (X)\) up to isomorphism in \(\mathsf {Alg}{(\varSigma )}\). A \(\varSigma \)-algebra \(\mathcal {A}\) is isomorphic to \(\mathcal {T}_\varSigma (X)\) iff the following conditions are satisfied:

  1. 1.

    Generators: There is an injective mapping \(em:X\rightarrow |\mathcal {A}|\).

  2. 2.

    No confusion: \(em(x)\ne \omega ^\mathcal {A}(\bar{a})\) for any \(x\in X\), any operation symbol \(\omega \in F\) and any tuple \(\bar{a}\in A^{ar(\omega _)}\). For any operation symbols \(\omega _1,\omega _2\in F\) and any tuples \(\bar{a}_1\in A^{ar(\omega _1)}\), \(\bar{a}_2\in A^{ar(\omega _2)}\) we have

    $$\omega _1^\mathcal {A}(\bar{a}_1)\ne \omega _2^\mathcal {A}(\bar{a}_2)\quad \text{ iff }\quad \omega _1\ne \omega _2 \;\text{ or }\; \bar{a}_1\ne \bar{a}_2. $$
  3. 3.

    No junk: \(\mathcal {A}\) has no proper \(\varSigma \)-subalgebra containing \(em(X)\).

As any free construction [10], the universal property in Proposition 1 ensures that we can extend the assignments \(X\mapsto \mathcal {T}_\varSigma (X)\) to a functor \(\mathcal {T}_\varSigma (\_\,):\mathsf {Set}\rightarrow \mathsf {Alg}{(\varSigma )}\) that is left-adjoint to the forgetful functor \(|\_\,|:\mathsf {Alg}{(\varSigma )}\rightarrow \mathsf {Set}\). The adjunction

is the fundament for the area of algebraic specifications as the two volumes [8, 9] exemplify. Just to mention, that any variant of equational and/or first-order specifications is syntactically based on terms while the semantics relies on the uniqueness of the evaluation of terms w.r.t. variable assignments. And, not to forget, the Kleisli category of this adjunction provides us a substitution calculus: A substitution of terms for variables is a morphism in the Kleisli category, i.e., a map \(\sigma :X\rightarrow T_\varSigma (Y)\). The corresponding extended map describes the simultaneous substitution of all variables x in \(\varSigma \)-terms on \(X\) by the corresponding terms . The composition of two substitutions \(\sigma :X\rightarrow T_\varSigma (Y)\) and \(\delta :Y\rightarrow T_\varSigma (Z)\) is given by \(\delta ^*\circ \sigma :X\rightarrow T_\varSigma (Z)\).

3 From Algebras to Graph Algebras

As graphs we consider “directed multigraphs” [7]. A graph \(G=(G_V,G_E, \mathsf {sr}^G, \mathsf {tg}^G)\) consists of a set \(G_V\) of vertices, a set \(G_E\) of edges, and two maps \(\mathsf {sr}^G,\mathsf {tg}^G:G_E\rightarrow G_V\). A homomorphism \(\varphi =(\varphi _V,\varphi _E)\) between two graphs \(G=(G_V,G_E, \mathsf {sr}^G, \mathsf {tg}^G)\) and \(H=(H_V,H_E, \mathsf {sr}^H, \mathsf {tg}^H)\) consists of two maps \(\varphi _V:H_V\rightarrow G_V\) and \(\varphi _E:H_E\rightarrow G_E\) such that \(\varphi _V\circ \mathsf {sr}^G=\mathsf {sr}^H\circ \varphi _E\) and \(\varphi _V\circ \mathsf {tg}^G=\mathsf {tg}^H\circ \varphi _E\).

The identity graph homomorphism on a graph \(G\) is the pair \(id_G=(id_{G_V},id_{G_E})\) of identity maps and graph homomorphisms are composed componentwise. By \(\mathsf {Graph}\) we denote the category with graphs as objects and graph homomorphisms as morphisms. To establish the concept of graph algebras, we need, first, an adequate concept of signature.

Definition 3

(Graph signature). A graph signature \(\varGamma =(OP,I,R)\) is given by a finite set OP of operation symbols and two maps \(I\) and \(R\) assigning to each operation symbol \(\omega \in OP\) a finite graph \(I(\omega )\), its input arity, and a finite graph \(R(\omega )\), its result arity, respectively. Moreover, we assume that there is an inclusion \(\iota _\omega :I(\omega )\hookrightarrow R(\omega )\) between the two arity graphs.

To substantiate this definition, we discuss, in more detail, the transition from algebraic signatures to graph signatures.

Let \(I_n=\{in_1,\ldots ,in_n\}\) be a set of indices. We can consider an n-tuple \(\bar{a}=(a_1,\ldots ,a_n)\) of elements from a set \(A\) as a representation of a map \(a:I_n\rightarrow A\) where \(a_i=a(in_i)\) for all \(1\le i\le n\). The empty tuple () represents, in this view, the unique map from the empty set \(I_0=\emptyset \) into \(A\).

For any \(n\in \mathbb {N}\) there is a bijection between \(A^n\) and the set \(A^{I_n}\) of all maps from \(I_n\) into \(A\), thus we can consider maps \(a\in A^{I_n}\) as inputs for operations in a \(\varSigma \)-algebra \(\mathcal {A}\). What about the output? Algebraic operations give only a single value as output thus we can consider the codomain of an operation in \(\mathcal {A}\) as the set \(A^{O}\) of all maps from a singleton \(O=\{out\}\) into \(A\). From this viewpoint, we can consider the declaration of an operation symbol \(\omega \) with \(ar(\omega )=n\) as declaring a span \(I_n\hookleftarrow \emptyset \hookrightarrow O\) of set inclusions, where the corresponding operation in a \(\varSigma \)-algebra \(\mathcal {A}\) would be a map from \(A^{I_n}\) into \(A^{O}\).

Operations are assumed, however, to have no side effects. This means that the input is neither deleted nor changed. In such a way, we can consider the declaration of the arity of an operation symbol \(\omega \) as declaring a set inclusion \(\iota _\omega :I_n\hookrightarrow I_n\cup O\) (obtained by pushing out the above span of inclusions). The corresponding operation in \(\mathcal {A}\) becomes then a map

$$\begin{aligned} \omega ^\mathcal {A}:A^{I_n}\longrightarrow A^{I_n\cup O}\quad \text{ such } \text{ that }\; a=\omega ^\mathcal {A}(a)\circ \iota _\omega \;\text{ for } \text{ all } \; a\in A^{I_n}. \end{aligned}$$
(3)

We can recognize the same pattern in “graph operations”, like composition of morphisms and limit/colimit constructions in categories, for example. There are, however, three essential differences to the case of algebraic operations:

  1. 1.

    There are two different kinds of input items, namely vertices and edges.

  2. 2.

    Operations can produce arbitrary many output items instead of exactly one.

  3. 3.

    To relate output edges in an appropriate way to the input, we have to work with non-empty “boundary graphs” instead of just the empty set.

As an example we consider the construction of pullbacks. Let a category \(C\) with pullbacks be given and let \(|{C}|\) denote the underlying graph of \(C\). To turn the existence of pullbacks into an operation, we have to choose for any cospan \(A{\mathop {\rightarrow }\limits ^{f}}C{\mathop {\leftarrow }\limits ^{g}}B\) in \(C\) one of the existing pullbacks, i.e., we have to choose an object \(D\) and morphisms \(g^*:D\rightarrow A\), \(f^*:D\rightarrow B\) such that the resulting square is a pullback in \(C\).

The input arity of a corresponding operation symbol \(\mathsf {pb}\) can be described by the graph \(\mathsf {Cospan}=(iv_1{\mathop {\longrightarrow }\limits ^{ie_1}}iv_3{\mathop {\longleftarrow }\limits ^{ie_2}}iv_2)\), i.e., a cospan in \(C\) is a graph homomorphism from \(\mathsf {Cospan}\) into \(|{C}|\). Here, “iv” stands for input vertex while “ie” refers to input edge. We will often use the term binding for these graph homomorphisms. The output arity of the operation could be described by the graph \(\mathsf {Span}=(iv_1{\mathop {\longleftarrow }\limits ^{oe_2}}ov{\mathop {\longrightarrow }\limits ^{oe_1}}iv_2)\), where “ov” stands for output vertex while “oe” refers to output edge. The “boundary graph” \(\mathsf {\underline{2}}\), consisting of the two vertices \(iv_1\) and \(iv_2\), connects the output items with the input items. Instead of a span of graph inclusions \(\;\mathsf {Cospan}\hookleftarrow \mathsf {\underline{2}}\hookrightarrow \mathsf {Span}\;\) we consider, however, the inclusion \(\iota _{\mathsf {pb}}\) of the graph \(\mathsf {Cospan}\) into the graph \(\mathsf {Square}\),

obtained by pushing out the above span of graph inclusions, as the declaration of the arity of the operation symbol \(\mathsf {pb}\).

Convention 4

(Graph signature). For notational convenience we use canonical names for input vertices and edges. For a given operation symbol \(\omega \in OP\), we denote the elements of \(I(\omega )_V\) by \(\{iv_1,\ldots ,iv_{nv_\omega }\}\) and the elements of \(I(\omega )_E\) by \(\{ie_1,\ldots ,ie_{ne_\omega }\}\), where \(nv_\omega \) and \(ne_\omega \) are the numbers of vertices and edges in \(I(\omega )\) resp. Output vertices and edges will be denoted by \(ov_i\) and \(oe_j\).

Example 2

(Graph signature). We consider a graph signature \(\varGamma =(OP,I,R)\) with \(OP=\{\mathsf {pb},\mathsf {comp},\mathsf {id},\mathsf {ini}\}\). For the operation symbol \(\mathsf {pb}\) we declare \(I(\mathsf {pb})=\mathsf {Cospan}\) and \(R(\mathsf {pb})=\mathsf {Square}\). The arity of the composition operation symbol \(\mathsf {comp}\) is given by the following inclusion of graphs

The input arity of \(\mathsf {id}\) is the graph \(\mathsf {\underline{1}}\) with exactly one vertex iv and the result arity is the graph \(\mathsf {Loop}\) with exactly one vertex iv and one edge oe. Finally, the input arity of \(\mathsf {ini}\) is the empty graph \(\underline{\emptyset }\), and the result arity is a graph \(\mathsf {\underline{1}}\) with exactly one vertex ov. That is, \(\mathsf {ini}\) is a constant symbol with a trivial result arity, but in general the result arity of a constant could be any finite graph!

For graphs \(G\) and \(H\) we denote by \(G^H\) the set of all graph homomorphisms from \(H\) into \(G\). A fixed choice of pullbacks in category \(C\) gives rise to a map

$$ \mathsf {pb}^C:|{C}|^{\mathsf {Cospan}}\longrightarrow |{C}|^{\mathsf {Square}} $$

such that \(b=pb^C(b)\circ \iota _{pb}\) for all bindings \(b:\mathsf {Cospan}\rightarrow |{C}|\).

Generalizing the pullback example, we coin now the new concept of graph algebra.

Definition 5

(Graph algebra). For a graph signature \(\varGamma =(OP,I,R)\) a \(\varGamma \) -algebra \(\mathcal {G}=(G,OP^\mathcal {G})\) is given by a (carrier) graph \(G=(G_V,G_E,\mathsf {sr}^G,\mathsf {tg}^G)\), also denoted by \(|\mathcal {G}|\), and a family \(OP^\mathcal {G}=(\omega ^\mathcal {G}:G^{I(\omega )}\rightarrow G^{R(\omega )}\mid \omega \in OP)\) of maps such that \(b=\omega ^\mathcal {G}(b)\circ \iota _\omega \) for all \(\omega \in OP\) and all \(b\in G^{I(\omega )}\). These maps will be called graph operations.

For a vertex \(v\in R(\omega )_V\) and edge \(e\in R(\omega )_E\), we write \(\omega ^\mathcal {G}_V(b)(v)\) and \(\omega ^\mathcal {G}_E(b)(e)\) rather than \(\omega ^\mathcal {G}(b)_V(v)\) and \(\omega ^\mathcal {G}(b)_E(e)\). This eases reading formulas with b defined by long tuples. We will also omit VE subindices if it eases reading formulas.

For any graph \(G\) there is exactly one graph homomorphism \(\underline{\emptyset }_G:\underline{\emptyset }\rightarrow G\), i.e., \(G^{\underline{\emptyset }}=\{\underline{\emptyset }_G\}\) is a singleton, thus for any constant symbol \(c\in OP\), i.e., \(I(c)=\underline{\emptyset }\), the corresponding graph operation in a graph \(\varGamma \)-algebra \(\mathcal {G}\) just points at a subgraph of \(G\), namely the image of \(R(c)\) w.r.t. \(c^\mathcal {G}(\underline{\emptyset }_G)\).

Example 3

(Graph algebra). The composition in a category \(C\) can be presented as a graph operation \(\mathsf {comp}^C:|{C}|^{I(\mathsf {comp})}\rightarrow |{C}|^{R(\mathsf {comp})}\) where the only output of the graph operation is given by \(\mathsf {comp}^C_E(b)(oe)=b(ie_2)\circ b(ie_1)\) for all bindings \(b:I(\mathsf {comp})\rightarrow |{C}|\). Note, that \(\mathsf {comp}^C\) is a total operation. The identity in \(C\) gives another graph operation \(\mathsf {id}^C:|{C}|^{\mathsf {\underline{1}}}\rightarrow |{C}|^{\mathsf {Loop}}\) such that \(\mathsf {id}^C_E(b)(oe)=id_{b(iv)}\).

If \(C\) has pullbacks, we can define a graph operation \(\mathsf {pb}^C:|{C}|^{\mathsf {Cospan}}\rightarrow |{C}|^{\mathsf {Square}}\), in such a way, that for any binding \(b:\mathsf {Cospan}\rightarrow |{C}|\) the result \(\mathsf {pb}^C(b):\mathsf {Square}\rightarrow |{C}|\) is a chosen pullback diagram. And, if \(C\) has initial objects, we can define a constant \(\mathsf {ini}^C:|{C}|^{\underline{\emptyset }}\rightarrow |{C}|^{\mathsf {\underline{1}}}\), in such a way, that \(\mathsf {ini}^C_V(\underline{\emptyset }_G)(ov)\) is a (chosen) initial object in \(C\).

A \(\varGamma \)-algebra \(\mathcal {G}\) is a subalgebra of a \(\varGamma \)-algebra \(\mathcal {H}\) if \(G\) is a subgraph of \(H\) and \(in\circ \omega ^{\mathcal {G}}(b)=\omega ^{\mathcal {H}}(in\circ b)\) for all \(\omega \in OP\) and all \(b\in G^{I(\omega )}\), where \(in:G\rightarrow H\) is the corresponding inclusion graph homomorphism (compare Definition 6). This means that the subgraph \(G\) of the carrier of \(\mathcal {H}\) has to be closed under the operations in \(\mathcal {H}\) in the sense that for all \(\omega \in OP\) and all \(b\in G^{I(\omega )}\) the image \(\omega ^{\mathcal {H}}(in\circ b)(R(\omega ))\) is a subgraph of \(G\). Especially, \(G\) has to contain the image graph \(c^\mathcal {H}(\underline{\emptyset }_H)(R(c))\) for any constant symbol \(c\) in OP.

A functor \(\mathfrak {F}:C\rightarrow D\) between two categories \(C\) and \(D\) is a graph homomorphism \(\mathfrak {F}:|{C}|\rightarrow |{D}|\) compatible with composition, i.e., for all morphisms \(f:A\rightarrow B\), \(g:B\rightarrow C\) in \(C\) we have \(\mathfrak {F}(g\circ f)=\mathfrak {F}(g)\circ \mathfrak {F}(f)\). We can reformulate this condition in terms of the corresponding graph operations \(comp^C\) and \(comp^D\) by requiring that the following diagram commutes:

That is, for any binding \(b:I(\mathsf {comp})\rightarrow |{C}|\) we require (compare (1))

$$\mathfrak {F}\circ \mathsf {comp}^C(b)=\mathsf {comp}^D(\mathfrak {F}\circ b). $$

This example motivates our concept of homomorphisms between graph algebras.

Definition 6

A \(\varGamma \) -homomorphism \(\varphi :\mathcal {G}\rightarrow \mathcal {H}\) between two \(\varGamma \)-algebras \(\mathcal {G}=(G,OP^\mathcal {G})\) and \(\mathcal {H}=(H,OP^\mathcal {H})\) is a graph homomorphism \(\varphi :G\rightarrow H\) such that

$$\begin{aligned} \varphi \circ \omega ^\mathcal {G}(b)=\omega ^\mathcal {H}(\varphi \circ b)\quad \text{ for } \text{ all }\;\; \omega \in OP \;\text{ and } \text{ all } \;\; b\in G^{I(\omega )}. \end{aligned}$$
(4)

Example 4

Given two categories \(C\) and \(D\) with pullback operations, a functor \(\mathfrak {F}:C\rightarrow D\), that preserves pullbacks, establishes a graph algebra homomorphism only if it maps chosen pullbacks in \(C\) to chosen pullbacks in \(D\).

The composition \(\psi \circ \varphi :\mathcal {G}\rightarrow \mathcal {K}\) of \(\varGamma \)-homomorphisms \(\varphi :\mathcal {G}\rightarrow \mathcal {H}\) and \(\psi :\mathcal {H}\rightarrow \mathcal {K}\) is given by the composition \(\psi \circ \varphi :G\rightarrow K\) of the underlying graph homomorphisms \(\varphi :G\rightarrow H\) and \(\psi :H\rightarrow K\). For any graph \(\varGamma \)-algebra \(\mathcal {G}\) the identity \(\varGamma \)-homomorphism \(id_\mathcal {G}:\mathcal {G}\rightarrow \mathcal {G}\) is given by the identity graph homomorphism \(id_G:G\rightarrow G\). In such a way, \(\varGamma \)-algebras and \(\varGamma \)-homomorphisms constitute a category \(\mathsf {GAlg}{(\varGamma )}\) where the assignments \(\mathcal {G}\mapsto |\mathcal {G}|\) and \((\varphi :\mathcal {G}\rightarrow \mathcal {H})\mapsto (\varphi :|\mathcal {G}|\rightarrow |\mathcal {H}|)\) define a forgetful functor \(|\_\,|:\mathsf {GAlg}{(\varGamma )}\rightarrow \mathsf {Graph}\).

We conclude this section with a discussion how algebras can be transformed into corresponding graph algebras. Any set \(A\) can be transformed into a graph \(\mathfrak {V}(A)\) with an empty set of edges, and any map \(f:A\rightarrow B\) provides trivially a graph homomorphism \(\mathfrak {V}(f):\mathfrak {V}(A)\rightarrow \mathfrak {V}(B)\) thus the assignments \(A\mapsto \mathfrak {V}(A)\) and \((f:A\rightarrow B)\mapsto (\mathfrak {V}(f):\mathfrak {V}(A)\rightarrow \mathfrak {V}(B))\) define a functor \(\mathfrak {V}:\mathsf {Set}\rightarrow \mathsf {Graph}\).

Turning back to the discussion, at the beginning of this section, it becomes obvious that we can transform any algebraic signature \(\varSigma =(F,ar)\) into a graph signature \(\varGamma _\varSigma =(F,I_\varSigma , R_\varSigma )\) with \(I_\varSigma (\omega )=\mathfrak {V}(I_{ar(\omega )})\) and \(R_\varSigma (\omega )=\mathfrak {V}(I_{ar(\omega )}\cup \{ov\})\). It is easy to see that any \(\varSigma \)-algebra can be transformed into a \(\varGamma _\varSigma \) algebra \(\mathfrak {G}(\mathcal {A})\), and any \(\varSigma \)-algebra homomorphism \(f:\mathcal {A}\rightarrow \mathcal {B}\) gives rise to a \(\varGamma _\varSigma \)-homomorphism \(\mathfrak {V}(f):\mathfrak {G}(\mathcal {A})\rightarrow \mathfrak {G}(\mathcal {B})\).

Finally, the assignments \(\mathcal {A}\mapsto \mathfrak {G}(\mathcal {A})\) and \((f:\mathcal {A}\rightarrow \mathcal {B})\mapsto (\mathfrak {V}(f):\mathfrak {G}(\mathcal {A})\rightarrow \mathfrak {G}(\mathcal {B}))\) define an embedding \(\mathfrak {G}:\mathsf {Alg}{(\varSigma )}\rightarrow \mathsf {GAlg}{(\varGamma _\varSigma )}\) where we have, by construction, that \(|\_\,|\circ \mathfrak {G}=\mathfrak {V}\circ |\_\,|\) (see Fig. 1). Note, that \(\mathsf {Alg}{(\varSigma )}\) and \(\mathsf {GAlg}{(\varGamma _\varSigma )}\) are, in general, neither isomorphic nor equivalent since the carrier of a \(\varGamma _\varSigma \)-algebra can have edges even if the operations only work on vertices.

Fig. 1.
figure 1

Two compatible adjunctions

In the next section we will discuss the construction of free \(\varGamma \)-algebras for arbitrary graph signatures \(\varGamma \) providing a functor \(\mathcal {T}_\varGamma (\_\,):\mathsf {Graph}\rightarrow \mathsf {GAlg}{(\varGamma )}\) to be shown to be left adjoint to the forgetful functor \(|\_\,|:\mathsf {GAlg}{(\varGamma )}\rightarrow \mathsf {Graph}\). This construction should generalize the construction of term algebras, in the sense, that for any algebraic signature \(\varSigma \) there is a natural isomorphism between the two functors \(\mathfrak {G}\circ \mathcal {T}_\varSigma (\_\,)\) and \(\mathcal {T}_{\varGamma _\varSigma }(\_\,)\circ \mathfrak {V}\) from \(\mathsf {Set}\) into \(\mathsf {GAlg}{(\varGamma _\varSigma )}\).

4 From Terms to Graph Terms

To have a guideline how to define terms in the setting of graph algebras, we analyze the construction of terms in Definition 1 in the light a graph signatures. As example we consider the algebraic signature \(\varSigma \) in Example 1.

Fig. 2.
figure 2

Term construction as pushout

For the corresponding graph signature \(\varGamma _\varSigma \) the graph inclusion \(\iota _\mathsf {p}: I_{\varGamma _\varSigma }(\mathsf {p})\rightarrow R_{\varGamma _\varSigma }(\mathsf {p})\) is depicted in the upper part of the diagram in Fig. 2. In the left lower corner we depict the set of terms that have been constructed until now. Applying rule 3 in Definition 1 for \(\omega =\mathsf {p}\) and two already constructed terms \(t_1,t_2\) means to apply \(\iota _\mathsf {p}\), considered as a graph transformation rule, for the binding \(b=(in_1\mapsto t_1, in_2\mapsto t_2)\) and to construct a pushout, i.e., to produce exactly one new vertex new, as depicted in the lower right corner in Fig. 2. Denoting this new item by the term \(\mathsf {p}\langle t_1,t_2\rangle \), solves two problems:

  1. 1.

    The term notation provides a uniform mechanism to create identifiers for new graph items introduced by applying non-deleting injective graph transformation rules (at least for graphs without edges). This problem is seldom addressed in the graph transformation literature.

  2. 2.

    The term \(\mathsf {p}\langle t_1,t_2\rangle \) codes all the information about the pushout that has been creating the new item:

    1. (a)

      The symbol “\(\mathsf {p}\)” identifies the rule that has been applied and, by consulting the signature, we find the necessary information about the input and result arity, respectively.

    2. (b)

      The string “\(t_1,t_2\)” codes the actual binding (match) \(b=(in_1\mapsto t_1, in_2\mapsto t_2)\) for the input arity.

    3. (c)

      Since there is exactly one new item, we do have all information to identify uniquely the new item, and thus to define the resulting binding \(b^*\).

In such a way, the term notation offers two possibilities to deal with the problem of applying the same rule twice for the same binding:

  1. 1.

    A priori: Before we apply a rule for a certain binding, we check the term denotations of all the items that have already been constructed. In such a way, we can find out, if the rule had already been applied for this binding. If this is the case, we do not apply the rule. Note, that the idea to use a rule as its own negative application condition [7], would be too rigid here. In case of the operation \(\mathsf {p}\), e.g., we couldn’t apply \(\iota _\mathsf {p}\) to any graph with more than two vertices.

  2. 2.

    A posteriori: After applying a rule another time for a certain binding we repair the mistake silently by identifying the newly generated items with the “same” already existing items by the assumption that sets are extensional.

We like to adapt the silent a posteriori reparation mechanism and extend the term notation correspondingly. To deal with the rules arising from declaring arities of graph operations (see Definition 3) we have to address two problems: (1) An item can be of two different kinds - vertex or edge, and (2) there can be any finite number of output items instead of exactly one. To tackle problem (1), we will use for each kind a separate string of given terms, instead of just one string. And, by using output items as additional parts of terms, we solve problem (2).

In the context of graph algebras, we consider a collection of variables to be a graph rather than a set. Given a graph signature \(\varGamma =(OP,I,R)\) and a graph \(X\) of variables, we will define (graph) \(\varGamma \)-terms over \(X\) using the following symbols/names: operation symbols from \(OP\), names of output vertices and edges in \(R(\omega )\setminus I(\omega )\) for all \(\omega \in OP\), and auxiliary symbols like commas and brackets.

Convention 7

For a graph \(G\), operation symbol \(\omega \in OP\), and binding \(b:I(\omega )\rightarrow G\), we write the strings “\(b(iv_1)\ldots b(iv_{nv_\omega })\)” and “\(b(ie_1)\ldots b(ie_{ne_\omega })\)” of, resp., vertices and edges in \(G\) without commas and brackets, denote them by \(\overline{b}_V\) and \(\overline{b}_E\) resp., and write \(\overline{b}\) for \(\overline{b}_V;\,\overline{b}_E\). Extensionality ensures that \(b1=b2\) iff \(\overline{b1}=\overline{b2}\) so that we can omit the overline bar.

Now we are prepared to define graph terms in parallel to the traditional definition of terms in Definition 1.

Definition 8

(Graph terms). Let be given a graph signature \(\varGamma =(OP,I,R)\) and a graph \(X\) of variables. The graph \(T_\varGamma (X)\) of all graph \(\varGamma \) -terms on \(X\) is the smallest graph, which satisfies the following three conditions:

\(\mathrm{(Variables).}\)  \(T_\varGamma (X)\) contains the graph of variables, \(X\sqsubseteq T_\varGamma (X)\);

\(\mathrm{(Constants).}\) For all \(c\in OP\) with \(I(c)=\underline{\emptyset }\), graph \(T_\varGamma (X)\) contains

  • for each \(ov\in R(c)_V\), tuple \(\langle {ov},{c},{\langle \rangle }\rangle \) as a vertex,

  • for each \(oe\in R(c)_E\), tuple \(\langle {oe},{c},{\langle \rangle }\rangle \) as an edge, where

\(sc^{T_\varGamma (X)}(\langle {oe},{c},{\langle \rangle }\rangle )=\langle {sc^{R(c)}(oe)},{c},{\langle \rangle }\rangle \) and \(tg^{T_\varGamma (X)}(\langle {oe},{c},{\langle \rangle }\rangle )=\langle {tg^{R(c)}(oe)}{c}{\langle \rangle \rangle }\); \(\mathrm{(Operations)}\) For all \(\omega \in OP\) with \(I(\omega )\ne \underline{\emptyset }\) and any \(b:I(\omega )\rightarrow T_\varGamma (X)\), graph \(T_\varGamma (X)\) contains

  • for each \(ov\in R(\omega )_V\setminus I(\omega )_V\), tuple \(\langle {ov},{\omega },{b}\rangle \) as a vertexFootnote 1,

  • for each \(oe\in R(\omega )_E\setminus I(\omega )_E\), tuple \(\langle {oe},{\omega },{b}\rangle \) as an edgeFootnote 2, whose source and target vertices are defined as follows:

Example 5

As an example we consider the graph signature \(\varGamma \) from Example 2 and the graph \(X\) depicted in the last line in the following diagram.

Vertex \(tv_0\) is generated by the rule \(\iota _{\mathsf {ini}}\), i.e., \(tv_0=\langle {ov},{ini},{\langle \rangle }\rangle \). Vertices \(tv_1,\ldots ,tv_4\) and edges \(te_1,\ldots ,te_8\) are generated by the following four applications bi, \(i=1..4\) of the rule \(\iota _{\mathsf {pb}}\) (as there are no isolated vertices in the arity of \(\mathsf {pb}\), it’s sufficient to specify the values of bindings on edges):

$$ \begin{array}{c||c|c|c|c|} &{} b1 &{} b2 &{} b3 &{} b4 \\ \hline \hline ie_1 &{} xe_1 &{} xe_3 &{} te_2 &{} xe_4 \\ ie_2 &{} xe_2 &{} xe_4 &{} te_3 &{} xe_4 \end{array} $$

which produce

figure a

Note, that the edge pair \(te_7\) and \(te_8\) could be declared as kernel of edge \(xe_4\). Finally, edges \(te_9\) and \(te_{10}\) are obtained by two applications of rule \(\iota _{\mathsf {comp}}\): \(b5(ie_1)= te_1\), \(b5(ie_2)=xe_1\), and \(b6(ie_1)= te_2\), \(b5(ie_2)=xe_2\), which produce \(te_9=\langle {oe},{\mathsf {comp}},{b5}\rangle \), \(te_{10}=\langle {oe},{\mathsf {comp}},{b6}\rangle \).

Analogously, to the case of terms, we can interpret the construction of graph terms as operations in special \(\varGamma \)-algebras:

Definition 9

(Graph term algebra). For a graph \(X\) of variables we denote by \(\mathcal {T}_\varGamma (X)=(T_\varGamma (X),OP^{\mathcal {T}_\varGamma (X)})\) the \(\varGamma \)-algebra of graph \(\varGamma \)-terms on \(X\) with:

\(\mathrm{(Constants).}\) For all \(c\in OP\) with \(I(c)=\underline{\emptyset }\)

$$\begin{aligned} c^{\mathcal {T}_\varGamma (X)}_V(\underline{\emptyset }_G)(ov)=\;\langle {ov},{c},{\langle \rangle }\rangle \quad \text{ for } \text{ all }\; ov\in R(c)_V, \end{aligned}$$
$$\begin{aligned} c^{\mathcal {T}_\varGamma (X)}_E(\underline{\emptyset }_G)(oe)= \;\langle {oe},{c},{\langle \rangle }\rangle \quad \text{ for } \text{ all }\; oe\in R(c)_E; \end{aligned}$$

\(\mathrm{(Operations).}\) For all \(\omega \in OP\) with \(I(\omega )\ne \underline{\emptyset }\) and all \(b\in T_\varGamma (X)^{I(\omega )}\)

The definitions ensure that all resulting bindings \(\omega ^{\mathcal {T}_\varGamma (X)}(b)\in T_\varGamma (X)^{R(\omega )}\) are indeed graph homomorphisms and that \(b=\omega ^{\mathcal {T}_\varGamma (X)}(b)\circ \iota _\omega \), as required.

The condition “the smallest graph” in Definition 8 ensures that \(\mathcal {T}_\varGamma (X)\) has “no junk”, i.e., no proper subalgebra containing \(X\), and the graph term notation ensures that there is “no confusion”, i.e., variables are not identified with items introduced by operation applications. Moreover, items, introduced by different operation applications, are not identified either.

More structurally, “no confusion” means, especially, that for any \(\omega \in OP\) and any \(b\in T_\varGamma (X)^{I(\omega )}\), the commutative triangle below (on the left) factorizes, by epi-mono-factorization \(b=b^m\circ b^e\) and \(\omega ^{\mathcal {T}_\varGamma (X)}(b)=\omega ^{\mathcal {T}_\varGamma (X)}(b)^m\circ \omega ^{\mathcal {T}_\varGamma (X)}(b)^e\), into a pushout square and a commutative triangle (below on the right).

Proposition 2

(Free graph algebras). For each graph \(X\) the graph term \(\varGamma \)-algebra \(\mathcal {T}_\varGamma (X)=(T_\varGamma (X),OP^{\mathcal {T}_\varGamma (X)})\) has the following universal property: For any \(\varGamma \)-algebra \(\mathcal {G}\) and any variable assignment \(\alpha :X\rightarrow |\mathcal {G}|\) there exists a unique \(\varGamma \)-homomorphism \(\alpha ^*:\mathcal {T}_\varGamma (X)\rightarrow \mathcal {G}\) such that: \(\alpha ^*\circ in_X= \alpha \).

Proof

We prove by structural induction according to Definition 8:

(Variables). In this basic case the defining condition forces \(\alpha ^*_V(xv)=\alpha _V(xv)\) for all \(xv\in X_V\) and \(\alpha ^*_E(xe)=\alpha _E(xe)\) for all \(xe\in X_E\).

(Constants). In this basic case the definition of operations in \(\mathcal {T}_\varGamma (X)\) and the desired homomorphism condition for \(\alpha ^*\) forces for all \(ov\in R(c)\)

$$\begin{aligned} \alpha ^*_V(\langle {ov},{c},{\langle \rangle }\rangle )=\alpha ^*_V(c_V^{\mathcal {T}_\varGamma (X)}(\underline{\emptyset }_{T_\varGamma (X)})(ov)) =c_V^\mathcal {G}(\alpha ^*\circ \underline{\emptyset }_{T_\varGamma (X)})(ov) =c_V^\mathcal {G}(\underline{\emptyset }_\mathcal {G})(ov) \end{aligned}$$

and for all \(oe\in R(c)_E\) we get, analogously, \(\alpha ^*_E(\langle {oe},{c},{\langle \rangle }\rangle )=c_E^\mathcal {G}(\underline{\emptyset }_\mathcal {G})(oe)\).

(Operations). The definition of operations in \(\mathcal {T}_\varGamma (X)\) and the desired homomorphism condition forces \(\alpha ^*\) to be defined according to a corresponding recursion scheme for all \(\omega \in OP\) with \(I(\omega )\ne \underline{\emptyset }\) and all \(b\in T_\varGamma (X)^{I(\omega )}\): The induction hypothesis is that \(\alpha ^*\) is already defined on the subgraph \(b(I(\omega ))\sqsubseteq T_\varGamma (X)\). We denote the restriction of \(\alpha ^*\) to \(b(I(\omega ))\) by \(\alpha ^*_b\). In the induction step we extend \(\alpha ^*\) to the subgraph \(\omega ^{\mathcal {T}_\varGamma (X)}(b)(R(\omega ))\sqsubseteq T_\varGamma (X)\) (that contains \(b(I(\omega ))\)), i.e., to all graph terms that have been constructed exactly by applying rule \(\iota _\omega \) for the binding b: For all \(ov\in R(\omega )_V\) we get

$$\begin{aligned} \alpha ^*_V(\langle {ov},{\omega },{b}\rangle )=\alpha ^*_V(\omega ^{\mathcal {T}_\varGamma (X)}_V(b)(ov)) =\omega _V^\mathcal {G}(\alpha ^*_b\circ b^e)(ov) \end{aligned}$$

and for all \(oe\in R(\omega )_E\) we get \(\alpha ^*_E(\langle {oe},{\omega },{b}\rangle )=\omega _E^\mathcal {G}(\alpha ^*_b\circ b^e)(oe)\).

More structurally considered, the induction step constructs the unique mediating morphism from \(\omega ^{\mathcal {T}_\varGamma (X)}(b)(R(\omega ))\) into \(G\) in the following diagram (Keep in mind that \(\alpha ^*\circ b^e=\omega ^\mathcal {G}(\alpha ^*_b\circ b^e)\circ \iota _\omega \) since \(\omega ^\mathcal {G}\) is a graph operation.):

A more traditional presentation of the induction step, analogously to (2), can be given if we use for the binding \(b\in T_\varGamma (X)^{I(\omega )}\) the abbreviations \(tv_j=b(iv_j)\), \(1\le j\le nv_\omega \) and \(te_k=b(ie_k)\), \(1\le k\le ne_\omega \) (compare Convention 7), consider tuples as presentations of finite maps, as discussed at the beginning of Sect. 3, and represent the two maps constituting a binding for \(I(\omega )\) in \(G\) as a sequence of vertices and edges of length \(nv_\omega +ne_\omega \) in \(G\): For all \(ov\in R(\omega )_V\), we get

$$\begin{aligned}&\alpha ^*_V(\langle {ov},{\omega },{ tv_1\ldots tv_{nv_\omega } te_1 \ldots te_{ne_\omega } }\rangle ) \\= & {} \omega _V^\mathcal {G}(\alpha ^*_V(tv_1)\ldots \alpha ^*_V(tv_{nv_\omega }) \alpha ^*_E(te_1)\ldots \alpha ^*_E(te_{ne_\omega }))(ov). \end{aligned}$$

The universal property in Proposition 2 ensures that we can extend the assignments \(X\mapsto \mathcal {T}_\varGamma (X)\) to a functor \(\mathcal {T}_\varGamma (\_\,):\mathsf {Graph}\rightarrow \mathsf {GAlg}{(\varGamma )}\) that is left-adjoint to the forgetful functor \(|\_\,|:\mathsf {GAlg}{(\varGamma )}\rightarrow \mathsf {Graph}\) (see Fig. 1). That the adjunction \(\mathcal {T}_\varGamma (\_\,)\dashv |\_\,|\) generalizes the construction of term algebras, in the sense, that for any algebraic signature \(\varSigma \) there is a natural isomorphism between the two functors \(\mathfrak {G}\circ \mathcal {T}_\varSigma (\_\,)\) and \(\mathcal {T}_{\varGamma _\varSigma }(\_\,)\circ \mathfrak {V}\) from \(\mathsf {Set}\) into \(\mathsf {GAlg}{(\varGamma _\varSigma )}\)(see Fig. 1) can be shown straightforwardly.

Establishing the adjunctions \(\mathcal {T}_\varGamma (\_\,)\dashv |\_\,|\) is the main result of the paper. Since the new adjunctions generalize the adjunctions \(\mathcal {T}_\varSigma (\_\,)\dashv |\_\,|\), we will be able to transfer smoothly many concepts, constructions, and results from the area of algebraic specifications to the new setting of graph algebras (see Sect. 6).

Equations, for example, can be defined as pairs of graph terms and can be used to formulate properties of graph operations. Associativity of composition, e.g., can be expressed by the equation (we recall Convention 7 about denotations of binding mappings)

$$\begin{aligned} \langle oe,\mathsf {comp},\langle oe,\mathsf {comp},xe_1xe_2\rangle xe_3\rangle = \langle oe, \mathsf {comp},xe_1\langle oe,\mathsf {comp},xe_2xe_3\rangle \rangle \end{aligned}$$

where \(X\) is the graph \((xv_1{\mathop {\rightarrow }\limits ^{xe_1}}xv_2{\mathop {\rightarrow }\limits ^{xe_2}}xv_3{\mathop {\rightarrow }\limits ^{xe_3}}xv_4)\). Since there are no isolated vertices in the arities of our sample operations we list only edge variables in the sample equations. We may also require that our choice of pullbacks is symmetric in the sense that the following equations are satisfied:

$$\begin{aligned} \langle {ov},{\mathsf {pb}},{xe_1xe_2}\rangle= & {} \langle {ov},{\mathsf {pb}},{xe_2xe_1}\rangle \\ \langle {oe_1},{\mathsf {pb}},{xe_1xe_2}\rangle= & {} \langle {oe_2},{\mathsf {pb}},{xe_2xe_1}\rangle \\ \langle {oe_2},{\mathsf {pb}},{xe_1xe_2}\rangle= & {} \langle {oe_1},{\mathsf {pb}},{xe_2xe_1}\rangle , \end{aligned}$$

where \(X\) is the graph \((xv_1{\mathop {\rightarrow }\limits ^{xe_1}}xv_3{\mathop {\leftarrow }\limits ^{xe_2}}xv_2)\). Note, that we can not summarize the three equations by a single (hypothetical) equation between bindings

$$\begin{aligned} \mathsf {pb}\langle xe_1xe_2\rangle = \mathsf {pb}\langle xe_2xe_1\rangle \end{aligned}$$

since \(oe_1\) and \(oe_2\) are interchanged in the last two equations above.

The Kleisli category of the new adjunction provides an appropriate substitution calculus. A substitution is an arrow in the Kleisli category, i.e., a graph homomorphism \(\sigma :X\rightarrow T_\varGamma (Y)\). The corresponding extended graph homomorphism \(\sigma ^*:T_\varGamma (X)\rightarrow T_\varGamma (Y)\) describes the simultaneous substitution of all variable vertices xv and variable edges xe in graph \(\varGamma \)-terms on \(X\) by the corresponding graph terms \(\sigma _V(xv)\in T_\varGamma (Y)_V\) or \(\sigma _E(xe)\in T_\varGamma (Y)_E\), respectively. The composition of two substitutions \(\sigma :X\rightarrow T_\varGamma (Y)\) and \(\delta :Y\rightarrow T_\varGamma (Z)\) is given by \(\delta ^*\circ \sigma :X\rightarrow T_\varGamma (Z)\). Substitutions \(\sigma :X\rightarrow T_\varGamma (Y)\) allow us, for example, to formalize the concepts of queries and views in databases [3].

Remark 1

(Universal properties). For a categorically minded reader, considering such operations as pullback and pushout without their universal properties does not make too much sense. Below we will show how to include universal properties into our framework of diagram operations. We will consider universality of pullbacks, but the method is quite general and applicable for any limit/colimit operation over graphs.

Commutativity of a pullback square can be expressed by the following equation

$$\langle oe,\mathsf {comp},\langle oe_1,\mathsf {pb},ie_1ie_2\rangle ie_2\rangle = \langle oe, \mathsf {comp},\langle oe_2,\mathsf {pb},ie_1ie_2\rangle ie_1\rangle $$

where operations \(\mathsf {pb}\) and \(\mathsf {comp}\) are defined in Example 3. Universal properties, however, are conditional statements thus we need a kind of implication to express them. The implications, we are looking for, are a further development of the sketch axioms in [11] (see also Sect. 5). Those implications are based on graph homomorphisms. To express the existence of mediating morphisms we consider, in case of pullbacks, the following inclusion of graphs:

where \(tv=\langle ov,\mathsf {pb}, xe_1xe_2\rangle \), \(te_1=\langle oe_2,\mathsf {pb}, xe_1xe_2\rangle \) and \(te_2=\langle oe_1,\mathsf {pb}, xe_1xe_2\rangle \). We denote the graph on the left-hand side by X and the graph on the right-hand side by Y. Since, m is the only item in Y, that is not in X or generated by X, respectively, the inclusion homomorphism allows us to formulate a conditional existence statement of the form

$$ \forall \, X.( prem_1 \; {\mathop {\Rightarrow }\limits ^{\iota }} \; \exists \, m.\; concl_1 )\quad \text{ where } $$
$$\begin{aligned} prem_1:= & {} \langle oe,\mathsf {comp}, xe_4xe_2\rangle = \langle oe, \mathsf {comp},xe_3xe_1\rangle \\ concl_1:= & {} \langle oe,\mathsf {comp},m\, te_1\rangle =xe_4 \wedge \langle oe,\mathsf {comp},m\, te_2\rangle =xe_3. \end{aligned}$$

A graph operation \(\mathsf {pb}^C:|{C}|^{\mathsf {Cospan}}\rightarrow |{C}|^{\mathsf {Square}}\), as in Example 3, satisfies this implication iff every binding \(b:X\rightarrow |C|\), that makes the premise \(prem_1\) true, can be extended to a binding \(\bar{b}:Y\rightarrow |C|\) with \(\bar{b}\circ \iota =b\) such that the following two conditions hold: (a) \(\bar{b}(te_1)=\langle oe_1,\mathsf {pb},xe_1xe_2\rangle \) and \(\bar{b}(te_2)=\langle oe_2,\mathsf {pb},xe_1xe_2\rangle \) and (b) the conclusion \(concl_1\) becomes true. Note, that condition (a) ensures that only an appropriate match for the edge m needs to be found.

To express the uniqueness of mediating morphisms we exploit a non-injective but surjective graph homomorphism \(\varphi :Y'\rightarrow Y\) where \(Y'\) is Y plus an additional edge \(m'\) from \(xv_4\) to tv. \(\varphi \) is the identity except that it maps m and \(m'\) in \(Y'\) to m in Y. The premise \(prem_2\) is given by two corresponding copies of \(concl_1\) above and the conclusion \(concl_2\) is just true. A graph operation \(\mathsf {pb}^C\) satisfies the implication \(\forall \, Y'.( prem_2 \; {\mathop {\Rightarrow }\limits ^{\varphi }} \; true)\) iff every binding \(b:Y'\rightarrow |C|\), that makes the premise \(prem_2\) true, can be extended to a binding \(\bar{b}:Y\rightarrow |C|\) with \(\bar{b}\circ \varphi =b\). In other words, there is no binding \(b:Y'\rightarrow |C|\) with \(\bar{b}(m)\ne \bar{b}(m)\) that makes the premise \(prem_2\) true.

5 Related Work

An abstract diagrammatic approach to logic, including a general notion of diagram predicates and their models (generalized sketches), and implications between diagram predicates (sketch axioms), was pioneered by Makkai in [11] (see also historical remarks in our paper [6]). However, Makkai did not work with diagram operations and algebras. Formal definitions of a (diagrammatic) graph operation and a graph algebra were introduced by the second author in [4], and many examples and discussions in the database context can be found in [3]. The latter paper also describes the construction of what they call sketch parsing. The idea is that any operation signature \(\varGamma \) gives rise to a predicate signature \(\varGamma ^*\) by forgetting the input arity parts in the entire operation arities. Then any \(\varGamma \)-term becomes a \(\varGamma ^*\)-sketch [6]. Parsing does the inverse: given an \(\varGamma ^*\)-sketch, it tries to convert it into an \(\varGamma \)-term. In these papers, graph terms are defined as trees labeled by diagrams respecting operation arities. In the present paper, we are more interested in the entire object of graph term algebra and its universal properties rather than in the notion of a single graph term. Neither of the papers above formally defined the graph term algebra and proved its universal properties.

Injective graph transformation rules have been studied extensively by Hartmut Ehrig and his co-authors (see [7]). The special feature of injective rules, elucidated in the paper, may shed new light on the “nature” of those rules.

6 Conclusion and Future Work

In the paper, we extended the classical construction of term algebra for operations over sets to the case of diagrammatic operations over graphs. We showed that any graph term algebra freely generated by applying graph operations to a given graph of variables is indeed free: it possesses the respective universal property in the category of graph algebras. This basic result shows that our definitions of graph operations and graph algebras work as we wanted, i.e., in parallel with the ordinary algebra case. Moreover, this result hopefully paves a way to a wider generalization of the core Universal Algebra framework for graph operations and graph algebras. In more detail, we aim at defining congruence relations, quotients and epi-mono factorizations for graph algebras, thus building what we could call Graph-based Universal Algebra. More abstractly, it would also be interesting to extend our result in [6] concerning institutions of generalized sketches to any of the envisaged logical extensions.

We see other interesting and useful extensions of the framework.

Typing. The step from unsorted to many-sorted algebras is relatively straightforward. In the same way, we see no principle problems to extend the framework, presented in this paper, to typed graphs [7]. This extension will be necessary to meet the situations in applications (compare [3, 12,13,14]).

Term Language. In the paper we considered two roles of ordinary terms and their extension for graph algebras. These two roles are (a) to denote elements in free algebras and (b) to provide induction/recursion schemes for evaluating the elements of free algebras in arbitrary algebras. However, terms are also used (c) to denote composed/derived operations in algebras. This role provides the foundation for functorial semantics and thus for a categorical approach to Universal Algebra. By extending the approach in [2], we plan to specify this role in the setting of graph algebras too.

From Graphs to Presheaf Toposes. To meet the spirit of the Festschrift, in the paper we focused on graph-based structures, which have been the basis for research on graph transformations in Hartmut’s group for decades [7]. The category of graphs, however, is a very simple instance of a quite general concept of a presheaf topos that encompasses 2-graphs, Petri nets, attributed graphs [7], and many other structures employed in computer science. There should be no principle problems to extend the definitions and results of the paper to the broader class of presheaf topoi.