Iteration Algebras for UnQL Graphs andCompleteness for Bisimulation
Makoto Hamana
Department of Computer Science, Gunma University, Japan
hamana@cs.gunma-u.ac.jp

This paper shows an application of Bloom and Ésik’s iteration algebras to model graph data in a graphdatabase query language. About twenty years ago, Buneman et al. developed a graph database querylanguage UnQL on the top of a functional meta-language UnCAL for describing and manipulating
graphs. Recently, the functional programming community has shown renewed interest in UnCAL,
because it provides an efficient graph transformation language which is useful for various applications, such as bidirectional computation. However, no mathematical semantics of UnQL/UnCAL
graphs has been developed. In this paper, we give an equational axiomatisation and algebraic semantics of UnCAL graphs. The main result of this paper is to prove that completeness of our equational
axioms for UnCAL for the original bisimulation of UnCAL graphs via iteration algebras. Anotherbenefit of algebraic semantics is a clean characterisation of structural recursion on graphs using free
iteration algebra.

1 Introduction
Graph database is used as a back-end of various web and net services, and therefore it is one of theimportant software systems in the Internet society. About twenty years ago, Buneman et al. [6, 7, 8]
developed a graph database query language UnQL (Unstructured data Query Language) on top of afunctional meta-language UnCAL (Unstructured Calculus) for describing and manipulating graph data.
The term “unstructured” is used to refer to unstructured or semi-structured data, i.e., data having noassumed format in a database (in contrast to relational database). Recently, the functional programming
community found a new application area of UnCAL in so-called bidirectional transformations on graphdata, because it provides an efficient graph transformation language. The theory and practice of UnCAL
have been extended and refined in various directions (e.g. [18, 19, 17, 1]), which has increased theimportance of UnCAL.
In this paper, we give a more conceptual understanding of UnCAL using semantics of type theory
and fixed points. We give an equational axiomatisation and algebraic semantics of UnCAL graphs. The
main result of this paper is to prove completeness of our equational axioms for UnCAL for the original
bisimulation of UnCAL graphs via iteration algebras. Another benefit of algebraic semantics is a clean
characterisation of the computation mechanism of UnCAL called “structural recursion on graphs” using
free iteration algebra.
UnCAL Overview. We begin by introducing UnCAL. UnCAL deals with graphs in a graph database.
Hence, it is better to start with viewing how concrete semi-structured data is processed in UnCAL.
Consider the semi-structured data sd below which is taken from [8].

Submitted to:
FICS 2015

c M. Hamana
This work is licensed under theCreative Commons Attribution License.

2

Iteration Algebras for UnQL Graphs

