Structural Recursion for Querying Ordered Graphs
Soichiro Hidaka
Zhenjiang Hu

Kazuyuki Asada ∗Hiroyuki Kato

National Institute of Informatics, Japan{hidaka,asada,hu,kato}@nii.ac.jp

Abstract
Structural recursion, in the form of, for example, folds on lists
and catamorphisms on algebraic data structures including trees,plays an important role in functional programming, by providinga systematic way for constructing and manipulating functional programs. It is, however, a challenge to define structural recursions forgraph data structures, the most ubiquitous sort of data in computing. This is because unlike lists and trees, graphs are essentially not
inductive and cannot be formalized as an initial algebra in general.
In this paper, we borrow from the database community the ideaof structural recursion on how to restrict recursions on infinite unordered regular trees so that they preserve the finiteness property
and become terminating, which are desirable properties for querylanguages. We propose a new graph transformation language called
λFG for transforming and querying ordered graphs, based on thewell-defined bisimulation relation on ordered graphs with special
ε-edges. The language λFG is a higher order graph transformation
language that extends the simply typed lambda calculus with graphconstructors and more powerful structural recursions, which is extended for transformations on the sibling dimension. It not only
gives a general framework for manipulating graphs and reasoning
about them, but also provides a solution to the open problem of how
to define a structural recursion on ordered graphs, with the help of
the bisimilarity for ordered graphs with ε-edges.
Categories and Subject Descriptors CR-number [subcategory]: third-level; D.3.2 [Programming Languages]: Language
Classifications—Specialized application languages; E.1 [Data
Structures]: Graphs and networks
Keywords Structural Recursion, Ordered Graphs, Graph Query
Language, Bisimulation, Optimization

1.

Introduction

Structural recursion, in the form of, for example, folds on lists andcatamorphisms (Meijer et al. 1991) on algebraic data structures including trees, plays an important role in functional programming,by providing a systematic way for construction and manipulation∗ Current affiliation is The University of Tokyo.

Permission to make digital or hard copies of part or all of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. Copyrights for third-party components of this work must be honored.
For all other uses, contact the owner/author(s).
ICFP ’13, September 25–27, 2013, Boston, MA, USA.
Copyright is held by the owner/author(s).
ACM 978-1-4503-2326-0/13/09.
http://dx.doi.org/10.1145/2500365.2500608

Keisuke Nakano
University of Electro-Communications, Japan
ksk@cs.uec.ac.jp

of functional programs (Bird and de Moor 1996; Gill et al. 1993;
Hu et al. 2006). It is, however, a challenge to define structural recursions for graph data structures, the most ubiquitous sort of datain computing. This is because, unlike lists and trees, graphs are
essentially not inductive and cannot be formalized as an initial algebra (Gibbons 1995). Many attempts have been made to resolve
this problem by using special trees to represent graphs so that structural recursion on trees can be used to manipulate graphs. This includes the work on representing graphs by trees with specific pointers (Hamana 2009; Dal Zilio et al. 2004; Oliveira and Cook 2012)and by trees with embedded functions (Fegaras and Sheard 1996).
However, these attempts have not been so successful, because of thegap between trees (with specific pointers/embedded functions) andgraphs, and they require programmers to bridge the gap by explicitly programming these specific pointers and embedded functions.
Would it be possible to define a structural recursion on graphs
as if the graphs were trees (special graphs), while using it to manipulate general graphs? Yes, this has been proved to be possible
to some extent in the database community, where UnCAL (and its
user-level surface syntax UnQL) (Buneman et al. 2000) was introduced to provide a powerful querying method through structural
recursion on finite graphs. The graph model of UnCAL is an unordered graph (whose outgoing edges are not ordered), which canbe treated as (unordered) regular trees (Ginali 1979) given a suitable definition of bisimulation. The benefit of bisimulation is thatstructural recursion on regular trees can be used for graphs, andmoreover, it leads to an interesting and important feature of structural recursion on graphs: bulk semantics. With bulk semantics, a
structural recursion can be evaluated by first processing all edges of
the input graph in parallel and then combining the results. Bulk semantics relies on the use of ε-edges (like ε transitions in the labeledtransition system) in graphs and provides a smart way of treating
shared nodes and cycles in graphs.
Despite usefulness of structural recursion in querying unorderedgraphs, there are two major limitations with UnCAL. One is that
UnCAL can treat only unordered graphs; it cannot treat other graphmodels, such as the widely used ordered graphs in which the outgoing edges of a node are ordered, e.g., in EMF Ecore, MOF, andKM3 (Jouault and Bézivin 2006). Another limitation is the lack of
expressive power of transformations in the sibling dimension. For
example, when the edges of input graphs are labeled with natural
numbers, we cannot write a transformation in UnCAL that extracts
all edges labeled with the average number on the labels of all siblings.
At first sight, it seems that the first limitation could be easily
overcome by encoding ordered graphs as unordered ones withsuitable edge labels, say by using hd and tl to represent the firstbranch and the rest of the branches, respectively. However, there
is a fatal problem with this hd -tl encoding. It is unsound in thecontext of UnCAL where ε-edges must be taken into account for
the graph construction and structural recursion. Figure 1 shows

G1

G2

a

1

b

2

G3

1

1

䡚

2

3

4

5

a

3

b

a

We propose λFG , a powerful higher-order graph transformation
language, which is an extension of the simply typed lambda calculus with graph constructors and a more powerful structural recursion for manipulating ordered graphs than what is available in
UnCAL. The main contributions of this paper can be summarized
as follows.

2

䋏

䋏

• We propose a novel definition of bisimilarity between ordered

G’1

G’2
1

hd
4

a
6

tl 2 tl 3
hd
5
䡚
㻛
b
7

1

hd

tl 2 tl 3
hd
54

tl 7 8 tl 9
hd hd
6

10

11

a

b

12

13

Figure 1. Examples of Head-tail Encoding and Its Unsoundness

an encoding example, where the numbers on the nodes have noparticular meaning, since we consider bisimulation. As shown in
Figure 1, the ordered graphs G1 and G2 , where we use dottedarrows to represent ε-edges, are naturally bisimilar (denoted by ∼in the figure), but the corresponding encoded graphs G01 and G02(7→ in the figure denotes the encoding) are not bisimilar at all.
One might think that we could do the encoding after deleting
ε-edges. However, as the graph G3 in Figure 1 shows, ε-edge elimination of some ordered graphs could produce infinite width graphs,
and this infinite-width problem is not trivial to solve (see Section 3).
Even if we could come up with an encoding, we would still haveto show consistency and soundness of the encoding and the corresponding decoding and provide a suitable notion of bisimilarity forordered graphs having ε-edges, which is very subtle as well (seeSection 3). Moreover, we would need an effective way to guarantee that UnCAL transformations map well-encoded graphs to wellencoded graphs that can be successfully decoded later. All thesesuggest it would be better to design a new language that treats ordered graph directly.
In fact, it has been an open problem for more than ten years as
to whether the definition of structural recursion in UnCAL can be
modified so that it treats ordered graphs rather than unordered ones
(the issue was first raised in the conclusion of the paper (Buneman
et al. 2000)):

graphs having ε-edges, forming the semantic foundation for
λFG . Specifically, we show that the branch order is not necessarily finite but of countable linear order, even for finite graphs,
and clarify that the combination of ε-edges and cycles inducessuch a countable linear order on the branchings, which would
cause issues that do not occur in the unordered case. We showthat we can decide whether an ordered graph is empty andwhether we can eliminate all ε-edges for a finite ordered graphin such a way that the finite width property of the graph is kept.
• We show that graph constructors and structural recursion onunordered graphs can be adapted to those of ordered ones,
forming the core syntax of λFG . Specifically, we define a more
powerful structural recursion on ordered graphs, which can
describe various graph queries including those on the sibling
dimension. We also prove that (1) any graph query in λFG isbisimulation generic in the sense that it returns bisimilar results
for bisimilar inputs, and (2) any graph query in λFG terminates,transforming node-finite graphs to node-finite graphs.
Unlike UnCAL, we also define bisimilarity for higher orderfunctions and prove bisimulation genericity of our structural
recursion as a higher order function; this is the key to extending
our language to a simply typed lambda calculus, and it makes
it clear how we can extend it to rich type systems such as
polymorphic/dependent type systems. Moreover, our proof ofbisimulation genericity is clearer than the original proof givenin (Buneman et al. 2000); this should make further extensionsof structural recursion for graphs easier.
• We have implemented an interpreter for λFG that is available

at http://www.biglab.org/src/lambdaFG/, andwe have tested all the examples in this paper. In addition, we
demonstrate (but have not implemented) that structural recursions are suitable for query reasoning and query optimizationsuch as fusion and tupling transformations. This shows that
our embedding of structural recursions into lambda calculus
would be a good foundation to overcome the known impedancemismatch problem that is often raised from a gap between two
languages when a query language is used in a general-purpose
one for developing a practical application.

... there are some important and interesting areas of research that may well bear fruit. In connection with XML,
we have shown how the principles of UnQL will work on
an ordered tree. However, it is not clear how they can beextended to an ordered graph model. ... we still lack a complete picture of this topic ...

Note that in this paper, the “ordered” in “ordered graph” refers
to the order on the branchings (rather than, say, the order on thenodes), and “graphs” generally refers to “ordered graphs” that canhave ε-edges.

In this paper, we provide a solution to this problem; i.e., we
define a new structural recursion for ordered graphs. For this, wedefine the subtle notion of bisimilarity for ordered graphs having εedges, and prove bisimulation genericity (well-definedness with respect to bisimilarity) of our structural recursion. Note that our (andref. (Buneman et al. 2000)’s) notion of bisimilarity is different fromthat of weak bisimilarity used in process algebra. Weak bisimilarity
does not fit our purpose, because, for example, the graph union operator (works like the list append in the case of ordered lists) would
not be associative.

Organization of the Paper We shall start with an overview of
λFG , a new graph transformation language for querying orderedgraphs in Section 2. In Section 3, we discuss the first key technicalcontribution of this paper, defining ordered graphs, bisimilarity forordered graphs having ε-edges, and ε-elimination. In Section 4, wegive the semantics of our structural recursion and λFG and prove
its bisimulation genericity. We demonstrate how to reason aboutgraph transformations and discuss the expressive power of λFG
in Section 5. Finally, we discuss related work in Section 6 andconclude the paper in Section 7.

(a) A
Graph: G