It contains information about country, e.g.
geography, people, government, etc.
It is depicted as a tree above,
sd / country:{name:"Luxembourg",
in which edges and leaves are
geography:{coordinates:{long:"49 45N", lat:"6 10E"},
labelled. Using UnCAL’s term
area:{total:2586, land:2586}},
people:{population:425017,
language for describing graphs
ethnicGroup:"Celtic",(and trees), this is defined by
ethnicGroup:"Portuguese",
sd shown at right. Then we canethnicGroup:"Italian"},define functions in UnCAL togovernment:{executive:{chiefOfState:{name:"Jean",..}}}}
process data. For example, afunction that retrieves all ethnic groups in the graph can be defined simply bysfun f1(L:T) = if L = ethnicGroup then (result:T) else f1(T)The keyword sfun denotes a function definition by structural recursion on graphs, which is the computational mechanism of UnCAL. Executing it, we can certainly extract:f1(sd){result:"Celtic", result:"Portuguese", result:"Italian"}&x1...xm
The notation {· · · :· · · , · · · } is a part&x&of the UnCAL’s term language for repy
GG
G G'
resenting graphs. It consists of markers x, labelled edges `: t , vertical comy
()
x G
G
G G'
positions s  t, horizontal compositions
x1...xk
hs , ti, other horizontal compositions
x1... xm
x'1...x'm'
x1...xmG
y1...yms ∪ t merging roots, forming cycles
Gcycle(t), constants { },( ), and definiGG'
y1...ymx1...xm
y1...yntions (x / t). These term constructions
G'y1...yn
y1...ynz1...znhave underlying graph theoretic mean
ing shown at th right. Namely, these(G)
G , G'G G'
are officially defined as operations on
Figure 1: Graph theoretic definitions of constructors [8]the ordinary representations of graphs:
Slightly changed notation. Correspondence between the original and this paper’s:(vertices set, edges set, leaves, roots)- &y = y, @ = , ⊕ = h−, −i, (− := −) = − / −.
tuples (V, E, {y1 , . . . ym }, {x1 , . . . , xn }), but
we do not use the graph theoretic definitions of these operations in this paper.

M. Hamana

3

UnCAL deals with graphs modulo bisimulation (i.e. not only modulo graph isomorphism).
An UnCAL graph is directed and have (possibly multiple) root(s)written & (or multiple x1 · · · xn ) and leaves (written y1 · · · ym ), andwith the roots and leaves drawn pictorially at the top and bottom,
respectively. The symbols x, y1 , y2 , & in the figures and terms arecalled markers, which are the names of nodes in a graph and areused for references for cycles. Also, they are used as port names
to connect two graphs. A dotted line labelled ε is called an ε-edge,
which is a “virtual” edge connecting two nodes directly. This isachieved by identifying graphs by extended bisimulation, which
ignores ε-edges suitably in UnCAL. The UnCAL graph G shownat the left is an example. This is extended bisimilar to a graph that
reduces all ε-edges. Using UnCAL’s language, G is represented
Figure 2: Graph G and bisimilar one as the following term tG
tG = a :({b: x} ∪ {c: x})  cycle(x / d :({p: y1 } ∪ {q: y2 } ∪ {r: x}) ).
UnCAL’s structural recursive function works also on cycle. For example, define another function
sfun f2(L:T) = a:f2(T)that replaces every edge with a. As expected,
f2( tG )a :({a: x} ∪ {a: x})  cycle(x / a :({a: y1 } ∪ {a: y2 } ∪ {a: x}) )where all labels are changed to a.
Another characteristic role of bisimulation is that it identifies expansion of cycles. For example, aterm cycle(& / a: &) corresponds to the graph shown below at the leftmost. It is bisimilar to the rightones, especially the infinitely expanded graph shown at the rightmost, which has no cycle.

These are in term notation:
cycle(& / a: &) ∼ a: cycle(& / a: &) ∼ a: a: cycle(& / a: &)Problems. There have been no algebraic laws that establish the above expansion of cycle. Namely,
these are merely bisimilar, and not a consequence of any algebraic law. But obviously, we expect that itshould be a consequence of the algebraic law of fixed point property of cycle.
In the original and subsequent formulation of UnCAL [8, 17, 18, 1], there are complications of thiskind. The relationship between terms and graphs in UnCAL is not a one-to-one correspondence. No term
notation exits for ε-edges and infinite graphs (generated by the cycle construct), thus the rightmost infinite
graphs of the above expansion cannot be expressed in syntax. But such an infinite graph is allowed asa possible graph in the original formulation of UnCAL. Consequently, instead of terms, one must use
graphs and graph theoretic reasoning with care of bisimulation to reason about UnCAL. Therefore, aproperty in UnCAL could not be established only using induction on terms. That fact sometime makessome proofs about UnCAL quite complicated.

Iteration Algebras for UnQL Graphs

4

Because UnCAL graphs are identified by bisimulation, it is necessary to use a procedure or algorithm
to check the bisimilarity as in the cycle example above. Listing some typical valid equations for thebisimulation can be a shortcut [8, 19], but it was only sound and not complete for bisimulation.
Hence, we give an algebraic and type-theoretic formulation of UnCAL by giving equational axiomsof UnCAL graphs. In this paper, we prove completeness of our proposed axioms using iteration algebra[4]. Thus we have a complete syntactic axiomatisations of the equality on UnQL/UnCAL graphs, as aset of axioms capturing the original bisimulation, without touching graphs, ε-edges, and the notion ofbisimulation explicitly. We prove it by connecting it with the algebraic axiomatisations of bisimulation[3, 12].
How to model UnCAL and structural recursion. The first idea to understand UnCAL is to interpret
it as a categorical structure. We can regard edges as morphisms (of the opposite directions), the verticalcomposition  as the composition of arrows, and cycle as a fixpoint operator in a suitable category.
Thus the target categorical structure should have a notion of fixpoint, which has been studied in iteration
theories of Bloom and Ésik [3]. In particular, iteration categories [10] are suitable, which are traced
cartesian categories [20] (monoidal version is used in Hasegawa’s modelling of cyclic sharing theories[16, 15]) additionally satisfying the commutative identities axiom [3] (see also [25] Section 2 for a useful
overview around this).
We also need to model UnCAL’s computational mechanism: “structural recursion on graphs”. The
general form of the definition of structural recursive function issfun F( ` : t ) = e(F)where e can involve F(t). The graph algorithm in [8] provide a transformation of graphs that producessome computed graphs using the definition (F). It becomes a function F satisfying the equations ([8]Prop. 3):F( yi ) = yi
F( ( ) ) = ( )F( { } ) = { }F( (x / t) ) = (x / F(t))
F( s ∪ t ) = F(s) ∪ F(t)F( hs , ti ) = hF(s) , F(t)i

F( `: t ) = e
F( s  t ) = F(s)  F(t)F( cycle(t) ) = cycle(F(t))· · · (./)
· · · (./)

(1)

when e does not depend1 on t. This is understandable naturally as the example f2 recurses structurally
the term tG . Combining the above categorical viewpoint, F can be understood as a functor that preserves
cycle and products (thus a traced cartesian functor). A categorical semantics of UnCAL can be given
along this idea, which will be reported elsewhere. This idea works for simple cases of structural recursion
such as f2.
However, there is a critical mismatch between the above categorical view and UnCAL’s structural
recursion of more involved cases. Buneman et al. mentioned a condition that the above nine equations
hold only when e does not depend on t in (F). Two equations marked (./) do not hold in general if e does
depend on t (other seven equations do hold). Crucially, f1 is already this case, where T appears as notof the form f1(T). The following another example shows why (./) do not hold: the structural recursivefunction aa? tests whether the argument contains “a:a:”.
sfun a?(L:T) = if L=a then true:{} else {}sfun aa?(L:T) = if L=a then a?(T) else aa?(T)The definition of aa? does depend on T at the “then”-clause. Then we have the inequalities:
1 Here “e depends on t” means that e contains t other than the form F(t).

M. Hamana

5

aa?( (a:&)(a:{})) = aa?( a:a:{} ) = true:{} , {} = {}{} = aa?(a:&)  aa?(a:{})aa?( cycle(a:&) ) = aa?( a:a:cycle(a:&) ) = true:{} , {} = cycle({}) = cycle(aa?(a:&))This means that F does not preserve cycle in general, and even is not functorial, thus the categoricalview seems not helpful to understand this pattern of recursion.
In this paper, we consider algebraic semantics of UnCAL using the notion of iteration Σ-algebras[4, 12] in §3. It solve the problem mentioned above, i.e. we derive the structural recursion even when
the case that e depends on t within the algebraic semantics.
Organisation. This paper is organised as follows. We first give a framework of equational theory for
UnCAL graphs by reformulating UnCAL graph data in a type theoretic manner in Section 2. We thengive algebraic semantics of UnCAL using iteration Σ-algebras in Section 3. We prove completeness of
our axioms for UnCAL graphs for bisimulation in Section 3.3. We further derive structural recursion
on UnCAL graphs in Section 3.5. Finally, in Section 3.6. we show several examples how structural
recursive functions on graphs are modeled.

2 UnCAL and its Equational Theory
We give a framework of equational theory for UnCAL graphs. We reformulate UnCAL graph data in a
type theoretic manner. We do not employ the graph theoretic and operational concepts (such as ε-edges,
bisimulation, and the graph theoretic definitions in Fig. 1). Instead, we give an algebraic axiomatisationof UnCAL graphs following the tradition of categorical type theory [9]. The syntax in this paper isslightly modified from the original presentation [8] to reflect the categorical idea, which may be morereadable for the reader familiar with categorical type theory.

2.1 Syntax
Markers and contexts. We assume an infinite set of symbols called markers, denoted by typicallyx, y, z, . . .. One can understand markers as variables in a type theory. The marker denoted by & is called
the default marker, which is just a default choice of a marker having no special property. Let L be a
set of labels. A label ` is a symbol (e.g. a, b, c, . . . in Fig. 2). A context, denoted by hhx1 , x2 , . . .ii, is asequence of pairwise distinct markers . We typically use X, Y, Z, . . . for contexts. We use hhii for the empty
contexts, X, Y for the concatenation, and |X| for its length. We may use the vector notation ~x for sequencex1 , . . . , xn . The outermost bracket hh ii of a context may be omitted. We may use the abbreviations forthe empty context 0 = hhii. Note that the concatenation may need suitable renaming to satisfy pairwise
distinctness of markers.
Raw terms.
t ::= y Y

|

`: t

|

st

|

hs , ti|cycleX (t)

|

{ }Y

|

( )Y

|

f

|

(x / t)We assume several conventions to simplify the presentation of theory. We often omit subscripts or
superscripts such as Y when they are unimportant or inferable. We identify hhs , ti , ui with hs , ht , uii;
thus we will freely omit parentheses as ht1 , . . . , tn i. A constant f express a branch in a tree, and we callthe symbol f a man, because it is similar to the shape of a kanji or Chinese character meaning a man,
which is originated from the figure of a man having two legs (and the top is a head).

Iteration Algebras for UnQL Graphs

6
(Nil)

Y ` { }Y : &(Emp)

Y ` ( )Y : hhii(Man)y1 , y2 ` fhhy1 ,y2 ii : &(Com)Y `s :ZX `t :YX ` st : Z(Label)`∈L Y `t :&Y ` `: t : &(Mark)

Y = hhy1 , . . . , yn ii
Y ` yi Y : &(Pair)Y ` s : X1
Y ` t : X2
Y ` hs , ti : X1 , X2

(Cyc)

Y, X ` t : X
Y ` cycleX (t) : X(Def)

Y `t :&Y ` (x / t) : x

Figure 3: Typing rules
Abbreviations. We use the following abbreviations.
{s} ∪ {t} , f  hs , ti
π1
, xhhx,yii
π2, yhhx,yii

s×t
idhhxii
idhhx1 ,...,xn ii, hs  π1 , t  π2 i
, xhhxii, x1 hhx1 ii × · · · × xn hhxn ii∆X , hidX , idX i
c , hπ2 , π1 iInheriting the convention of h−, −i, we also identify (s × t) × u with s × (t × u), thus we omit parentheses
as t1 × . . . × tn .

2.2 Typed syntax
For contexts X, Y, we inductively define a judgment relation Y ` t : X of terms by the typing rules in Fig.
3. We call a marker free in t when it occurs in t other than the left hand-side of a definition (x / s). In
a judgment, free markers in t are always taken from Y. Thus Y is a variable context (which we call thesource context) in ordinary type theory, and X is the roots (which we call the target context or type). For
example, the term tG in §1 is well-typed y1 , y2 ` tG : &, which corresponds a graph in Fig. 2, where
the marker &is the name of the root. When t is well-typed by the typing rules, we call t a (well-typed
UnCAL) term. We identify t of type & with (& / t).
Definition 2.1 (Substitution) Let Y = hhy1 · · · , yk ii, W be contexts such that |Y| ≤ |W| and Y can be embedded into W in an order-preserving manner, and Y 0 is the subsequence of W deleting all of Y (NB.
|W| = |Y| + |Y 0 |, Y 0 is possibly empty). Suppose W ` t : X,Z ` si : hhyi ii(1 ≤ i ≤ k). Then a0substitution Z, Y ` t [~y 7→ ~s] : X is inductively defined as follows.
(t1  t2 ) [~y 7→ ~s] , t1  (t2 [~y 7→ ~s])yi [~y 7→ ~s] , si0x [~y 7→ ~s] , x (if x in Y ) ht1 , t2 i [~y 7→ ~s] , h(t1 [~y 7→ ~s]) , (t2 [~y 7→ ~s])i{ }Y [~y 7→ ~s] , { }Z+Y 0
cycle(t) [~y 7→ ~s] , cycle(t [~y 7→ ~s])( )Y [~y 7→ ~s] , ( )Z+Y 0(x / t) [~y 7→ ~s] , (x / t [~y 7→ ~s])(`: t) [~y 7→ ~s] , `: ( t [~y 7→ ~s] )fhhy1 ,y2 ii [y1 7→ s1 , y2 7→ s2 ] , fhhy1 ,y2 ii  (s1 , s2 )Note that t [~y 7→ ~s] denotes a meta-level substitution operation, not an explicit substitution.

2.3 Equational theory
For terms Y ` s : X and Y ` t : X, an (UnCAL) equation is of the form Y ` s = t : X. Hereafter, forsimplicity, we often omit the source X and target Y contexts, and simply write s = t for an equation, buteven such an abbreviated form, we assume that it has implicitly suitable source and target contexts andis of the above judgemental form.

M. Hamana

7

Composition(sub) t  hs1 , · · · , sk , idY 0 i = t [~y 7→ ~s]
Deleting trivial cycle(SP)
hπ1  t , π2  ti = t(c2)
cycle(f) = id
Parameterised fixpoint
Commutative monoid(fix)
cycle(t) = t  hidY , cycle(t)i(unitLf) f  ({ }0 × id) = id
(Bekic̆)
cycle(ht, si) = hπ2 , cycle(s)i (assocf)f  (id × f) = f  (f × id)
hidY , cycle(t  hidY,X , cycle(s)i)i(comf)
fc = f(natY )
cycle(t)  s = cycle(t  (s × idX ))Degenerated bialgebra(natX )
cycle(s  t) = s  cycle(t  (idY × s)) (compa) ∆  f = (f × f)  (id × c × id)  (∆ × ∆)(CI)
cycle(ht  (idX × ρ1 ) , . . . , t  (idX × ρm )i)(degen)f  ∆ = id
= ∆m  cycle(t  (idX × ∆m ))Figure 4: Axioms AxGr for UnCAL graphs
Fig. 4 shows our proposed axioms AxGr to characterise UnCAL graphs. These axioms are chosen
to soundly and completely represent the original bisimulation of graphs by the equality of this logic.
Actually, it is sound: for every axiom s = t, s and t are bisimilar. But completeness is not clear only fromthe axioms. We will show it in §3.
The axiom (sub) is similar to the β-reduction in the λ-calculus, which induces the axioms for cartesian
product (cf. the derived theory below). The cartesian structure provides a canonical commutative
comonoid with comultiplication ∆.
Two terms are paired with a common root by {s} ∪ {t} = f  (s , t). The commutative monoid axioms
states that this pairing {−} ∪ {−} can be parentheses free in nested case. The degenerate bialgebra axioms
state the compatibility between the commutative monoid and comonoid structures. The degenerated
bialgebra is suitable to model directed acyclic graphs (cf. [14] §4.5), where it is stated within a PROP
[21]. The monoid multiplication f expresses a branch in a tree, while the comultiplication ∆ expresses
a sharing. Commutativity expresses that there is no order between the branches of a node, cf. (commu∪)
in the derived theory below, and degeneration expresses that the branches of a node form a set (not asequence), cf. (degen’).
Parameterised fixpoint axioms axiomatise a fixpoint operator. They (minus (CI)) are known as theaxioms for Conway operators of Bloom and Ésik [3], which ensures that all equalities that holds in
cpo semantics do hold. It is also arisen in work independently of Hyland and Hasegawa [15], whoestablished a connection with the notion of traced cartesian categories [20]. There are equalities that
Conway operators do not satisfy, e.g. cycle(t) = cycle(t  t) does not hold only by the Conway axioms. The axiom (CI) fills this gap, which corresponds to the commutative identities of Bloom andÉsik [3]. This form is taken from [25] and adopted to the UnCAL setting, where ∆m , hid& , · · · , id& i,
Y = hhy1 , . . . , ym ii, & ` ∆m : Y, X+Y ` t : &, Y ` ρi : Y such that ρi = hqi1 , . . . , qim i where each qi j is
one of Y ` πi : & for i = 1, . . . , m. The axiom (c2) (and derived (c1) below) have been taken as necessary
ones for completeness for bisimulation used in several axiomatisations, e.g. [23, 5, 12].
The equational logic EL-UnCAL for UnCAL is a logic to deduce formally proved equations, called(UnCAL) theorems. The equational logic is almost the same as ordinary one for algebraic terms. The
inference rule of the logic consists of reflexivity, symmetricity, transitivity, congruence rules for all
constructors, with the following axiom and the substitution rules.
(Ax)(Y ` s = t : X) ∈ E
Y `s=t :X(Sub)

W ` t = t0 : X
Z ` si = s0i : yi (1 ≤ i ≤ k)
Z + Y 0 ` t [~y 7→ ~s] = t0 [~y 7→ ~s0 ] : X

The set of all theorems deduced from the axioms AxGr is called a (UnCAL) theory.

Iteration Algebras for UnQL Graphs

8

Derived theory. The following are formally derivable from the axioms, thus are theorems.
(tmnl) t = ( )Y for all Y ` t : hhii
(fst)
π1  hs , ti = s(snd) π2  hs , ti = t(bmul)( )& × ( )&(unitRf) f  (id × { }0 )(c1)cycle(id)(unR)t  id(unL)
id  t(assoc)(s  t)  u

=
=
=
=
=
=

(dpair)ht1 , t2 i  s= ht1  s, t2  si
(fsi)
hπ1 , π2 i
= id
(SP)
hπ1  t , π2  ti = t( )&  f(bcomul)∆  { }0id(bunit)( )&  { }0
{ }0(comm∪){s} ∪ {t}t(unit∪){{ }} ∪ {t}t(assoc∪) {{s} ∪ {t}} ∪ {u}s  (t  u) (degen’){t} ∪ {t}

=
=
=
=
=
=

({ }0 × { }0 )id{t} ∪ {s}t = {t} ∪ {{ }}{s} ∪ {{t} ∪ {u}}tBecause of the first three lines, UnCAL has the cartesian products. For (c1), the proof iscycle(id) =(unitLf) cycle(f  ({ }0 × id)) =(natY ) cycle(f)  { }0 =(c2) id  { }0 . = { }0 .

3 Algebraic Semantics of UnCALIn this section, we consider algebraic semantics of UnCAL. We also give a complete characterisation of
the structural recursion, where e can depend on t in (F).

3.1 Iteration Σ-Algebras
We first review the notion of iteration Σ-algebras and various characterisation results by Bloom and Ésik.
Let Σ be a signature, i.e. a set of function symbols equipped with arities. We define µ-terms byt ::= x | f (t1 , . . . , tn ) | µx. t,
where x is a variable. We use the convention that a function symbol f (n) ∈ Σ denotes n-ary. For a set Vof variables, we denote by T(V) the set of all µ-terms generated by V. We define ConwayCI as the set offollowing equational axioms:
Conway equationsµx. t[s/x] = t[ µx. s[t/x] /x ],µx. µy. t = µx. t[x/y]Group equations associated with a group Gµx. (t[1 · x/x], . . . , t[n · x/x])1 = µy. (x[y/x], . . . , [y/x])
Note that the fixed point lawµx. t = t[µx. t/x]
is an instance the first axiom of Conway equations by taking s = x. The group equations [11] known as
an alternative form of the commutative identities, are an axiom schema parameterised by a finite group(G, ·) of order n, whose elements are natural numbers from 1 to n. We also note that the µ-notation ishere extended on vectors (t1 , . . . , tn ), and (−)1 denotes the first component of a vector. Given a vectorx = (x1 , . . . , xn ) of distinct variables, the notation i · x = (xi·1 , . . . , xi·n ) is used.

M. Hamana

9

Definition 3.1 ([4]) A pre-iteration Σ-algebra (A, (| − |)A ) consists of an nonempty set A and an interpreV
tation function (| − |)(−)
A : T(V) × A → A satisfyingρ(iii) (| t |)A = (| t0 |)A =⇒ (| µx. t |)A = (| µx. t0 |)A .

(i) (| x |)A = ρ(x) for each x ∈ V
ρ

ρ0

ρ

(ii) (| t[t1 /x1 , · · · , tn /xn ] |)A = (| t |)A with ρ0 (xi ) = (| ti |)A , ρ0 (x) = ρ(x) for x , xi
A pre-iteration Σ-algebra can be seen as a Σ-algebra (A, { fA | f ∈ Σ}) with extra operations (| µx. t |)A
for all t. A pre-iteration Σ-algebra A satisfies an equation s = t over µ-terms, if (| s |)A = (| t |)A . Let E
be a set of equations over µ-terms. An iteration Σ-algebra is a pre-iteration Σ-algebra that satisfies all
equations in ConwayCI. An iteration (Σ, E)-algebra is an iteration Σ-algebra that satisfies all equations
in E. A homomorphism of iteration Σ-algebras h : A → B is a function such that h ◦ (| t |)A = (| t |) ◦ hV
for all t. Since the variety of iteration Σ-algebras is exactly the variety of all continuous Σ-algebras ([4]Introduction), the interpretation of µx. t in an iteration Σ-algebra can be determined through it.
We now regard each label ` ∈ L as an unary function symbol. Then we consider an iteration L ∪(0){0 , +(2) }-algebra. We define the axiom set AxBR bys + (t + u) = (s + t) + uµx. x = 0s+t = t+ s
µx. (x + y) = yt+0 = tfor y not containing x

and AxCBR , ConwayCI ∪ AxBR. We write AxCBR `µ s = t if an equation s = t is derivable fromAxCBR by the standard equational logic EL-µ for µ-terms. For example, idempotency is derivable:
AxCBR `µ t + t = t

The proof is t = µx.(x + t) = (µx.(x + t)) + t = t + t, which uses the last axiom in AxBR and the fixed point
law. Since µ-terms can be regarded as a representation of process terms of regular behavior as Milner
shown in [23] (or synchronization trees [3]), the standard notion of strong bisimulation between twoµ-terms can be defined. We write s ∼ t if they are bisimilar.
Theorem 3.2 ([3, 4, 12, 13])(i) The axiom set AxCBR completely axiomatises the bisimulation, i.e., AxCBR `µ s = t ⇐⇒ s ∼ t(ii) The set T(V) of all µ-terms forms a free pre-iteration Σ-algebra over V.
(iii) The set BR of all regular L-labeled trees having V-leaves modulo bisimulation forms a free iteration (L ∪ {0, +}, AxBR)-algebra over V ([12] below Lemma 2, [24] Thm. 2).
Note that BR stands for Regular trees modulo Bisimulation, and AxBR stands for the axioms for regulartrees modulo bisimulation.

3.2 Characterising UnCAL Normal Forms
UnCAL normal forms. Given an UnCAL term t of type &, we compute the normal form of t by thefollowing three rewrite rules (N.B. we do not here use the other axioms) as a rewrite system [2], which
are oriented equational axioms taken from the derived theory, AxGr and abbreviations.
(sub) t  hs1 , · · · , sk , idi = t [~y 7→ ~s](Bekic̆)
cycle(ht, si) = hπ2 , cycle(s)i  hidA , cycle(t  hidA×V , cycle(s)i)i(union)f  (s , t) = {s} ∪ {t}Iteration Algebras for UnQL Graphs

10

Let M be the set of all rewriting normal forms by the above rules, which finally erases all h− , −i and  ina given t. Normal forms are uniquely determined because the rewrite rules are confluent and terminating,hence have the unique normal form property [2]. Then by induction on terms we have that terms in M
follow the grammar
M 3 t ::= y

|

`: t

|

cycleX (t)

|

{}

|

{s} ∪ {t}|(x / t).

Any outermost definition must be of the form (& / t0 ) by the assumption that the original given t is oftype &, thus we identity it with t0 . Other definitions appear inside of t, as the following cases:• Case {(x1 / t1 )} ∪ {(x2 / t2 )}. We identify it with merely {t1 } ∪ {t2 }, because marker names x1 , x2
are hidden by this construction.
• Case Y ` cycle x (x / t0 ) : x. We identify it with merely cycle& (t0 ), because these are equivalent byrenaming of free maker x.
The UnCAL normal forms N are obtained from M by these identifications. It is of the form
N 3
T(V) 3

t ::=
t ::=

y
y

|
|

`: t
`(t)

|
|

cycleX (t)µx1 . . . . µxn .t

|
|

{}
0

|
|

{s} ∪ {t}s+tEvery normal form bijectively corresponds to a µ-term in T(V), i.e. N  T(V), because each the above
construct corresponds to the lower one, where X = hhx1 , . . . , xn ii. Hereafter, we may identify normal forms
and µ-terms as above. Define the pair of signature and axioms by
UnC , (L ∪ {0, +}, AxBR).

We regard an arbitrary UnC-algebra A as an algebraic model of UnCAL graphs. First, we show theexistence of a free model. Define NCBR to be the quotient of N by the congruence generated by AxCBR.
Proposition 3.3
NCBR forms a free iteration UnC-algebra over V. Thus for any function
ψ : V → A, there exists an unique UnC-algebra homomorphism ψ] such thatthe right diagram commutes, where η is an embedding of variables.

V

η-

NCBR

Q
Q
Q
ψ Qs
Q

ψ]

?

A

Proposition 3.4 NCBR  BR.
Proof. By Theorem 3.2 (iii).



3.3 Completeness of the Axioms for Bisimulation
Buneman et al. formulated that UnCAL graphs were identified by extended bisimulation, which is abisimulation on graphs involving ε-edges. As discussed in §1, since our approach is to use only UnCAL
terms, it suffices to consider only the standard (strong) bisimulation between UnCAL terms, as done in[23, 3, 12, 13]. We denote by ∼ bisimulation for UnCAL term.
In this subsection, we show the completeness of AxGr for bisimulation, using the following Lemma
3.5 that reduces the problem of EL-UnCAL to that of EL-µ through UnCAL normal forms. AxCBR has
been shown to be complete for the bisimulation [3].
Lemma 3.5 For UnCAL normal forms n, m ∈ N , AxCBR `µ n = m ⇐⇒ Y ` n = m : X is derivable from
AxGr in EL-UnCAL.

M. Hamana

11

Proof. [⇒] : By induction on proofs of EL-µ. For every axiom in AxCBR, there exists the corresponding
axiom in AxGr or an EL-UnCAL theorem, hence it can be emulated.
[⇐] : By induction on proofs of EL-UnCAL. Let s = t is an axiom of EL-UnCAL. It easy to see that taking
normal forms of both side, they are equal term, or correspond to an axiom in AxCBR or EL-µ theorem.

Theorem 3.6 (Completeness) AxGr is sound and complete for the bisimulation, i.e.,Y ` s = t : X is derivable from AxGr in EL-UnCAL iff s ∼ t.
Proof. [⇒] : Because every axiom in AxGr is bisimilar, and the bisimulation is closed under contexts
and substitutions [8].
[⇐] : Suppose s ∼ t. Since for each rewrite rule for the normalisation function nf, both sides of the rule isbisimilar, nf preserves the bisimilarity. So we have s ∼ nf(s) ∼ nf(t) ∼ t. Since AxCBR is complete axiomsof bisimulation [3, 12], AxCBR `µ nf(s) = nf(t). By Lemma 3.5, we have a theorem Y ` nf(s) = nf(t) : X.
Thus s = t is derivable.


3.4 Interpretation in Algebraic Models
To interpret UnCAL terms and equations, we connect two freeness results in Thm.
3.2.
Since UnCAL normal forms N is isomorphic to a free pre-iteration algebra T(V), it has theuniversal property.
Define T& to be the set of all well-typed UnCAL terms of type &.
T&
We define nf : T& → N by the function to compute the UnCAL normal formof a term. Then for any derivable equation Y ` s = t : X in EL-UnCAL, wenfhave AxCBR ` nf(s) = nf(t) by Lemma 3.5, thus for all assignment ψ : V →?
0ηA,
T(V)  NVQψ] (| nf(s) |)η = ψ] (| nf(t) |)η
S Q η(| − |)η
S QQ
0where η and η are embedding of variables.
S
Q ?
s
S
NCBR  BR
Since NCBR  BR, we name the isomorphisms (−) : NCBR → BR andψSS(−) : BR → NCBR . We write simply a normal form t to denote a represenψ]S
tative [t] in NCBR . Thus given a normal form t (which is a syntactic term,
S ?
w
A
always finite), t is a (possibly infinite) regular tree by obtained by expanding cycles in t using fixpoints. Conversely, notice that since t is a tree, there are no cycles and the original
cycles in t are infinitely expanded. Since N  T(V), the functions (−) may also be applied to µ-terms.
The iteration UnC-algebra BR has operations 0BR = { }, +BR (r, s) = { r } ∪ { s }, `BR (r) = `(r).