Simple(b) An EquivalentGraph: G0(c) Result of a2d xc on(a)Figure 2. Examples of Graphs

σ ::= σ → σ | σ + σ | σ × σ{ function, coproduct, product types }| List(σ) | Bool
{ list and boolean types }| Label | GX
{ label and graph types }Ye ::= x | λx.e | e e | case e of inl (x) → e or inr (y) → e| inl e | inr e | (e, e) | prl e | prr e { terms of lambda calculus }| nil | cons(e, e) | foldr(e, e) | ...
{ functions for lists }| if e then e else e{ conditional }| a|e=e{ labels (a ∈ L) and label equality }| [] | e ++ e | [e : e] | [&y] | &x := e | () | e ⊕ e| e @ e | cycle(e){ graph constructors }| isEmpty(e){ graph emptiness checking }| srec(e, e){ structural recursion functions }Figure 3. λFG Language

2.

Overview of λFG

We start with an overview of our transformation language λFG fortransforming (querying) ordered graphs. We introduce our graphmodel to which closed terms of graph types in λFG are interpreted.
Then we present the syntax and typing rules of λFG and explain
how to represent graphs and write transformations for graphs in
λFG .

graphs. When we say just “finite”, it always means finiteness on theset of nodes. We allow a graph to have multiple roots, as a multirooted graph is to a forest what a single-rooted graph is to a tree. For
single-rooted graphs, we often use the default marker & to indicate{&}
the root and use GY to denote GY .

2.1

2.1.1

Ordered Graphs

Graphs treated in λFG are multi-rooted, directed, and edge-labeled.
The graph model in λFG has three prominent features: ε-edges,
markers, and graph concatenation. An ε-edge represents a shortcut between the two nodes and behaves like the ε-transition in
automata. Nodes may be marked with input and output markers.
These markers are used as an interface to other graphs throughε-edges. Graph concatenation sequentially aligns two graphs in agiven order.
Formally, we define an ordered graph as follows. We write L
for a set of labels and Lε for L ∪ {ε}. Let X and Y be finite setsof input and output markers, respectively; we add the prefix & formarkers like &x . Accordingly, an ordered graph G (or just graph)is defined by a triple (V, B, I), where• V is a set of nodes,• B : V → List(Lε ×V +Y ) is a branch function mapping anode to a list of branches: a branch in Lε ×V +Y is either alabeled edge Edge(l, v) or an output marker Outm(&y), and• I : X → V is a function which determines the input nodes (alsocalled roots) of the graph.
Note that in the terminology of coalgebra theory, an orderedgraph is a coalgebra (V, B) of the endofunctor List(Lε ×(-)+Y )equipped with a number |X| of initial states I.
Example 1 (Ordered Graph). The ordered graph in Figure 2(a),where the branches are ordered for each node, is represented as(V, B, I), where
V
B

=
=

I(&)

=

{1, 2, 3, 4}{1 7→ [Edge(d, 2), Edge(a, 4)], 2 7→ [Edge(c, 3)],
3 7→ [Edge(d, 2)], 4 7→ [Edge(b, 3), Outm(&y)]}1.

In our graph model, every node in the range of function I iscalled a root. In Example 1, node 1 is the root node. Even though it
is called a “root”, it may have incoming edges. However, we canconvert any graph having such edges incoming to the root into
graphs bisimilar to the original one but having no such incomingedges.
We shall write GYX for the set of ordered graphs with the input
marker set X and the output marker set Y . We say that a graph isfinite if V is a finite set and write Gf X
Y for the set of finite ordered

Graph Equivalence

λFG uses bisimilarity (also called value-equivalence) as the graphequivalence for ordered graphs. For instance, the graphs G and
G0 in Figures 2(a) and 2(b) are equivalent. In G0 , nodes 3 and
30 are bisimilar because both nodes only have one outgoing edge
labeled d to node 2. Also in G0 , there is an ε-edge (denoted by
the dotted line) from node 1 to node 3, which can be eliminatedwhile maintaining bisimilarity by replacing the ε-edge with an
outgoing edge labeled d from node 1 to node 2. The parts that are
unreachable from the roots are disregarded. The formal definitionof bisimilarity for ordered graphs having ε-edges, which is one of
the important results in this paper, is described in Section 3.
Note that the notion of equivalence based on bisimilarity influences the expressiveness of our query language. For example, since
we do not distinguish bisimilar graphs like in Figures 2(a) and 2(b)—they have different numbers of nodes—, we cannot count the
number of nodes of a graph.
2.2 Syntax of λFG
The syntax of λFG is given in Figure 3, and its typing rules are
given in Figure 4, though we have omitted some standard typing
rules. From here onwards, we will explain the syntax, but will omit
the standard explanations for lambda terms and conditionals. We
will explain graph constructors and structural recursion in detailin Sections 2.2.1 and 2.2.2 and give their formal semantics in
Sections 3.4 and 4. We use the underlined syntax to distinguishcertain graph constructors from ordinary list constructors.
List(σ) is the usual list type whose elements belong to σ; nil,cons(e, e), and foldr(e, e) are standard list functions, and we can
add any convenient list functions. These are used for specifying d
in srec(e, d).
Note that we do not include the label ε in the syntax; ε-edges
are only used in the semantics. Equality only applies to labels.
We have prepared a set of markers Marker ; the metavariables
X, Y , and so on denote finite subsets of Marker . Note that weassume type annotations for bound variables, graph constructors,
and structural recursions: e.g., λxσ .e, []Y , and srecX,Y,Z (e, d);but we will omit them in this presentation for simplicity. We havea type inference procedure to omit marker set annotations in a way
similar to our previous work for UnCAL (Hidaka et al. 2012).
The set of markers α in the type of d is an “abstract” set ofmarkers, which can be viewed as being similar to a type variable in` e1 : Label ` e2 : Labele1 = e2 : Bool(a ∈ L)` a: Label` [] : GY` e 1 : GX
Y
` e 2 : GX
Y
` e1 ++ e2 : GX
Y

` e1 : Label` e2 : GY` [e1 : e2 ] : GY

` e: GY(&y ∈ Y )` [&y]: GY{&x}` (): G∅Y

` &x := e: GY` e 1 : GX
Y
` e2 : GYZ` e1 @ e2 : GX
Z

1
2
` e1 : GX` e2 : GXYY(X1 ∩ X2 = ∅)1 ∪X2
` e1 ⊕ e2 : GX
Y

` e: GX(X ∩ Y = ∅)X∪Y
` cycle(e): GX
Y` e: GXY` isEmpty(e): Bool

` e: Label×GY → GZ
Z
Z
Z
` d: List(GZ
Z×α +GZ×Y ) → GZ×α+Z×Y
Z×X` srec(e, d): GX
Y → GZ×Y

2.2.2(Note that we have omitted the typing environments Γ in each rule.)
Figure 4. Typing Rules for Graph-Related Expressions in λFG&x1 ... &xm

a
G1
[]

G

G2

[a : G]

G1 ++ G2

&x
&y
[&y]

G
&x := G

input marker &). () constructs a trivial graph that has neither a node
nor an edge; and G1 ⊕ G2 constructs a disjoint union of G1 andG2 , i.e., the set of nodes of G1 ⊕G2 is the disjoint union of those ofG1 and G2 and branching of nodes (B) is the same as the original.
Then, G1 @G2 appends two graphs by replacing the output markers
of G1 with an ε-edge pointing to the corresponding input nodes of
G2 , and cycle(G) replaces the output marker of G with ε-edges
pointing to the corresponding input nodes of G to form cycles.
Note that this set of constructors is powerful enough to describe
any finite ordered graphs (although such a description may not be
unique). More precisely, for any finite graph, there is a term usinggraph constructors whose interpretation is bisimilar to the given
graph. This can be shown in a quite similar way to that in (Buneman
et al. 2000). For instance, the ordered graph in Figure 2(a) can beconstructed as follows:&n 1 @ cycle((&n 1 := [d : [&n 2 ]] ++ [a : [&n 4 ]]) ⊕(&n 2 := [c : [&n 3 ]]) ⊕(&n 3 := [d : [&n 2 ]]) ⊕(&n 4 := [b : [&n 3 ]] ++ [&y])).

()Structural Recursion

Structural recursion in λFG provides a powerful mechanism to describe transformations and queries over ordered graphs that guarantees the termination of the computation and preserves the finitenessof graphs.
In general, the typing rule of srec is the one given in Figure 4;
but here, for ease of explanation, we will use the following simplified variant in which the input graph has no output marker.
` e: Label×G∅ → GZ
Z

Z×X
` srec0 (e, d): GX∅ → GZ×∅&x1 ... &xk&x1 ... &xk&x’1 ... &x’m

G1

G2

&y1 ... &yn &y1 ... &yn
G1G2

G1
&y1 ... &ym
εε&y1 ... &ym
G2&z1 ... &zn
G1@G2

This srec0 is obtained as syntax sugar from the original srec:εε&x1 ... &xm
G&x1 ... &xm &y1 ... &yn
cycle (G)Figure 5. Graph Constructors
polymorphic lambda calculi. This polymorphism in the semantics
of our structural recursion is explained in Section 4.
X
The graph type GX
Y is interpreted as a set Gf Y of finite graphs.
Similarly to the notation given in Section 2.1 for sets of graphs, we{& }use GY to denote GY . The predicate isEmpty(e) is true if thegraph obtained by e has no non-ε-edges in the accessible part.
2.2.1

Z` d: List(GZ
Z×α ) → GZ×αGraph Construction