3.5 Deriving structural recursion of involved case
Next we model UnCAL’s structural recursion of graphs. We use pairs of “the recursive computation” andthe history of data structure. This is similar to the technique of paramorphism [22], which is a way torepresent primitive recursion in terms of “fold” in functional programming. Our universal characterisation of graphs is the key to make this possible by the unique homomorphism from the free pre-iteration
UnC-algebra N using the above analysis.
We take a term X ` e` (v, r) : X involving metavariables v and r, where e` (F(t), t) is the right-handside e of F(`: t) in (F) . For example, in case of the example f1 in Introduction (see also Example 3.9),
we takee` (v, r) , result: r,e` (F(t), t) = result: t
if ` = ethnicGroupe` (v, r) , v,e` (F(t), t) = F(t)if ` , ethnicGroup

Iteration Algebras for UnQL Graphs

12

We construct a specific iteration UnC-algebra BRe for {e` (v, r)}`∈L . Let k , |X|. Without loss ofgenerality, we can assume that e` (v, r) is of the form ht1 , · · · , tk i where every ti is a normal form. We
define the iteration UnC-algebra BRe = BRk × BR having operation`BRe (v, r) = ( e` (v, r), `: r ),0BRe = ({~}, { })~ is the k-tuple of {}. Hereafter, we willand +BRe is an obvious tuple extensions of +BR . Here {}use this convention ~o of tuple extension of an operator o.
00
Then, two freeness results in Thm. 3.2 are depicted in the right diagram,
ηV
T(V)  N
where η(x) = ( x1 , · · · , xk , x ). Since T(V)  N, the interpretation in BRe is
Q
0
S Q η
η0
described as(| − |)S Qηηη(| x |)BRe = η(x), (| { } |)BRe = 0BRe , (| {s} ∪ {t} |)BRe = (| s |)BRe +BRe (| t |)BReηηη(| `: t |)BRe = `BRe ((| t |)BRe ), (| cycle(t) |)BRe = η] (cycle(t))η

Now (| − |)BRe is characterised as the unique pre-iteration L ∪ {0, +}-algebra
homomorphism from T(V) that extends η. Definingη

φ , π1 ◦ (| − |)BRe : N

S Qs
Q ?
S
BR
ηS
S
η]
S
S ?
w

BR

BRe

π1

?

- BRk  N k

CBR ,

k
BRk  NCBR

it is the unique function satisfying
φ(x) = (x1 , . . . , xk ),φ(`: t) = e` (v, t),φ({ }) = {~},

φ({s} ∪ {t}) = φ(s) ~∪ φ(t),φ(cycle(t)) = π1 ◦ η] (cycle(t))

The function φ takes normal forms of the type &. For non-normal forms, just precompose nf, i.e., definekthe function Φ : T& → NCBR
by Φ(s) , φ(nf(s)), thus, Φ|X| : TX → NCBR k|X| → TXk , because TX  T&|X| . In
summary, we have the following, where s is a possibly non-normal formΦ(s)= φ( nf(s) )|X|+|Y|~ Φ|Y| (t2 )Φ(ht1 , t2 i) = Φ|X| (t1 ) ×Φ0 (( ))= ()φ(x)= hx1 , · · · , xk iφ(`: t)= e` (φ(t), t)φ(cycle(t)) = π1 ◦ η] (cycle(t))φ({ }) = {~}φ(t1 ∪ t2 ) = φ(t1 ) ~∪ φ(t2 )(2)~ is the “zip” operator of two tuples. Here we use a map NCBR → Tm(V) to regard a normal form
where ×modulo AxCBR as a term, for which any choise of representative is harmless, because UnCAL graphs
are identified by bisimulation and AxCBR axiomatises it. Identifying three kinds functions Φ, Φ|X| , φ asa single function (also denoted by Φ, by abuse of notion) on Tm(V), this Φ is essentially what Buneman
et al. [8] called the structural recursion on graphs for the case that e depends on t. Actually, we could
make the characterisation more precise than [8], i.e., we obtain also the laws for the cases of  (by thecase Φ(s) = φ(nf(s))) and cycle, which tells how to compute them.
This is not merely rephrasing the known result, but also a stronger characterisation, which gives
precise understanding of the structural recursion on graphs:(i) Buneman et al. stated that (1) without (./) is a property ([8] Prop. 3) of a “structural recursivefunction on graphs” defined by the algorithms in [8]. This property (i.e. soundness) is desirable,
but unfortunately, no completeness was given. There may be many functions that satisfy the property. In contrast to it, our characterisation is sound and complete: (2) determines a unique function
by the universality.