λFG provides useful graph constructors to build arbitrary finite
ordered graphs. Figure 5 summarizes the constructors; let us see
how type discipline on the input and output markers works foreach constructor. First, [] constructs a root-only graph with thedefault input marker and no output markers. For two graphs G1 andG2 having identical input markers and output markers, G1 ++ G2
concatenates them by adding two branching ε-edges from each newroot to the corresponding old roots of G1 and G2 . Next, [a : G]extends G with a new fresh root node pointing to the old root of
G with an a-labeled edge; the constructor [&y] constructs a graphwith a single node marked with an output marker &y (in (Buneman
et al. 2000), [a : G] and [&y] are denoted as {a : G} and &y,
respectively). Marker renaming &x := G associates an input marker&x with the root node of G (here, G should have only one default

srec0 (e, d) = srec(e, i ◦ d ◦ p)def

ZZ
where p : List(GZ
Z×α +GZ×∅ ) → List(GZ×α ) discards eleZZ
ments in GZ×∅ in an input list and i : GZ×α → GZ
Z×α+Z×∅ isthe obvious isomorphism. Throughout this section, we will simply
srec for srec0 .
Now let us briefly explain the semantics of srec(e, d); there are
two different styles: recursive semantics and bulk semantics. Recursive semantics is more concise and useful for reasoning about not
only the behavior of a function defined in a recursive way but also
program transformation/optimization (This will be considered in
Section 5.1). On the other hand, bulk semantics is useful for understanding how a graph is transformed on the whole, for parallel computation, and for proving the termination and finiteness-preserving
properties. We will explain recursive semantics in a simple form
here and formally describe these two semantics in Section 4.
We introduce a reasonable condition called productionconsumption compatibility (PCC) on e and d so that we can givea clearer form of recursive semantics. The condition is explained
in detail in Section 4.1, and the following examples in this section
satisfy it. Furthermore, for simplicity, we consider the following
case: d = foldr( , ι ) for some monoid ( , ι ) on GZ
Z×α ; weconsider general d in Section 4.1. The structural recursion functiondef
f = srec(e, d) satisfies the following equations (here, equality
means the bisimilarity):f ([])
f (g1 ++ g2 )f ([l : g])f (&x := g)f (())
f (g1 ⊕ g2 )

=
=
=
=
=
=

ι
f (g1 ) f (g2 )
e(l, g) @ f (g)(⊕&z∈Z (&z , &x ) := [(&z , &)]) @ f (g)()
f (g1 ) ⊕ f (g2 ).

(1)

&
book

“ λ-calculi”

book

title
section section
title“untyped
λ-calculus”

book

title
sectionsectionparagraphintroduction

title

refs

refs “π-calculus”

ref“data encoding”

ref
book

book

Figure 6. Ordered Graph Representation of Books

Though the above equations do not necessarily determine the functions f uniquely (up to bisimilarity), we can obtain a definition off by the above equations: graphs can be regarded as infinite trees
constructed by the above seven graph constructors (i.e., all the ninegraph constructors but @ and cycle), and hence the above equations can be taken as a definition by a fixed-point operator.
Thus, f transforms graphs along the structures of graphs; e replaces a label with a new graph, and d (i.e., ) acts on branches
and transforms in sibling directions. The fourth equation is just renaming of input markers and the fifth and sixth equations are casesof multi-rooted graphs; these three equations are straightforward,
and so will be omitted in other forms of recursive semantics given
later. In the case of the monoid (++, [])—this satisfies PCC withany e—, the above recursive semantics is the same as given in
UnCAL (Buneman et al. 2000) except that we treat ordered graphs
rather than unordered graphs.
Though the above recursive semantics gives us a definition of
the structural recursion, it is not obvious how to make the semantics
terminating and that the semantics outputs finite (up to bisimilarity)graphs for given finite input graphs. It is the bulk semantics thatshows the termination and finiteness of output graphs; and the bulk
semantics satisfies the above equations.
In the following, we give several examples demonstrating thepower of our language in transforming ordered graphs. Further
examples are given in Sections 4.1 and 5.2.
Example 2. This example shows how we can manipulate edges of
the graph and change its shape. The following structural recursion
a2d xc replaces all labels a with d and contracts c-labeled edges
by using the function rc (remove c).
a2d xc = srec(rc, foldr(++, []))
where rc(l, g) = if l = a then [d : [&]]
else if l = c then [&] else [l : [&]]
Applying the function a2d xc to the graph in Fig. 2(a) yields thegraph in Fig. 2(c). Note that [&] can be considered as a hole thatwill be later filled in with a recursive result.
Example 3. This example demonstrates that our structural recursion can define transformations in the sibling direction, showingthat it is more powerful than the structural recursion in UnCAL.
The following function reverses the branches of each node of agraph.
revBranches = srec(idE, foldr(+̂+, []))
where idE(l, g) = [l : [&]]
r1 +̂+r2 = r2 ++ r1

Example 4. This example demonstrates the usefulness of nested
structural recursion. Figure 6 shows an ordered graph representation of a list of books that contains hierarchical structures with“section”-labeled edges. Since “section”s must be ordered andthere would be reference links in books, we can regard books
as ordered graphs. The following nested structural recursion
toc, which is adapted from (Robertson et al. 2009), computes atable-of-contents of books in which sections can be arbitrarily
nested:toc = srec(extractSection, foldr(++, []))
where extractSection(l, g) =if l = section
then [section : (get title(g) ++ [&])]
else [&]
where the function get title, again defined by a structural recursion, results in the title of the section.
get title(g) = srec(extractTitle, foldr(++, []))
where extractTitle(l1 , g1 ) =if l1 = title
then [title : srec(λ(l2 , g2 ).[l2 : []], foldr(++, [])) (g1 )]else []
Example 5. We can define complex graph transformations bygluing together smaller ones. Suppose that we want to make areverse version of the table-of-contents of a book. We can simply
define it as
tocRev(g) = revBranches (toc(g)).
Before ending the review of λFG , it is worth remarking thatcompared with the structural recursion in UnCAL (Buneman et al.
2000), structural recursion in λFG can deal with ordered graphs
and computations on the sibling dimension of graphs; in fact, srec
in UnCAL does not have the function argument d. As will be seen
later, the key to the success of our extension from unordered graphs
to ordered ones is a new definition of bisimilarity for orderedgraphs having ε-edges, under which (finite) ordered graphs areequivalent to (possibly infinite) regular trees up to bisimilarity.
In the rest of this paper, we will formally define our version ofbisimilarity on ordered graphs, give a formal semantics for λFG ,prove the three important properties of λFG , namely bisimulation
genericity, termination, and finiteness-preservation, and demonstrate how to reason about graph transformations.

3. Ordered Graphs and Bisimilarity
As discussed in the introduction, direct manipulation of graphs isdifficult. We will tackle this problem by regarding graphs as theirequivalent trees so that we can manipulate graphs as if to manipulate trees. To this end, we need to define the semantic equivalence
for the graph model of λFG : bisimilarity between ordered graphs. It
should be noticed that ordered graphs have a big problem that does
not occur with unordered graphs: i.e., ε-elimination might induce
branches with an infinite width. In the following, we shall illustrate
this problem and show how to define bisimilarity between orderedgraphs. We will show an effective procedure to avoid infinite-widthgraphs.
3.1 Bisimilarity for Ordered Graphs
Let us show some examples of ordered graphs in order to geta feeling for the bisimilarity to be defined. Consider the graphs
in Figure 7. Unfolding the graph Gs will yield an infinite tree(the graph in the middle), and performing “ε-elimination” on theinfinite tree will give the graph on the right, whose branchings

is called a proper branch of v if the in -th branch B(vn ).in is notan ε-edge; i.e., it is either a non-ε edge or an output marker. The setof all proper branches of v in G is denoted by Pb(G, v).

00

Gs

00

a
0

01

∼

a

10

∼

00

Definition 7 (Order on Proper Branches). Given two properεεbranches p = (v →i0 v1 ... →in−1 vn →in ) and
ε
ε
0
0
0
p = (v →i00 v1 ... →i0 0
vn0 →i0 0 ), let their branch indexasequences be p̃ = (i0 , ..., in−1 , in ) and p̃0 = (i00 , ..., i0n0 −1 , i0n0 ).

a

1

11

Gd

aa
...
01 11

...

n −1

0

a
1

∼

10

01 20

a

a

a
...

def

... 11 ... ... 21 ...

a

a
...

...

...

11

01

21

look like a stream. However, such infiniteness that occurs in ordered graphs having ε-edges is not just the stream type, as in thenext example Gd . Unfolding Gd will yield the tree in the middle,
and performing “ε-elimination” will give the graph on the right.
This graph has a set of branches behaving like the ordered set{n/2m ∈Q | n, m ∈ N, 0<n<2m }, which is a dense countable linear ordered set.1 It is worth noting that, if we were in an unorderedsetting where the branches are sets (that is, duplications of identical branches are ignored), Gs and Gd after ε-elimination would
be bisimilar to the graph with only one branch; consequently, εelimination in this case would just delete the ε-loops.
Now let us define bisimilarity between ordered graphs. As canbe seen from the above examples, the ε-elimination of an orderedgraph might induce a countable width. Therefore, we shall first
define a generalized notion of an “ordered graph with a countable
width”, and then proceed to define bisimilarity for such generalizedgraphs. To this end, for a set S, we extend the set of lists List(S)(=Σn∈N S n ) to that of the countable list CList(S) defined as
def

CList(S) = ΣL∈L S L
where N is generalized to L, the set of countable linear orderedsets up to order isomorphism 2 . Replacing List with CList, we
extend the notion of ordered graph to that of ordered graph with acountable width. The set of such extended graphs is denoted byX
G cX
Y . Certainly, our original ordered graphs GY are a subset ofcX
G Y.
Once we become aware of the importance of countable linear
order, our idea to define bisimilarity between graphs in G cX
Y israther simple. Informally, given two graphs, a relation R is a bisimulation relation if for any two R-related nodes v and v 0 , their corresponding proper branch sets are related through R. Here a proper
branch of a node is defined as a path from v going through zero or
more ε-edges and reaching a non-ε-edge.
Now we see the formal definitions. For a branching function
B(v), we use |B(v)| to denote the countable linear ordered set L,
call i ∈ |B(v)| a branch index of a node v, and write B(v).i ∈Lε ×V +Y for the i-th branch.
Definition 6 (Proper Branch). Let G = (V, B, I) ∈v ∈ V . The path starting from vεdef

We define p ≤Pb p0 ⇐⇒ p̃ ≤l p̃0 , where ≤l is the lexicographicalorder between branch index sequences.

00∼

Figure 7. Graphs with Stream Branching and with Dense Branching

G cX
Y

and

ε

v (= v0 ) →i0 v1 ... →in−1 vn →in
1 In this paper, the term countable includes the finite case.
2

n

def

More precisely, CList(S) is the set of objects of the skeleton of thecomma category (U ↓ S) where U : CLO → Set is the forgetful functorfrom the category CLO of countable linear ordered sets and monotonefunctions.

Now we are ready to define the bisimilarity.
Definition 8 (Bisimilarity). For two graphs G = (V, B, I) and0
G0 = (V 0 , B 0 , I 0 ) in G cX
Y , a relation R between V and V iscalled a bisimulation relation, if for any vRv 0 , there is an orderisomorphism f : (Pb(G, v), ≤Pb ) → (Pb(G0 , v 0 ), ≤Pb ) satisfying the following order-preserving property: For any proper branchεεp = (v →i0 ... vn →in ) ∈ Pb(G, v) with f (p) = (v 0 →i00000... vn0 →i0 0 ) ∈ Pb(G , v ), we haven

• Edge Correspondence: if B(vn ).in

= Edge(l, u) forsome l ∈ L, u ∈ V , then there exists u0 ∈ V 0 such thatB 0 (vn0 0 ).i0n0 = Edge(l, u0 ) and uRu0 ,• Marker Correspondence: if B(vn ).in = Outm(&y) for some&y ∈ Y , then B 0 (vn0 0 ).i0n0 = Outm(&y).

Two graphs G and G0 are bisimilar (denoted by G ∼ G0 ) if there isa bisimulation relation R such that for every input marker &x ∈ X,
I(&x ) R I 0 (&x ).
3.2 Elimination of ε-Edges
The ε-edges are introduced (and necessary) in our internal semantics of graph transformation, but unnecessary ε-edges in the final
result should be eliminated. The following definition leads to aprocedure to eliminate ε-edges (for example by taking transitive
closures) from the graphs and shows that the graph obtained by
ε-elimination is bisimilar to the original graph.
Definition 9 (ε-elimination). For a graph G = (V, B, I) ∈ G cX
Y ,the ε-elimination ε-elim(G) of G is a graph (V, B 0 , I) ∈ G cX
Y
def
def
where |B 0 (v)| = Pb(G, v) and B 0 (v).p = B(vn ).in for p =ε(v →i0 ... vn →in ) in |B 0 (v)|.
Note that the ε-elimination does not change the sets of nodes.
Proposition 10.
1. For any G ∈ G cX
Y , ε-elim(G) has no ε-edge, and G andε-elim(G) are bisimilar.
2. Two graphs G, G0 ∈ G cX
Y are bisimilar if and only if ε-elim(G)and ε-elim(G0 ) are bisimilar.
3.3 Decidability of Empty and Finite-Width Graphs
In our graph transformation, i.e., any function from a graph typeto a graph type in λFG like tocRev in Example 5 the input graphis usually an ordered graph that has neither ε-edges nor infinite
width, but the result may contain ε-edges in our context. In thefollowing, we show that, given a graph with ε-edges, it is possible
to decide whether there is a corresponding bisimilar ordered graphthat has neither ε-edges nor infinite width, and there is a procedure
to compute out such a bisimilar graph.
Let FG/ε be the set of finite ordered graphs (with finite widthand possibly with ε-edges) that are bisimilar to some finite orderedgraphs without ε-edge or infinite width. The following procedureanswers (decides) whether a finite ordered graph G is in FG/ε ornot.
1. For each node accessible from a root, check if there is an εcycle—a cyclic path consisting only of ε-edges—on the nodeor not. If there is no ε-cycle, then G is in FG/ε.
2. Otherwise, for every accessible node with an ε-cycle, if there is
no proper branch, then graph G is in FG/ε; otherwise, it is not
in FG/ε.
If G is in FG/ε, we can effectively eliminate ε-edges; otherwise,
it is impossible to eliminate ε-edges and keep the width finite.
isEmpty(G) is true iff G has no non-ε edge in the accessible
part, and thus, it is decidable.
Note that this procedure is useful for evaluating λFG ; though
we need ε-edges for the implementation—for structural recursion
and for the efficiency of the graph calculation—, practical graphs
in the real world have no ε-edges. If a user writes such a practicalquery, the result should be a graph in FG/ε; if it is an incorrect query
not intended by the user and then if the result has ε-edges, theabove procedure can determine this and can warn the user. Notealso that, in the FG/ε class, since we can eliminate ε-edges, we canuse familiar effective procedures for checking bisimilarity and for
obtaining the minimum graphs in a similar way to that of unorderedgraphs.
3.4

Graph Constructors

In Section 2.2.1, we have given an intuitive explanation for ourgraph constructors; the formal semantics of them should be obvious. As an example, we give the semantic definition of G1 ++ G2(the formal semantics of all graph constructors can be found in Appendix A). For Gi = (Vi , Bi , Ii ) ∈ GYX ,G1 ++ G2 = (V1 ∪ V2 ∪ {v1 , . . . , vm }, B 0 , I 0 )
def

where
v1 , . . . , vm are fresh node identifiers{&x1 , . . . , &xm } = Dom(I1 ) (= Dom(I2 ))B 0 = B1 ∪ B2 ∪{vi 7→ [Edge(ε, I1 (&xi )), Edge(ε, I2 (&xi ))] | i=1, ..., m}0

I (&xi ) = vi .
Above, we assume V1 and V2 to be disjoint, which is realized bytaking copies of them; recall that node identity is ignored in thecontext of bisimilarity.
One important property of the graph constructors is that they
are bisimulation generic. As an example, consider G1 ++ G2 ; wewant to show that ++ is bisimulation generic in the sense thatif G1 ∼ G01 and G2 ∼ G02 , then G1 ++ G2 ∼ G01 ++ G02 .
We say that two graphs are strongly bisimilar if they are bisimilar without special treatment of ε-edges (i.e., ε-edges are considered as ordinary edges but labeled ε). It is quite straightforward to see that the graph concatenation constructor ++ is stronglybisimulation generic. Furthermore, we can see that ε-elim(G1 ++G2 ) is bisimilar to ε-elim(ε-elim(G1 ) ++ ε-elim(G2 )). This meansthat strong-bisimulation genericity implies bisimulation genericity for this graph constructor. Similarly we can show other graphconstructors are bisimulation generic. This leads to the following
proposition.
Proposition 11 (Bisimulation Genericity of Graph Constructors).
All the graph constructors are strongly-bisimulation generic andalso are bisimulation generic.

4. Structural Recursion
Here, we give the semantics of our structural recursion; we modify
structural recursion for unordered graphs UnCAL (Buneman et al.
2000) to deal with ordered graphs and extend it so that we cantransform graphs also in the sibling direction. We start by giving
recursive semantics of our structural recursion; this enables us tounderstand the behavior of functions by recursive reasoning. After
that, we give the bulk semantics of the structural recursion to show
the termination and finiteness preserving properties.
Next, we show that our structural recursion and every transformation in λFG are bisimulation generic; i.e., they returns bisimilar
results for bisimilar inputs. This bisimulation genericity plays animportant role in our framework, allowing us to reason about properties of graphs by using (possibly infinite) trees bisimilar to them.
To this end, we extend the notion of bisimilarity to higher orderfunctions in Section 4.3 and give the whole semantics of λFG .
After that, we will discuss implementation and termination
property. Finally, we will summarize relations of conditions andresults provided in this section.
Below, we often use the following marker renaming graphs:
for a “marker renaming” function f : X → Y , we define a graphdef L
bf c ∈ GYX as bf c =&x∈X &x := [f (&x )]. As two use cases,
0X
0for G ∈ GY with f : X → X, bf c @ G ∈ GYX is “input marker
renaming” by f : an input marker f (&x ) is replaced with &x andinput markers of G that are not in the image of f are removed. Also,
for G ∈ GYX with f : Y → Y 0 , G @ bf c ∈ GYX0 is “output marker
renaming” by f : an output marker &y is replaced with f (&y).
4.1 Recursive Semantics
In Section 2.2.2, we described the recursive semantics of ourstructural recursion in the simple setting where we ignored output
marker cases, assumed production-consumption compatibility(PCC), and restricted d to be the form of foldr( , ι ). Here,we will give other forms of recursive semantics, relaxing theserestrictions; but we still ignore output marker cases for the sakeof simplifying the presentation. (For recursive semantics for thegeneral d without ignoring output markers, see Appendix B.)
Z
Hence, in this subsection, the type of d is List(GZ
Z×α ) → GZ×α .
(In bulk semantics, though, we will deal with also output marker
cases.)First, let us explain the polymorphism α in the type of d. This α
plays two important roles: It is used to substitute a concrete set for
α in order to express recursive semantics and define bulk semantics;
it is also used to show bisimulation genericity of the bulk semantics
by using relational parametricity. Formally, we should introduce
α by formulating λFG as polymorphic typed lambda calculus aswell as by introducing sets of markers as types, but to keep thepresentation simple, we formulated λFG as a simply typed lambda
calculus. In the following explanation of semantics, we will write
dX for the “type application” of d to X on α, and when we interpretsrec(e, d), we introduce the universal quantifier ∀α. for d to bind
α. We use the “type application” only in semantics for the above
purposes, and do not use syntactically in λFG itself. Thus, λFG
is essentially a rank-2 polymorphic lambda calculus; hence, type
inference is decidable (Kfoury and Tiuryn 1990).
Now, let us consider recursive semantics of f = srec(e, d). For
general e and d, the straightforward generalization of Equations (1)should be, just in form, as the following:f ([l1 : g1 ] ++ · · · ++ [ln : gn ])`´= d∅ [e(l1 , g1 ) @ f (g1 ), . . . , e(ln , gn ) @ f (gn )] .

(2)

This equation means that, when we start from the root of a graph,
we have the branches [li : gi ] under the root; then f first computes

e(li , gi ) and recursively computes f (gi ); they are connected by @and finally are transformed in the sibling direction by using d.
However, for general e and d, this recursive semantics is notnecessarily correct, i.e., the structural recursion functions definedby bulk semantics given later do not necessarily satisfy this equation. On the other hand, if we evaluate the above recursively, then,since the computation of d depends on f (gi ), and since gi may
include a cyclic path returning to the original root, the evaluation
may not terminate. Even if it terminates, the result is not necessarily
bisimilar to the result by bulk semantics.
Instead, for general e and d, we have the following recursive
semantics.
f ([l1 : g1 ] ++ · · · ++ [ln : gn ])`´= dn̄ [e(l1 , g1 )@bin1 c, . . . , e(ln , gn )@binn c]
“`
´
`
´”
@ biso1 c@f (g1 ) ⊕ · · · ⊕ bison c@f (gn )def

In the next example, e and d do not satisfy PCC, but we still canreason that this works as expected from the recursive semantics (3).
To contract the even edges of a graph, from (3), it is enough that e isan “identity” and d contracts even labeled edges; i.e., we can apply
defeven contract = srec(e, d) wheredefe(l, g) = [l : &],defd([]) = [] ,defd([g]) = g,d(g :: g 0 :: gs) = g ++ p(g 0 ) ++ d(gs),
def

def

{& }

{& }

p = srec(λ(l, g).[&], foldr(++, [])) : G{&}×α → G{&}×α .
4.2 Bulk Semantics

(3)

def

where n̄ = {1, ..., n}, ini : Z → Z×n̄ is defined as ini (&z ) =def(&z , i), and isoi : Z×{i} ∼= Z is defined as isoi ((&z , i)) = &z .
This might look a bit complicated, but you can disregard markerrenaming parts @bini c and bisoi c@, which are not essential. A
noteworthy point in Equation (5) is that d is applied before @connects e(li , gi ) to f (gi ); in Equation (2), the order is reversed.
Now, the PCC condition is naturally introduced as the requirement that the recursive semantics (2) and (3) coincide, i.e., theorder of application of d and connecting e(li , gi ) with f (gi ) by
@ may be interchanged. Formally e: Label×G∅ → GZ
Z andZ
d: List(GZ
Z×α ) → GZ×α are called production-consumption
compatible (PCC) if they satisfy the following equation:`´d∅ [e(l1 , g1 ) @ g10 , . . . , e(ln , gn ) @ gn0 ]`´= dn̄ [e(l1 , g1 ) @ bin1 c, . . . , e(ln , gn ) @ binn c]
“`
´
`
´”
@ biso1 c@g10 ⊕ · · · ⊕ bison c@gn0
Intuitively, the above condition says that d consumes only the information in the graphs produced by e and does not traverse beyond
the output markers of the graphs produced by e. For example, if
we write e such that any e(l, G) has no output markers down to
depth three, we can write d that can traverse graphs up to depth
three. Note that, if d changes only the positions of graphs in an
input list—such positions are regarded as positions of branches—and does not traverse each graph, then d satisfies the PCC condition
with any e.
By definition, if e and d satisfy PCC, then f = srec(e, d)
has the recursive semantics (2). Note that, in this paper, we call
only the functions defined by the following equivalent semantics
structural recursion functions (and denoted by srec(e, d)): (i) thebulk semantics (Definition 13), (ii) the recursive semantics (3), and(iii) when PCC holds, the recursive semantics (2) and (1). For
example, if e and d do not satisfy PCC, then in this paper we do
not call functions defined by the recursive semantics (2) structural
recursion functions even if they terminate.
Introducing d is our extension for sibling transformations fromthe original structural recursion in UnCAL. Note that, no matter
whether we use the general recursive semantics (3) or the recursive
semantics (2) with PCC, access by d is confined to the graphs
produced by e anyway. This is the key restriction on our structural
recursion for termination.
Example 12. In this example, d satisfies PCC with any e. To redef
move the even branches of a graph, we can apply even remove =
def
def
def
srec(e, d) where e(l, g) = [l : &]; and d([]) = [], d([g]) = g, anddefd(g :: g 0 :: gs) = g ++ d(gs).

Here, we give bulk semantics of the structural recursion srec(e, d)for a general d not assuming PCC nor ignoring output markers.
Before giving the formal definition of the bulk semantics ofsrec(e, d), we illustrate the behavior of the semantics in an exdef
ample a2d xc = srec(rc, foldr(++, [])) (see Example 2 for rc).
Mainly, an evaluation with the bulk semantics consists of threesteps; we start with the input graph (a) in Figure 8.
1. Applying the Map Computation on Edges with e
We apply the function rc (which renames a-labeled edges as
d-labeled ones and contracts the c-labeled edges) to every llabeled edge and the graph g following the edge, to yield aZgraph in GZ. Let us call the graphs produced by an expression
e e-graphs. Graph (b) is a graph whose edges are labeled by
rc-graphs.
2. Applying Map Computation on Nodes with d
For each edge—from a node v to a node v 0 —of Graph (b),we replace every output marker &z of the e-graph with a pair(&z , v 0 ), which will be used in the next “grouping” step. Next,
for every node v of Graph (b), we use binary operator ++ tocombine all e-graphs which are labels of the branches of v. Let
us call the graphs produced using d (= foldr(++, [])) d-graphs;
Graph (c) shows the result. Nodes 1 and 4 have more than one
branch which need to be merged using ++. After producing thed-graph for v, we replace each input marker &z with a pair(&z , v).
3. Grouping New Graphs with ε-Edges
Now, for each node of Graph (b)—equivalently, for each nodeof the original graph—, we have a d-graph produced as above.
We group all these d-graphs in Graph (c) by connecting every
output marker (&z , v) of every d-graph to the corresponding
input node of some d-graph by using an ε-edge. The root of
the new graph is that of the d-graph on the original root node.
Thereby, we get Graph (d) as an evaluation result of the structural recursion. Graph (e) is the graph obtained by performing ε-elimination on Graph (d). We remark that ε-elimination
may increase the number of non-ε edges as this example. (Wecan further minimize Graph (e) if necessary, resulting the graphin Figure 2(c).)
Before applying a structural recursion function srec(e, d)
to G, we have to perform ε-elimination on G; if ε-elim(G)has infinite width, we raise an error. Without the ε-elimination,
if we extend the bulk semantics to treat input graphs havdef
ing ε-edges by extending e to ē(ε, g) = bidZ c, then thesrec(ē, d) is not necessarily bisimulation generic, as shownby the following counter example. The two graphs on the leftare bisimilar, but if we apply the structural recursion function
even remove in Example 12, the resulting graphs are not bisimilar.

&

(a)

a
b

d
2

d

3

c
(b)

srec(rc, foldr(++,[]))
4
&y

1
(&,1)

&
d

&

&

(&,&)

d

d

(&,2)

(&,4)

3

&

(&,2)
4

2

&y

(&,3)

(&,4)
(&,&y)

d

b

b

(&,3)

&

&

4(&,&y)

d
3
(&,2)

d

d

(&,3)
&
b

b
(&,&y)

ε-elimination

(d)

(c)

&
d

d
d
d

1

2

d
d

&

&
d

(&,&)

(e)

1

&

Figure 8. Bulk Semantics of Structural Recursion: An Example of srec(rc, foldr(++, []))

a
2

&
1

&
1
b
4

3

c
5

~

&
1

a b c
2 3 4

a

䋏

spondence,

&
1

~/

2

∼
=

a

c

2

4

Z×V
we obtain a graph G0 = oplus(d0V ◦ B 0 ) ∈ GZ×V+Z×Y , whichcorresponds to (c) in Figure 8; then, in correspondence with (d) in
Figure 8, we define
defThough, if d = foldr(++, []) or d = foldr(+̂+, []) (reverse function), then we can show the bisimulation genericity without
performing ε-elimination.
Now let us give the formal definition of the bulk semantics ofthe structural recursion. Note that the following definition is moreconcise than the one given in (Asada et al. 2012), which mimics theoriginal bulk semantics of UnCAL given in (Buneman et al. 2000);
and this simplification makes the proof of bisimulation genericity
clearer.
Definition 13 (Bulk Semantics). For functions
e: L×GY → GZZ

Z
Z×V
oplus : (V →GZ×V→ GZ×V+Z×Y ) −+Z×Y ,
Ldef
oplus(f ) =(&z,v)∈Z×V (&z, v) := ([&z] @ f (v))

ZZZ
d: ∀α.List(GZ×α+GZ×Y) → GZ×α+Z×Y,

Z×X
a structural recursion function srec(e, d): GYX → GZ×Y
is defined as follows.
Let G = (V, B, I) be a graph in GYX . As explained above,
we perform ε-elimination on G in order to ensure bisimulation
genericity; hence, we assume G has no ε-edges. Let us defineZẽ: L×V → GZ
as e ◦ (idL ×G|(-) ), where G|(-) : V → GY
def

extracts the subgraph of G whose root is a given node: i.e., G|v =(V, B, {&7→v}).
Then, as in the first step explained above, we construct a newdefbranching function B 0 = map(hẽ, π2 i+idY ) ◦ B of typemap(hẽ,π2 i+id

B

)

Y
Z
V −
→ List(L×V +Y ) −−−−−−−−−−−→ List(GZ
×V +Y ).

This corresponds to a step producing Graph (b) in Figure 8.
def
As for the second step, first, we construct a function d0α =dα ◦ map(p+q) of typemap(p+q)

d

α
Z
Z
Z
List(GZZ ×α+Y ) −−−−−→ List(GZ×α
+GZ×Y
)−
→
GZ×α+Z×Y

def

def

where p(G, &a) = G @ b&z 7→ (&z , &a)c and q(&y) =b&z 7→ (&z , &y)c. Next, by using the following bijective corre-srec(e, d)(G) = bidZ ×Ic@ cycle(G0 )def

Z×X(∈ GZ×Y).

It is worth remarking that the above bulk semantics is essentiallyroot-independent: the whole part except for the final step—i.e., till
constructing cycle(G0 )—does not use the input function I.
The following is clear from the above bulk semantics.
Proposition 14. If the functions e and d map finite graphs to finite
graphs, so does srec(e, d).
From the above bulk semantics, we can show obviously
the termination property of λFG . We can implement the above
bulk semantics in an obvious way: We may represent graphs(X, Y, V, B, I) using “set” and “map” (implemented as, e.g.,balanced trees); X,Y , and V are as “set”s, and B and I areas “map”s. Then implementation of the bulk semantics is
straightforward. It is clear that the computation of the bulk
semantics terminates by the above definition and the finitenesson nodes and width of graphs, which is ensured by the above
proposition. Our actual implementation in OCaml can be found at
http://www.biglab.org/src/lambdaFG/; note that din srec in the implementation is currently restricted to the form
foldr( , ι ).
4.3 Semantics of λFG and Bisimilarity on Functions
Before proving the bisimulation genericity of the structural recursion, we will summarize the whole semantics of λFG .
A requirement of our semantics is that it should guaranteethat any transformation—including the one using higher orderfunctions—in λFG must be bisimulation generic. To this end,
we extend the notion of bisimilarity on graphs to bisimilarity

on functions in λFG . We have defined bisimilarity for graphtypes GX
Y , and we can use the equality relations for the otherbasic types. It is well known that, if we want to lift equivalence
relations to function types, we need to switch from the notion ofan equivalence relation to that of a partial equivalence relation,i.e., equivalence relation on some subset of the original set. Thisis because, in the current case, it is not true that all functions on
Gf X
Y are bisimulation generic, so we have to focus on its subset
consisting of bisimulation generic functions.
Formally, for types σ of λFG , we define binary logical relations∼σ from the above equivalence relations on the base types. Let us
recall the logical relation ∼σ only in the essential case, i.e., function
types: σ = σ1 → σ2 (for other cases, one can consult (Mitchelldef1996)). We define a binary relation ∼σ on [[σ]] = [[σ1 ]] → [[σ2 ]] as
0

0

def

0

0

0

Next, from the assumption that e1 ∼ e2 and d1 ∼ d2 , thefollowing diagram commutes.

B2

4.4

Bisimulation Genericity of the Structural Recursion

We prove a stronger statement of bisimulation genericity than theoriginal one in (Buneman et al. 2000), which proves only first-orderbisimulation genericity, i.e., only bisimulation genericity on grapharguments. In addition, our proof is much clearer than the original
naive proof. This simplification should make further extensions ofstructural recursion easier.
Theorem 15 (Bisimulation Genericity of srec). The higher orderfunction srec is bisimulation generic; i.e., for e1 ∼ e2 , d1 ∼ d2 ,and G1 ∼ G2 , srec(e1 , d1 )(G1 ) ∼ srec(e2 , d2 )(G2 ).
We will use the following notions and notations in the proofof the above theorem. We write R : A1 p A2 for a relation
R ⊆ A1 ×A2 ; e.g., the diagram on the left below means that if
a1 R a2 , then f1 (a1 ) S f2 (a2 ).
A1
R

f1

_

A2

f2

/ B1
_S

X1

I1

S_

/ B2

X2

I2

/ V1
R_
/ V2

B1

B2

/ CList(L×V1 +Y1 )_ CList(L×R+T )/ CList(L×V2 +Y2 )For S : X1 p X2 and T : Y1 p Y2 , let us define the relation
X1
p GYX22 : for Gi , let (Vi , Bi , Ii ) = ε-elim(Gi ), then∼S
T : GY1
p V2 such thatG 1 ∼ST G2 if there exists a relation R : V1
the right diagram above commutes (i.e., each of the two squares istrue). We write simply X for the diagonal relation between X andX
p GYX is the same as ∼.
X, then note that ∼X
Y : GY
Proof. Let Gi be (Vi , Bi , Ii ). From G1 ∼ G2 , there exists R :V1 p V2 such that the following diagram commutes.
X
X

I1

I2

/ V1
R_
/ V2

B1

B2

/ List(L×V1 +Y )_ List(L×R+Y )/ List(L×V2 +Y )

(4)

d0

map(he˜2 ,π2 i+idY )

d02 V

2

2

Note that to show the right square above, we also use the relationalparametricity of di and hence of d0i ; see Definition 13 for thedefinition of d0i . Then, for the above compositions, transposing Vi
by using oplus as in Definition 13 yields
1G01

f ∼σ f ⇐⇒ ∀x, x ∈ [[σ1 ]]. (x ∼σ1 x ⇒ f (x) ∼σ2 f (x )).
For any type σ, ∼σ becomes a partial equivalence relation on [[σ]],defi.e., an equivalence relation on the subset |∼σ | = {x ∈ [[σ]] | x ∼σx}. We say a function f : [[σ1 ]] → [[σ2 ]] bisimulation generic if f isin |∼σ1 →σ2 |.
Now from the Basic Lemma of the logical relation (Mitchell1996), interpretations of all the terms are bisimulation generic if interpretations of all the constants (including constant functions) arebisimulation generic; accordingly, we can form a model (a cartesian closed category) of λFG such that the interpretations of types
are the quotient sets of the partial equivalence relations. We havealready shown the bisimulation genericity of graph constructors,
and now we will show the same for the structural recursion.

map(he˜1 ,π2 i+idY )1 V1Z
V1 / List(L×V1 +Y ) / List(GZZ ×V1 +Y ) / GZ×V
1 +Z×YZ__∼
List(∼Z
×R+Y)
R _ List(L×R+Y ) _Z×R+Z×Y
Z
Z
Z///
List(L×V2 +Y )GZ×V +Z×Y
V2
List(GZ ×V2 +Y )

B1

1

G02

Z×V1
/ GZ×V
1 +Z×YZ×R_ ∼Z×R+Z×Y
Z×V2/ GZ×V+Z×Y

0i.e., G01 ∼Z×R
Z×R+Z×Y G2 .

(5)

2After that, we can show that0cycle(G01 ) ∼Z×R
Z×Y cycle(G2 ),(6)

and from the left square of the diagram (4) we get
0bidZ ×I1 c @ cycle(G01 ) ∼Z×X
Z×Y bidZ ×I2 c @ cycle(G2 )i.e., srec(e1 , d1 )(G1 ) ∼ srec(e2 , d2 )(G2 ).
For readers familiar with category theory, we will elaborate a biton the general technique behind Equation (6). From the correspondence Y 7→ GY , we can construct a monad on Set; then cycle
becomes an iteration operator (dual of fixed point operator) in its
Kleisli category. Furthermore, the iteration operator is uniform onvalues (i.e., functions). The above Equation (6) from Equation (5)is then the uniformity principle on relations (Hasegawa 2002).
4.5 Remark
We conclude this section with a summary of some conditions that
we assumed occasionally. (Ignoring output marker cases is just for
presentation and not essential.)
We use PCC to obtain more familiar form of recursive semantics (2), and moreover we assumed d to be in the fold form of
monoid to obtain simpler recursive semantics (1). The PCC condition and its recursive semantics are also used for optimization
given in Section 5.1.
The polymorphism of α of d is used to express recursive semantics and define bulk semantics, and its parametricity is used toprove the bisimulation genericity of the bulk semantics. The preprocessing of ε-elimination for input graphs of structural recursion
functions is also used to prove the bisimulation genericity.
Termination and node-finiteness preserving properties of thestructural recursion was shown via the bulk semantics, and essentially comes from the suitable restriction of recursion pattern; ourstructural recursion still has rich expressive power (see Section 5.2)
and enables systematic optimization by the recursive semantics (seeSection 5.1).

5. Discussion
5.1 Optimization of λFG Programs
Embedding graph queries into lambda calculus as structural recursions would make query optimization easier and more systematic.
This is not only because existing optimization techniques for functional programs can be directly brought in, but also because structural recursion itself has nice algebraic properties for optimization.

Here, we illustrate the usefulness of structural recursion in reasoning and manipulating graph queries with two known transformation
techniques, fusion and tupling.
Fusion Transformation Fusion (or called deforestation) (Meijer
et al. 1991; Gill et al. 1993; Takano and Meijer 1995) is an important program transformation to turn a composition of two structural
recursions into one so that unnecessary intermediate data passed
from one structural recursion to another can be removed. The following is our fusion rule showing that a composition of a function
f and a structural recursion srec(e, d) can be merged into one aslong as the PCC condition holds for e and d:f ◦ srec(e, d) = srec(e0 ◦ e, d0 )holds, provided that f is promoted on d and demoted on @; i.e., forsome f 0 , we havef ◦ d = d0 ◦ map f 0

and f 0 (g @ r) = e0 (g) @ f (r).

Tupling Transformation Tupling (Hu et al. 1997) is another important optimization technique. It eliminates multiple traversals of
the same data. Our following tupling transformation rule reduces
two traversals of G given by two structural recursions into one.
(&x 1 := srec(e1 , d1 )(G)) ⊕ (&x 2 := srec(e2 , d2 )(G))= srec(e, d)(G)where
e (l, g) = (&x 1 := (e1 (l, g) @ [&x 1 ]))⊕ (&x 2 := (e2 (l, g) @ [&x 2 ]))d gs= (&x 1 := d1 (map (λg.[&x 1 ] @ g) gs))
⊕ (&x 2 := d2 (map (λg.[&x 2 ] @ g) gs))
The new structural recursion basically computes in parallel twographs marked by &x 1 and &x 2 . Note that the tuple construction
and projection that are used in the ordinary tupling technique are
encoded here by the disjoint union (⊕) and marker renaming: apair “(g1 , g2 )” is by (&x 1 := (g1 @ [&x 1 ])) ⊕ (&x 2 := (g2 @ [&x 2 ])),
and a projection “πi (g)” is by [&x i ] @ g.
5.2

Expressive Power of λFG

In the previous sections, we described the definition and propertiesof λFG , and showed some interesting query examples. In this section, we discuss the expressive power of λFG from the user’s pointof view, to show that λFG can serve as a basis of query languages
on ordered graphs under bisimulation.
As has already been demonstrated by Buneman et al. (2000)
in the unordered setting, nesting of srec can produce a sequence of combinations of label and graph variable bindings(λ(l1 , g1 ), λ(l2 , g2 ), . . .). We can combine this nesting with conditionals on these variables to express variety of join conditions. For
example, two nested structural recursions can extract subgraphs
following consecutive edges with identical labels. Moreover,regular path expressions of labels can be expressed by srec witha body e generating multiple roots via tupling (Hu et al. 1997), as
shown in Section 5.1. Such an e can be systematically constructedfrom the regular path expressions of labels via finite state automata,as in Buneman et al. (2000) (while NFA is used in (Buneman et al.
2000), we need DFA to make the result well-defined). These kindsof queries in λFG can be concisely expressed by using a moreuser-friendly syntactic sugar like UnQL for UnCAL in (Buneman
et al. 2000) (although we do not give any concrete desugaring ruleshere) so that users do not have to write nested structural recursions
with multiple root expressions manually. For example,
select e where [path:g] in db
binds the graph variable g to every subgraph pointed to by a regularpath expression path from the root of the graph that db is bound to,

G2

G
& 1 a
1

2

∼
b

&

b

a
1

2

2′
b

insert reverse edge

G1′
&

1

a′
a

≁

2
b

G2′ a′
&
1

a

2

2′
b

b

Figure 9. insertion of reverse edge

and will join (++) the graphs generated by the expression e thatrefers the graph variable g.
It is worth noting that, in case of extracting subgraphs underregular path pattern, we just shortcut the edges with unmatchinglabels like in the else clause of extractSection in Example 4.
If there is a cycle of these unmatching labels (labels other thansection in the example) above the matching subgraph, thenthe cycle turns into an ε-cycle, meaning that the result of query
represents infinite number of that subgraphs. This infinity is
no surprising since original input graph essentially includes
infinite number of that subgraphs when the cycle is unfolded.
The infinity in the result is reported by ε-elimination error in
λFG . Interestingly, this exhibits the expressive power of λFG todetect cyclic patterns specified by the automata mentioned above.
For example, extractSection corresponds
to automata on the right, which includes¬sectiona cycle. If this cycle and the ones in the section
input graph matches, then an ε-cycle is
!"#
?/.-,
()*+
>=<
/ '&%$/ 89:;
1
2
produced.
Expressive Power on Sibling Dimension With the parameter dZZof type List(GZ
Z×α +GZ×Y ) → GZ×α+Z×Y in srec we can
express not only queries such as extracting subgraphs as mentioned
above, but also those manipulating siblings of nodes, like reversal(Example 2), removing and contracting even-numbered siblings(Example 12).
Expressiveness under Bisimilarity Equivalence Since our language is bisimulation generic, targeting graphs under bisimilarity
equivalence, queries that distinguish bisimilar graphs are not expressible. For example, we cannot count the number of nodes, since
two bisimilar graphs may have different numbers of nodes. As another example, we cannot insert a ‘reverse’ edge. For example,
in Figure 9, the graph G2 is obtained from G1 by unfolding thecycle formed by the edge labeled b at node 2; hence so G1 andG2 are bisimilar. The bisimulation relation S : G1 .V × G2 .V is{(1, 1), (2, 2), (2, 20 )}. Now suppose we insert for every a-labelededge a reversed a0 -labeled edge like in G01 and G02 . Notice the difference between outgoing edges from node 2 and those from node
20 . In G01 , there is an outgoing edge a0 from node 2. However, in
G02 , there is no such edge from node 20 . So G01 and G02 are notbisimilar anymore. The essential reason for this bisimulation genericity violation is that the reverse edge on a node is inserted on incoming edges while bisimulation is determined by outgoing edges.
So bisimilar nodes are treated differently.
It would be interesting to combine λFG with the predicate ofbisimilarity on graphs. Since (for ε-eliminable graphs) the bisimilarity is decidable, we can readily introduce such predicate in λFG
and express queries that identify nodes in terms of their bisimilarity.

6.

Related Work

Our structural recursion for ordered graphs is very much related
to research on algebras of programming (Meijer et al. 1991; Bird
and de Moor 1996; Hu et al. 2006), where structural recursions
such as folds and catamorphisms are used to structure programs andsystematically manipulate programs. In particular, our approach is
influenced by the many attempts at defining structural recursions
for specific graphs, such as graphs represented by trees with specific pointers (Hamana 2009; Dal Zilio et al. 2004; Oliveira andCook 2012) and graphs represented by trees with embedded functions (Fegaras and Sheard 1996). However, they do not ensure allof the bisimulation genericity, terminating property, and finitenesspreserving property, which are our original goals as explained in
the introduction.
In the database community, structural recursion is an importantprimitive in database queries. Rewriting rules for optimization canbe obtained by exploiting axiom of languages based on structural
recursion. Although it works for various data models such as relations (Breazu-Tannen et al. 1991), nested collections (Wong 1994),
unordered graphs (Buneman et al. 2000), and ordered trees (Robertson et al. 2009), structural recursion for querying ordered graphs
has not been established yet.
As described in the introduction, our work was inspired by the
structural recursion in UnCAL (Buneman et al. 2000) that is practically used for manipulating unordered graphs. We borrow fromdatabase community the idea of how to restrict a structural recursion for infinite regular trees so that a structural recursion for finite graphs preserves finiteness of graphs and becomes terminating,which are desirable properties for query languages. We solve theopen problem of dealing with ordered graphs by providing a novel
definition of bisimulation relation for ordered graphs. To enhancethe expressive power to deal with transformation among children
graphs, we extend the original structural recursion from srec(e) tosrec(e, d) so that d can be used to combine results among children.
A lot of work has been devoted to efficient implementation ofgraph algorithms in lazy functional languages (Burton and Yang
1990; King and Launchbury 1995; Erwig 1997; Johnsson 1998).
The emphasis there is placed on the importance of achieving efficient implementation of general graph algorithms through themonadic model for including actions on the state in the non-strict
context. In contrast, we focus on inductive traversals of orderedgraphs and aim to provide an efficient way to deal with a specificclass of important graph algorithms—graph querying. In addition,
unlike the above where graph equivalences are up to isomorphism,
our graph equivalences are up to bisimilarity and all our transformations are guaranteed to be bisimulation generic.
Algebraic graph transformations (Ehrig et al. 2006) formalize
graph transformations using categories in which objects are graphs
and graph patterns to be matched, and matching be graph morphisms. A step of transformations is realized by a pushout complement followed by a pushout in the double-pushout approach.
Category theory is elegantly used in the proofs and various constructions like transformation rule compositions. In contrast to ourgraph model, their graph model is based on graph isomorphism,
and order between outgoing edges are not considered.
Picard and Matthes (2012) deal with node-labeled graphs using
coinductive data types in Coq proof assistant. Although outgoingedges of their graphs are also ordered and graph equivalence basedon bisimulation is considered, ε-edges are not considered.
Our decision procedure on ε-eliminability under finite-width in
Section 3.3 is close to the eliminability of ε-transition cycles ofweighted automata in Lombardy and Sakarovitch (2012). However,while eliminability of ε-transition cycle in the weighted automata isdetermined solely by the weight of the ε-edge (whether the weightis starable), we also consider the presence of proper branches. Notealso that there is no notion of order between transitions in Lombardy and Sakarovitch (2012), so our ε-elimination cannot be derived from that of weighted automata.
The treatment for ε-edges in the current paper was inspiredby (Jacobs 2010). Although there was no consideration of ε-edge
itself in that study, the author showed that the trace semantics forsome kinds of coalgebra induces iteration operators by forgetting
the length of trace paths; the resulting iteration operators can be
regarded as ε-elimination. The countable list monad CList is nottreated in that paper (or in any literature to the best of our knowledge); it does not satisfy the assumption of the theorem in that paper. Since our definition of bisimilarity agrees with (strong) bisimilarity defined generally by coalgebra theory if graphs contain noε-edges, Proposition 10 suggests that our bisimilarity for graphs
having ε-edges can be equivalently defined by the combination of
the usual strong bisimulation and ε-elimination. In this viewpoint,
our essential contribution in Sections 3.1 and 3.2 is that we define
and exploit CList and define the ε-elimination.
This paper is also related to our another submission (Asada et al.
2013), which also treats an extension of UnCAL. In the current paper, we provide a novel solution to the problem of querying over theordered graphs, while Asada et al. (2013) shows that the solution
can be partially generalized with less expressiveness of queries.
More specifically, the two papers are technically independent in thefollowing two points. First, though Asada et al. (2013) shows thatbranch patterns of graphs can be generalized by using monads, thegeneralization assumes the existence of a monad with an iteration
operator. For ordered graph case, the definition of the monad CListwith its iteration operator (i.e., the ε-elimination) is the very contribution of the current paper, and Asada et al. (2013) just use the result to include ordered graph case as an example of the generalization. The other point is that the current paper is not an instantiationof Asada et al. (2013); though the current paper extends the structural recursion with d for sibling transformations, it is not achievedin Asada et al. (2013). Also, the decidability of ε-eliminability is
not generalized in Asada et al. (2013).

7. Conclusions and Future Work
We presented the first solution to the open problem of how tomodify the graph model and structural recursion from unorderedgraphs to ordered ones and defined a new graph transformation
language λFG for doing so. The key technical contributions area novel definition of a bisimulation relation on ordered graphs
having ε-edges and an extension of structural recursion with anoperation for combining sibling results to achieve expressive poweron the sibling dimension. We implemented λFG and showed two
important optimization rules.
There are many interesting future paths of study. First, weshould analyse structural recursion more thoroughly; for instance,
we should examine the circumstances under which structural
recursion is productive. A structural recursion is said to be productive, if it produces a finite ordered graph without ε-edges (i.e.,
FG/ε defined in Section 3.3) for any input ordered graph without
ε-edge. Second, following our previous work on bidirectionalizing
UnCAL (Hidaka et al. 2010), we are very interested in developinga systematic way to bidirectionalize λFG .

Acknowledgments
We would like to thank Kazutaka Matsuda for various comments
to the current and earlier versions of the paper. We also would liketo thank the anonymous reviewers of the present and earlier versions for their thorough comments and constructive suggestions
to improve the paper. The research was supported in part by theGrand-Challenging Project on the “Linguistic Foundation for Bidi-

rectional Model Transformation” of the National Institute of Informatics, and a Grant-in-Aid for Scientific Research for Encouragement of Young Scientists (B) No. 23700047, and a Grant-in-Aid
for Scientific Research (B) No. 22300012.

References
K. Asada, S. Hidaka, H. Kato, Z. Hu, and K. Nakano. Parameterized graphtransformation languages with monads. Technical Report GRACETR-2012-07, GRACE Center, National Institute of Informatics, 2012.
http://www.biglab.org/papers.html.
K. Asada, S. Hidaka, H. Kato, Z. Hu, and K. Nakano. A parameterizedgraph transformation calculus for finite graphs with monadic branches,
2013. To appear in PPDP’13.
R. Bird and O. de Moor. Algebras of Programming. Prentice Hall, 1996.
V. Breazu-Tannen, P. Buneman, and S. Naqvi. Structural recursion asa query language. In Proc. of the Third International Workshop on
Database Programming Languages(DBPL 91), pages 9–19, 1991.
P. Buneman, M. F. Fernandez, and D. Suciu. UnQL: a query language andalgebra for semistructured data based on structural recursion. VLDB
Journal: Very Large Data Bases, 9(1):76–110, 2000.
F. W. Burton and H.-K. Yang. Manipulating multilinked data structuresin a pure functional language. Softw. Pract. Exper., 20:1167–1185,
November 1990.
S. Dal Zilio, D. Lugiez, and C. Meyssonnier. A logic you can count on.
POPL’04, pages 135–146, New York, NY, USA, 2004. ACM.
H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer. Fundamentals of Algebraic
Graph Transformation. Springer-Verlag, 2006.

F. Jouault and J. Bézivin. KM3: A DSL for metamodel specification.
In Formal Methods for Open Object-Based Distributed Systems, pages
171–185. LNCS 4037, Springer, 2006.
A. J. Kfoury and J. Tiuryn. Type reconstruction in finite-rank fragments ofthe polymorphic lambda-calculus (extended summary). In LICS, pages
2–11, 1990.
D. J. King and J. Launchbury. Structuring depth-first search algorithms in
Haskell. POPL ’95, pages 344–354, New York, 1995. ACM.
S. Lombardy and J. Sakarovitch. The removal of weighted ε-transitions.
CIAA’12, pages 345–352. Springer-Verlag, 2012.
E. Meijer, M. Fokkinga, and R. Paterson. Functional programming withbananas, lenses, envelopes and barbed wire. In Proc. Conference on
Functional Programming Languages and Computer Architecture (LNCS
523), pages 124–144, Cambridge, Massachuetts, Aug. 1991.
J. C. Mitchell. Foundations for programming languages. Foundation ofcomputing series. MIT Press, 1996.
B. C. Oliveira and W. R. Cook. Functional programming with structured
graphs. ICFP ’12, pages 77–88, New York, 2012. ACM.
C. Picard and R. Matthes. Permutations in Coinductive Graph Representation. In D. Pattinson and L. Schröder, editors, Coalgebraic Methods
in Computer Science, volume 7399 of LNCS, pages 218–237. Springer,
2012.
E. L. Robertson, L. V. Saxton, D. V. Gucht, and S. Vansummeren. Structural
recursion as a query language on lists and ordered trees. Theory ofComputing Systems, 44(4):590–619, 2009.
A. Takano and E. Meijer. Shortcut deforestation in calculational form.
FPCA ’95, pages 306–313, New York, 1995. ACM.
L. Wong. Querying Nested Collections. PhD thesis, Philadelphia, PA, USA,1994.

M. Erwig. Functional programming with graphs. ICFP ’97, pages 52–65,
New York, NY, USA, 1997. ACM.
L. Fegaras and T. Sheard. Revisiting catamorphisms over datatypes withembedded functions. POPL ’96, St. Petersburg Beach, Florida, Jan.
1996.
J. Gibbons. An initial-algebra approach to directed acyclic graphs. In Mathematics of Program Construction, MPC ’95, pages 282–303, London,
UK, 1995. Springer-Verlag.
A. Gill, J. Launchbury, and S. P. Jones. A short cut to deforestation. In
Proc. Conference on Functional Programming Languages and Computer Architecture, pages 223–232, Copenhagen, June 1993.
S. Ginali. Regular trees and the free iterative theory. J. Comput. Syst. Sci.,
18(3):228–242, 1979.
M. Hamana. Initial algebra semantics for cyclic sharing structures. TLCA
’09, pages 127–141, Berlin, Heidelberg, 2009. Springer-Verlag.
M. Hasegawa. The uniformity principle on traced monoidal categories.
Electr. Notes Theor. Comput. Sci., 69:137–155, 2002.
S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, and K. Nakano. Bidirectionalizing graph transformations. In ACM SIGPLAN International
Conference on Functional Programming, pages 205–216. ACM, 2010.
S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, K. Nakano, and I. Sasano.
Marker-directed Optimization of UnCAL Graph Transformations. In
LOPSTR’11, volume 7225 of LNCS, pages 123–138. Springer, 2012.
Z. Hu, H. Iwasaki, M. Takeichi, and A. Takano. Tupling calculation eliminates multiple data traversals. ICFP’97, pages 164–175, Amsterdam,
The Netherlands, June 1997. ACM Press.
Z. Hu, T. Yokoyama, and M. Takeichi. Program optimizations and transformations in calculational form. In Summer School on Generative andTransformational Techniques in Software Engineering, pages 139–164,
Braga, Portugal, 2006. Springer, LNCS 4043.
B. Jacobs. From coalgebraic to monoidal traces. Electronic Notes in
Theoretical Computer Science, 264(2):125 – 140, 2010. Proceedingsof the Tenth Workshop on Coalgebraic Methods in Computer Science(CMCS 2010).
T. Johnsson. Efficient graph algorithms using lazy monolithic arrays. J.
Funct. Program., 8:323–333, July 1998.

A. Semantics of Graph Constructors
Figure 10 summarizes the semantic definitions of all graph constructors in λFG . In the definitions of ++, ⊕, and @, we assume V1
and V2 to be disjoint, which is realized by taking copies of them.
The semantics should be easy to understand with the help of
Figure 5 and the intuitive explanations given in Section 2.2.1.

B. Recursive Semantics with Output Markers
In Section 4.1, we gave recursive semantics by omitting output
marker case. Throughout here, we consider general case with output markers. Hence, the typing rule is the one in Figure 4.
Now we will give both cases with and without PCC, whose
definition will be given at the end. Before that, let us see more
simple case, i.e., in addition to PCC, we assume that, for somemonoid ( , ι ) on GZ
Z×α+Z×Y ,d = foldr( , ι ) ◦ List([p, q])Z
Z: List(GZ
Z×α +GZ×Y ) → GZ×α+Z×Y
def

def

Z
where p = (-) @ binl c : GZ
Z×α → GZ×α+Z×Y and q =ZZ(-) @ binr c : GZ×Y → GZ×α+Z×Y . Then, a structural recursiondeffunction f = srec(e, d) characterized by the following recursive
semantics:
f ([])= ι
f (g1 ++ g2 ) = f (g1 ) f (g2 )= e(l, g) @ f (g)f ([l : g])f ([&y])= b&z 7→ (&z , &y)c(7)
f (&x := g) = (⊕&z∈Z (&z , &x ) := [(&z , &)]) @ f (g)f (())= ()f (g1 ⊕ g2 ) = f (g1 ) ⊕ f (g2 ).

The fourth equation is the new one for the output marker case.
The meaning should be quite easy to understand, and the following
more general versions are essentially the same as this.

[]
G1 ++ G2==

[l : G]=[&y]&x := GG1 ⊕ G2===()
G1 @ G2==

cycle(G)=({root}, {root 7→ []}, {& 7→ root}) where root is a fresh nodelet (V1 , B1 , I1 ) = G1 ; (V2 , B2 , I2 ) = G2{&x 1 , . . . , &x m } = Dom(I1 ) (= Dom(I2 ))v1 , . . . , vm are fresh node identifiers
B 0 = B1 ∪ B2 ∪{vi 7→ [Edge(ε, I1 (&x i )), Edge(ε, I2 (&xi ))] | i = 1, . . . , m}
I 0 (&xi ) = viin (V1 ∪ V2 ∪ {v1 , . . . , vm }, B 0 , I 0 )let (V, B, I) = G
root is a fresh nodein (V ∪ {root}, B ∪ {root 7→ [Edge(l, I(&))]}, {& 7→ root})({v }, {v 7→ [Outm(&y)]}, {& 7→ v }) where v is a fresh nodelet (V, B, I) = G in (V, B, {&x 7→ I(&)})
let (V1 , B1 , I1 ) = G1 ; (V2 , B2 , I2 ) = G2
in (V1 ∪ V2 , B1 ∪ B2 , I1 ∪ I2 )({}, {}, {})let (V1 , B1 , I1 ) = G1 ; (V2 , B2 , I2 ) = G2
B 0 (v1 (∈ V1 )) = [ fillOutm b | b ← B1 (v1 )]where fillOutm (Edge(l0 , v 0 )) = Edge(l0 , v 0 )fillOutm (Outm(&y)) = Edge(ε, I2 (&y))
B 0 (v2 (∈ V2 )) = B2 (v2 )in (V1 ∪ V2 , B 0 , I1 )let (V, B, I) = G
B 0 (v) = [ cyclize b | b ← B(v)]where cyclize (Edge(l0 , v 0 )) = Edge(l0 , v 0 )cyclize (Outm(&y)) = if &y ∈/ Dom(I) then Outm(&y)
else Edge(ε, I(&y))
in (V, B 0 , I)
Figure 10. Semantics of Graph Constructors

Now let us see another recursive semantics, with relaxing assumptions. For e and d satisfying PCC, we have the following recursive semantics.
()[li : gi ]f (++n)i=1[&yi ]
(
(8)
`
´ )
`
inl e(li , gi ) @ f (gi )n ´`´ ]i=1 @ b∇Z×Y c= dY [
inr b &z 7→ (&z , &yi )cwhere [xi ]ni=1 is comprehension representation of a list [x1 , ..., xn ].
The above equation is read as follows: for each i on the left handside, the content of {-} is upper or lower; then on the right handside, for each i, according to the case on the left hand side, we
think the upper or lower.
Compare the above with the following recursive semantics
given in Section 4.1, where we omit the case of output markers:f ([l1 : g1 ] ++ ... ++ [ln : gn ])`´= d∅ [e(l1 , g1 ) @ f (g1 ), ..., e(ln , gn ) @ f (gn )] .
In Section 4.1, as well as assuming Y to be ∅, we simplified thetyping of d
from

Z
Z
d : List(GZ
Z×α +GZ×Y ) → GZ×α+Z×Y

toZ
d : List(GZ
Z×α ) → GZ×αhence we did not need to use inl and ∇ in Equation (8).

For general d without assuming PCC, we have the following
recursive semantics.
()[li : gi ]n
f (++i=1)[&yi ]( `´)´` inl e(li , gi ) @ b&z 7→ (&z , &i )c`´]n= dn [(9)i=1
inr b &z 7→ (&z , &yi )c()`L´f (gi )
@ ( n
biso
c@
) ⊕ bidZ×Y cii=1[]
where isoi : Z×{i} ∼= Z.
Production-Consumption Compatibility The PCC condition is defined as follows: e: Label×GY → GZ
Z and
Z
Z
d: List(GZ
Z×α +GZ×Y ) → GZ×α+Z×Y are called productionconsumption compatible (PCC) if they satisfy the following: For
any n, suppose that, for each i ∈ n, li ∈ L, Gi ∈ GY , andG0i ∈ GZ
Z×Y are given, or &y ∈ Y is given. Then the following
equation holds(`´ )inl e(li , Gi ) @ G0i
`
´ ]n
dY ([
i=1 ) @ b∇Z×Y c
inr b&z 7→ (&z , &y)c
( `)` inl e(li , Gi ) @ b&z 7→ (&z , i)c) n ´
`
´
=dn [
]i=1
inr b&z 7→ (&z , &y)c´`L
˘G0i ¯@ ( ni=1 bisoi c@ [] ) ⊕ bidZ×Y c
where ∇Z×Y : Z×Y +Z×Y → Z×Y and isoi : Z×{i} ∼= Z.