M. Hamana

13(ii) This derivation does not entail Φ(s  t) = Φ(s)  Φ(t). It tells us that the only way to compute Φ(s  t)
is to compute the normal form of s  t and then apply φ.
(iii) This analysis does not entail Φ(cycle(t)) = cycle(Φ(t)) either. The iteration algebra structure tells
us that the homomorphism φ maps a term cycle(t) to its interpretation in BRe where the cycles
are expanded in a regular tree and at the same time, labels ` are interpreted using the operations ofBRe.
(iv) The structure preserved by structural recursion is the (pre-)iteration algebra structure. The structural recursive function φ is the composition of a pre-iteration algebra homomorphism, an a iteration algebra homomorphism and a projection.

3.6 Examples
We may use the notation {t1 , t2 , . . .} as the abbreviation of {t1 } ∪ {t2 } ∪ · · · .
Example 3.7 ([8] Replace all labels with a) This is the example considered in Introduction.
sfun f2(L:T) = a:f2(T)In this case, the recursion does not depend on T (because the right-hand side uses merely f2(T)). We
define the iteration UnC-algebra BRe by`BRe (v, r) = (a: v, `: r).
(We may omit over and underlines to denote the isomorphisms for simplicity). Then Φ is the desired
structural recursive function f2. E.g.
Φ(b: cycle(c: &)) = a: φ(cycle(c: &)) = a: π1 ◦ η] (c: c: · · · ) = a: (a: a: · · ·) = a: cycle(a: &)Example 3.8 ([8] Double the children of each node)
sfun f4(L:T) = {a:f4(T)}∪{b:f4(T)}

Example of execution.
f4(a:b:c:{}){a:{ a:{a:{}, b:{}}, b:{a:{}, b:{}} }} ∪ {b:{ a:{a:{}, b:{}}, b:{a:{}, b:{}} }}This case does not depend on T. We define the iteration UnC-algebra BRe by`BRe (v, r) = ({a: v} ∪ {b: v}, `: r).
Then Φ gives the structural recursive function defined by f4.
Example 3.9 ([8] Retrieve all ethnic groups) We revisit the example given in §1.
For the structural recursive recursive definition of f1,
sfun f1(L:T) = if L = ethnicGroup then (result:T) else f1(T)This case does depend on T. Example of execution:
f1(sd){result:"Celtic":{}, result:"Portuguese":{}, result:"Italian":{}}

Iteration Algebras for UnQL Graphs

14
We define the iteration UnC-algebra BRe by

ethnicGroupBRe (v, r) , (result: r, ethnicGroup: r)`BRe (v, r) , (v, `: r) for ` , ethnicGroup
Then Φ is the structural recursive function defined by f1:
Φ (sd) = {result:"Celtic":{}, result:"Portuguese":{}, result:"Italian":{}}

Example 3.10 Consider another example in §1 of aa?. This case does depend on T. We define theiteration UnC-algebra BRe by
aBRe (v, r) , (a?(r), a: r)`BRe (v, r) , (v, `: r) for ` , a.
Then Φ gives the structural function aa?
Φ((a:&)@(a:{})) = φ( nf((a:&)@(a:{})) ) = φ(a:a:{}) = true:{}Φ(cycle(a:&)) = π1 ◦ η] (cycle(a:&)) = π1 ◦ η] (a:a: · · ·) = π1 (a?(a: · · ·), a: · · ·) = true : { }4 Conclusion
In this paper, we have shown an application of Bloom and Ésik’s iteration algebras to model graph data
used in UnQL/UnCAL for describing and manipulating graphs. We have formulated UnCAL and given
an axiomatisation of UnCAL graphs that characterises the original bisimulation. We have given algebraic
semantics using Bloom and Ésik’s iteration iteration algebras. The main result of this paper was to showthat completeness of our equational axioms for UnCAL for the original bisimulation of UnCAL graphs
via iteration algebras. As a consequence, we have given a clean characterisation of the computation
mechanism of UnCAL, called “structural recursion on graphs” using free iteration algebra.
Acknowledgments. I am grateful to Kazutaka Matsuda and Kazuyuki Asada for discussions about
UnCAL and its interpretation, and their helpful comments on a draft of the paper. A part of this work
was done while I was visiting National Institute of Informatics (NII) during 2013 – 2014.

References[1] K. Asada, S. Hidaka, H. Kato, Z. Hu & K. Nakano (2013): A parameterized graph transformation calculus
for finite graphs with monadic branches. In: Proc. of PPDP ’13, pp. 73–84, doi:10.1145/2505879.2505903.
[2] F. Baader & T. Nipkow (1998): Term Rewriting and All That. Cambridge University Press.
[3] S. L. Bloom & Z. Ésik (1993): Iteration Theories - The Equational Logic of Iterative Processes. EATCS
Monographs on Theoretical Computer Science, Springer.
[4] S. L. Bloom & Z. Ésik (1994): Solving Polynomial Fixed Point Equations. In: Proc. of MFCS’94, LNCS
841, pp. 52–67, doi:10.1007/3-540-58338-6 58.
[5] S. L. Bloom, Z. Ésik & D. Taubner (1993): Iteration Theories of Synchronization Trees. Inf. Comput. 102(1),pp. 1–55, doi:10.1006/inco.1993.1001.
[6] P. Buneman, S. Davidson, G. Hillebrand & D. Suciu (1996): A query language and optimization techniques
for unstructured data . In: Proc. of ACM-SIGMOD’96, doi:10.1145/233269.233368.

M. Hamana

15[7] P. Buneman, S. B. Davidson, M. F. Fernandez & D. Suciu (1997): Adding Structure to Unstructured Data.
In: Proc. of ICDT ’97, pp. 336–350, doi:10.1007/3-540-62222-5 55.
[8] P. Buneman, M. F. Fernandez & D. Suciu (2000): UnQL: A Query Language and Algebra for Semistructured
Data Based on Structural Recursion. VLDB J. 9(1), pp. 76–110, doi:10.1007/s007780050084.
[9] R.L. Crole (1993): Categories for Types. Cambridge Mathematical Textbook.
[10] Z. Ésik (1999): Axiomatizing Iteration Categories. Acta Cybernetica 14, pp. 65–82.
[11] Z. Ésik (1999): Group Axioms for Iteration. Inf. Comput. 148(2), pp. 131–180, doi:10.1006/inco.1998.2746.
[12] Z. Ésik (2000): Axiomatizing the Least Fixed Point Operation and Binary Supremum. In: Proc. of Computer
Science Logic 2000, LNCS 1862, pp. 302–316, doi:10.1007/3-540-44622-2 20.
[13] Z. Ésik (2002): Continuous Additive Algebras and Injective Simulations of Synchronization Trees. J. Log.
Comput. 12(2), pp. 271–300, doi:10.1093/logcom/12.2.271.
[14] M. P. Fiore & M. D. Campos (2013): The Algebra of Directed Acyclic Graphs. In: Computation, Logic,
Games, and Quantum Foundations, LNCS 7860, pp. 37–51, doi:10.1007/978-3-642-38164-5 4.
[15] M. Hasegawa (1997): Models of Sharing Graphs: A Categorical Semantics of let and letrec. Ph.D. thesis,
University of Edinburgh. Distinguished Dissertation Series, Springer-Verlag, 1999.
[16] M. Hasegawa (1997): Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic
Lambda Calculi. In: Proc. of TLCA’97, pp. 196–213, doi:10.1007/3-540-62688-3 37.
[17] S. Hidaka, K. Asada, Z. Hu, H. Kato & K. Nakano (2013): Structural recursion for querying ordered graphs.
In: Proc. of ACM SIGPLAN ICFP’13, pp. 305–318, doi:10.1145/2500365.2500608.
[18] S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda & K. Nakano (2010): Bidirectionalizing graph transformations. In: Proc. of ICFP 2010, pp. 205–216, doi:10.1145/1863543.1863573.
[19] S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, K. Nakano & I. Sasano (2011): MarkerDirected Optimization of UnCAL Graph Transformations. In: Proc. of LOPSTR’11, pp. 123–138,
doi:10.1007/978-3-642-32211-2 9.
[20] A. Joyal, R. Street & D. Verity (1996): Traced monoidal categories. Mathematical Proceedings of theCambridge Philosophical Society 119(3), pp. 447–468, doi:10.1017/S0305004100074338.
[21] S. Mac Lane (1971): Categories for the Working Mathematician. Graduate Texts in Mathematics 5, SpringerVerlag, doi:10.1007/978-1-4612-9839-7.
[22] L. G. L. T. Meertens (1992): Paramorphisms.
Formal Asp. Comput. 4(5), pp. 413–424,
doi:10.1007/BF01211391.
[23] R. Milner (1984): A Complete Inference System for a Class of Regular Behaviours. J. Comput. Syst. Sci.
28(3), pp. 439–466, doi:10.1016/0022-0000(84)90023-0.
[24] P. M. Sewell (1995): The Algebra of Finite State Processes. Ph.D. thesis, University of Edinburgh. Dept. ofComputer Science technical report CST-118-95, also published as LFCS-95-328.
[25] A. K. Simpson & G. D. Plotkin (2000): Complete Axioms for Categorical Fixed-Point Operators. In: Proc.
of LICS’00, pp. 30–41, doi:10.1109/LICS.2000.855753.